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] (obs : ObsoletenessCondition sig) (kb : KnowledgeBase sig) extends TreeDerivation obs kb.rules : Type (max (max u_1 u_2) u_3)

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

• tree : FiniteDegreeTree (ChaseNode obs kb.rules)
• isSome_root : self.tree.root.isSome = true
• triggers_exist (ns : List Nat) (before : ChaseNode obs kb.rules) : before ∈ (self.tree.drop ns).root → let after := (self.tree.drop ns).childNodes; exists_trigger_list obs kb.rules before after ∨ not_exists_trigger_list obs kb.rules before after
• fairness_leaves (leaf : ChaseNode obs kb.rules) : leaf ∈ self.tree.leaves → ∀ (trg : RTrigger { cond := obs.cond, monotone := ⋯ } kb.rules), ¬trg.val.active leaf.facts
• fairness_infinite_branches (trg : RTrigger { cond := obs.cond, monotone := ⋯ } kb.rules) : ∃ (i : Nat), ∀ (ns : List Nat), ns.length ≥ i → ∀ (node : ChaseNode obs kb.rules), node ∈ self.tree.get? ns → ¬trg.val.active node.facts
• database_first : self.tree.root = some { facts := kb.db.toFactSet.val, origin := none, facts_contain_origin_result := ⋯ }

instance ChaseTree.instMembershipChaseNodeRules {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsoletenessCondition sig} {kb : KnowledgeBase sig} : Membership (ChaseNode obs kb.rules) (ChaseTree obs kb)

Equations

• ChaseTree.instMembershipChaseNodeRules = { mem := fun (td : ChaseTree obs kb) (node : ChaseNode obs kb.rules) => node ∈ td.tree }

def ChaseTree.chaseBranch_for_branch {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsoletenessCondition sig} {kb : KnowledgeBase sig} {ct : ChaseTree obs kb} {branch : ChaseDerivation obs kb.rules} (branch_mem : branch ∈ ct.branches) : ChaseBranch 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.database_first' {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsoletenessCondition sig} {kb : KnowledgeBase sig} {ct : ChaseTree obs kb} : ct.root = { facts := kb.db.toFactSet.val, origin := none, facts_contain_origin_result := ⋯ }

We restate the database_first condition in terms of the TreeDerivation vocabulary.

theorem ChaseTree.facts_finite_of_mem {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsoletenessCondition sig} {kb : KnowledgeBase sig} {ct : ChaseTree obs kb} {node : ChaseNode 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.

theorem ChaseTree.func_term_not_mem_root {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsoletenessCondition sig} {kb : KnowledgeBase sig} {ct : ChaseTree 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 ∈ ct.root.facts.terms

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

theorem ChaseTree.result_models_kb {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsoletenessCondition sig} {kb : KnowledgeBase sig} {ct : ChaseTree 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 ChaseTree.constants_node_subset_constants_db_union_constants_rules {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsoletenessCondition sig} {kb : KnowledgeBase sig} {ct : ChaseTree obs kb} {node : ChaseNode 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 ChaseTree.functional_term_originates_from_some_trigger {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsoletenessCondition sig} {kb : KnowledgeBase sig} {ct : ChaseTree 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.mapped_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 ChaseTree.trigger_introducing_functional_term_occurs_in_chase {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsoletenessCondition sig} {kb : KnowledgeBase sig} {ct : ChaseTree 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.mapped_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 ChaseTree.result_of_trigger_introducing_functional_term_occurs_in_chase {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsoletenessCondition sig} {kb : KnowledgeBase sig} {ct : ChaseTree 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.