The Chase on Deterministic Rules

In our most general setting, we consider existential rules with disjunctions. Here, we consider the special case of deterministic rules, i.e. rules with exactly one head disjunct (so essentially no disjunction at all). Here, ChaseTree and ChaseBranch consequently coincide. At least intuitively. Formally, we still need to implement the corresponding transitions.

Arguably the most interesting result of this file is deterministicChaseBranchResultUniversallyModelsKb. It states that in the deterministic setting, the result of a ChaseBranch is itself a universal model. That is, a model that can be homomorphically embedded into every other model [DNR08]. On disjunctive rules this is more complicated as can be seen in RegularChaseTree.universal_result.

def TreeDerivation.firstBranch_from_start {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {N : Type u} [CN : ChaseNode N obs rules] (td : TreeDerivation N obs rules) (start : td.NodeWithAddress) : ChaseDerivation N obs rules

The firstBranch_from_start of a TreeDerivation is generated by always picking the first child node by starting from a particular node in the tree.

Equations

• td.firstBranch_from_start start = td.generate_subderivation start (fun (node : td.NodeWithAddress) => node.childNodes[0]?) id ⋯ ⋯

theorem TreeDerivation.branches_start_eq_firstBranch_from_start {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {N : Type u} [CN : ChaseNode N obs rules] {td : TreeDerivation N obs rules} {start : td.NodeWithAddress} (det : rules.isDeterministic) (deriv : ChaseDerivation N obs rules) : deriv ∈ start.subderivation.branches → deriv = td.firstBranch_from_start start

In the deterministic setting, each derivation in a branches of a tree derivation node directly corresponds to the firstBranch_from_start.

def TreeDerivation.firstBranch {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {N : Type u} [CN : ChaseNode N obs rules] (td : TreeDerivation N obs rules) : ChaseDerivation N obs rules

The firstBranch of a TreeDerivation is generated by always picking the first child node starting from the root.

Equations

• td.firstBranch = td.firstBranch_from_start (TreeDerivation.NodeWithAddress.root td)

theorem TreeDerivation.firstBranch_mem_branches {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {N : Type u} [CN : ChaseNode N obs rules] {td : TreeDerivation N obs rules} : td.firstBranch ∈ td.branches

The first branch is a branch. This holds in general and not only in the deterministic setting.

theorem TreeDerivation.branches_eq_firstBranch_of_determinsitic {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {N : Type u} [CN : ChaseNode N obs rules] {td : TreeDerivation N obs rules} (det : rules.isDeterministic) (b : ChaseDerivation N obs rules) : b ∈ td.branches → b = td.firstBranch

In the deterministic setting, the branches of a TreeDerivation only contain the firstBranch.

def RegularTreeDerivation.firstResult {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} (td : RegularTreeDerivation obs rules) : FactSet sig

The firstResult is the result of the firstBranch.

Equations

• td.firstResult = RegularChaseDerivation.result (TreeDerivation.firstBranch td)

theorem RegularTreeDerivation.firstResult_mem_result {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {td : RegularTreeDerivation obs rules} : td.firstResult ∈ td.result

The firstResult is a member of the TreeDerivation.result.

theorem RegularChaseTree.deterministicChaseTreeResultUniversallyModelsKb {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {kb : KnowledgeBase sig} {ct : RegularChaseTree obs kb} : kb.isDeterministic → (RegularTreeDerivation.firstResult ct.toTreeDerivation).universallyModelsKb kb

In the deterministic setting, the firstResult of a RegularChaseTree is by itself a universal model.

def ChaseDerivation.intoTree {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {N : Type u} [CN : ChaseNode N obs rules] (cd : ChaseDerivation N obs rules) (deterministic : rules.isDeterministic) : TreeDerivation N obs rules

We can straightforwardly convert a ChaseDerivation into a TreeDerivation that has the original ChaseDerivation as its only branch.

Equations

• cd.intoTree deterministic = { tree := FiniteDegreeTree.from_branch cd.branch, isSome_root := ⋯, triggers_exist := ⋯, fairness_leaves := ⋯, fairness_infinite_branches := ⋯ }

theorem ChaseDerivation.root_intoTree {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {N : Type u} [CN : ChaseNode N obs rules] {cd : ChaseDerivation N obs rules} {det : rules.isDeterministic} : (cd.intoTree det).root = cd.head

The root of intoTree is the original head.

theorem ChaseDerivation.next_intoTree {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {N : Type u} [CN : ChaseNode N obs rules] {cd : ChaseDerivation N obs rules} {det : rules.isDeterministic} : (cd.intoTree det).childNodes[0]? = cd.next

The first child node of intoTree is the original next node.

theorem ChaseDerivation.firstBranch_from_start_with_intoTree_eq_cd {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {N : Type u} [CN : ChaseNode N obs rules] {td : TreeDerivation N obs rules} {cd : ChaseDerivation N obs rules} (det : rules.isDeterministic) {start : td.NodeWithAddress} (cd_eq : cd.intoTree det = start.subderivation) : td.firstBranch_from_start start = cd

In the context of any TreeDerivation, for a given start node and a ChaseDerivation cd, firstBranch_from_start for the start node returns exactly cd as long as the tree at the start node coincides the tree transformed cd. This is an auxiliary result for firstBranch_intoTree_eq_self below.

theorem ChaseDerivation.firstBranch_intoTree_eq_self {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {N : Type u} [CN : ChaseNode N obs rules] (cd : ChaseDerivation N obs rules) (det : rules.isDeterministic) : (cd.intoTree det).firstBranch = cd

The firstBranch of intoTree is the original ChaseDerivation.

theorem ChaseDerivation.branches_intoTree {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {N : Type u} [CN : ChaseNode N obs rules] {cd : ChaseDerivation N obs rules} (det : rules.isDeterministic) (d : ChaseDerivation N obs rules) : d ∈ (cd.intoTree det).branches → d = cd

The branches of intoTree consist only of the original derivation.

theorem RegularChaseDerivation.firstResult_intoTree_eq_result {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} (cd : RegularChaseDerivation obs rules) (det : rules.isDeterministic) : RegularTreeDerivation.firstResult (ChaseDerivation.intoTree cd det) = cd.result

The firstResult of intoTree is the original ChaseDerivationSkeleton.result.

def ChaseBranch.intoTree {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {kb : KnowledgeBase sig} {N : Type u} [CN : ChaseNode N obs kb.rules] (cb : ChaseBranch N obs kb) (det : kb.isDeterministic) : ChaseTree N obs kb

We can not only convert a ChaseDerivation into a TreeDerivation but also a ChaseBranch into a ChaseTree.

Equations

• cb.intoTree det = { toTreeDerivation := cb.intoTree det, database_first := ⋯ }

theorem RegularChaseBranch.deterministicChaseBranchResultUniversallyModelsKb {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {kb : KnowledgeBase sig} (cb : RegularChaseBranch obs kb) : kb.isDeterministic → cb.result.universallyModelsKb kb

In the deterministic setting, a ChaseDerivationSkeleton.result for a ChaseBranch is a universal model.