Chase Tree

A ChaseTree is a special kind of TreeDerivation which is defined for a KnowledgeBase and enforces the root of the TreeDerivation to be the database from the KnowledgeBase.

Compared to the TreeDerivation some new theorems can be shown or some existing ones strengthened. For example, we know now that functional terms can never occur in a database so every functional term must originate as a fresh term from some trigger that is used in the chase.

The ChaseTree is to the TreeDerivation what the ChaseBranch is to the ChaseDerivation.

structure ChaseTree {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (N : Type u) (obs : ObsolescenceCondition sig) (kb : KnowledgeBase sig) [CN : ChaseNode N obs kb.rules] extends TreeDerivation N obs kb.rules : Type u

The ChaseTree merely extends the TreeDerivation with the condition that the root is the database from the knowledge base.

• tree : FiniteDegreeTree N
• isSome_root : self.tree.root.isSome = true
• triggers_exist (t2 : FiniteDegreeTree N) : t2 <:+ self.tree → ∀ (before : N), before ∈ t2.root → ChaseNode.succ_list before t2.childNodes
• fairness_leaves (leaf : N) : leaf ∈ self.tree.leaves → ∀ (trg : RTrigger { cond := obs.cond, monotone := ⋯ } kb.rules), ¬trg.val.active (ChaseNode.outgoingFacts obs kb.rules leaf)
• fairness_infinite_branches (trg : RTrigger { cond := obs.cond, monotone := ⋯ } kb.rules) : ∃ (i : Nat), ∀ (ns : List Nat), ns.length ≥ i → ∀ (node : N), node ∈ self.tree.get? ns → ¬trg.val.active (ChaseNode.outgoingFacts obs kb.rules node)
• database_first : ChaseNode.ingoingFacts obs kb.rules self.root = kb.db.toFactSet.val ∧ ChaseNode.outgoingFacts obs kb.rules self.root = kb.db.toFactSet.val ∧ ChaseNode.origin self.root = none

@[instance_reducible]

instance ChaseTree.instMembership {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] : Membership N (ChaseTree N obs kb)

Equations

• ChaseTree.instMembership = { mem := fun (td : ChaseTree N obs kb) (node : N) => node ∈ td.tree }

theorem ChaseTree.mem_iff {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] {ct : ChaseTree N obs kb} {e : N} : e ∈ ct ↔ ∃ (ns : List Nat), ct.tree.get? ns = some e

An element is a member of the tree iff it occurs at some address.

def ChaseTree.chaseBranch_for_branch {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] {ct : ChaseTree N obs kb} {branch : ChaseDerivation N obs kb.rules} (branch_mem : branch ∈ ct.branches) : ChaseBranch N obs kb

We can convert ChaseDerivations that are branches in the ChaseTree to ChaseBranches.

Equations

• ChaseTree.chaseBranch_for_branch branch_mem = { toChaseDerivation := branch, database_first := ⋯ }

theorem ChaseTree.func_term_not_mem_root {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] {ct : ChaseTree N obs kb} {t : GroundTerm sig} (t_is_func : ∃ (func : SkolemFS sig), ∃ (ts : List (GroundTerm sig)), ∃ (arity_ok : ts.length = func.arity), t = GroundTerm.func func ts arity_ok) : ¬t ∈ (ChaseNode.outgoingFacts obs kb.rules ct.root).terms

The root of the ChaseTree does not contain any function terms.

theorem ChaseTree.mem_childTrees_of_isSome_origin {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] {ct : ChaseTree N obs kb} {n : N} (n_mem : n ∈ ct) : (ChaseNode.origin n).isSome = true → ∃ (c : TreeDerivation N obs kb.rules), c ∈ ct.childTrees ∧ n ∈ c

A node that has an origin must be in a child tree.

theorem ChaseTree.mem_childNodes_of_some_member_of_isSome_origin {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] {ct : ChaseTree N obs kb} (n : ct.NodeWithAddress) : (ChaseNode.origin n.node).isSome = true → ∃ (n2 : ct.NodeWithAddress), n ∈ n2.childNodes

Each node that has an origin must be a child node of some other node in the tree.

RegularChaseTree

Similar to the RegularTreeDerivation, we consider RegularChaseTrees as the special ChaseTrees where the node type is fixed to be RegularChaseNode (representing Skolem and restricted chase).

@[reducible, inline]

abbrev RegularChaseTree {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (obs : ObsolescenceCondition sig) (kb : KnowledgeBase sig) : Type (max (max u_3 u_2) u_1)

Equations

• RegularChaseTree obs kb = ChaseTree (RegularChaseNode obs kb.rules) obs kb

theorem RegularChaseTree.facts_finite_of_mem {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {kb : KnowledgeBase sig} {ct : RegularChaseTree obs kb} {node : RegularChaseNode obs kb.rules} (node_mem : node ∈ ct) : Set.finite node.facts

Opposed to a TreeDerivation, we know that each node in a ChaseBranch has a finite set of facts. This is because the database is finite and each trigger only adds finitely many new facts.

@[reducible, inline]

abbrev RegularChaseTree.result {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {kb : KnowledgeBase sig} (ct : RegularChaseTree obs kb) : Set (FactSet sig)

We define a shortcut for RegularTreeDerivation.result.

Equations

• ct.result = RegularTreeDerivation.result ct.toTreeDerivation

theorem RegularChaseTree.result_models_kb {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {kb : KnowledgeBase sig} {ct : RegularChaseTree obs kb} (fs : FactSet sig) : fs ∈ ct.result → fs.modelsKb kb

Each element of the result of a ChaseTree not only models the rule set but the whole KnowledgeBase.

theorem RegularChaseTree.constants_node_subset_constants_db_union_constants_rules {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {kb : KnowledgeBase sig} {ct : RegularChaseTree obs kb} {node : RegularChaseNode obs kb.rules} (node_mem : node ∈ ct) : node.facts.constants ⊆ kb.db.constants.val ∪ kb.rules.head_constants

Constants in the chase must be in the database or in some rule.

theorem RegularChaseTree.functional_term_originates_from_some_trigger {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {kb : KnowledgeBase sig} {ct : RegularChaseTree obs kb} (node : ct.NodeWithAddress) {t : GroundTerm sig} (t_is_func : ∃ (func : SkolemFS sig), ∃ (ts : List (GroundTerm sig)), ∃ (arity_ok : ts.length = func.arity), t = GroundTerm.func func ts arity_ok) (t_mem : t ∈ node.node.facts.terms) : ∃ (node2 : ct.NodeWithAddress), node2 ≼ node ∧ ∃ (orig : (trg : RTrigger { cond := obs.cond, monotone := ⋯ } kb.rules) × Fin trg.val.rule.head.length), orig ∈ node2.node.origin ∧ t ∈ orig.fst.val.fresh_terms_for_head_disjunct ↑orig.snd ⋯

Each functional term in the chase originates as a fresh term from a trigger.

theorem RegularChaseTree.trigger_introducing_functional_term_occurs_in_chase {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {kb : KnowledgeBase sig} {ct : RegularChaseTree obs kb} (node : ct.NodeWithAddress) {t : GroundTerm sig} (t_mem_node : t ∈ node.node.facts.terms) {trg : RTrigger { cond := obs.cond, monotone := ⋯ } kb.rules} {disj_idx : Nat} {lt : disj_idx < trg.val.rule.head.length} (t_mem_trg : t ∈ trg.val.fresh_terms_for_head_disjunct disj_idx lt) : ∃ (node2 : ct.NodeWithAddress), node2 ≼ node ∧ ∃ (orig : (trg : RTrigger { cond := obs.cond, monotone := ⋯ } kb.rules) × Fin trg.val.rule.head.length), orig ∈ node2.node.origin ∧ orig.fst.equiv trg ∧ ↑orig.snd = disj_idx

If a functional term occurs in the chase, then the trigger that introduces this term must have been used in the chase.

theorem RegularChaseTree.result_of_trigger_introducing_functional_term_occurs_in_chase {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {kb : KnowledgeBase sig} {ct : RegularChaseTree obs kb} (node : ct.NodeWithAddress) {t : GroundTerm sig} (t_mem_node : t ∈ node.node.facts.terms) {trg : RTrigger { cond := obs.cond, monotone := ⋯ } kb.rules} {disj_idx : Nat} {lt : disj_idx < trg.val.rule.head.length} (t_mem_trg : t ∈ trg.val.fresh_terms_for_head_disjunct disj_idx lt) : trg.val.mapped_head[disj_idx].toSet ⊆ node.node.facts

If a functional term occurs in the chase, then the result of the trigger that introduces this term is contained in the current node.