Chase Branch

A ChaseBranch is a special kind of ChaseDerivation which is defined for a KnowledgeBase and enforces the head of the ChaseDerivation to be the database from the KnowledgeBase. This is arguably the most common way for defining chase sequences/derivations in the literature. We call this branch here, since we consider rules with disjunctions that would actually create a chase tree (see TreeDerivation and ChaseTree) and intuitively the ChaseBranch is a branch in such a tree. However, it can be defined outside the tree, which is what we do here (and mostly did for the ChaseDerivation already).

Compared to the ChaseDerivation 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.

structure ChaseBranch {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (obs : ObsolescenceCondition sig) (kb : KnowledgeBase sig) extends ChaseDerivation obs kb.rules : Type (max (max u_1 u_2) u_3)

The ChaseBranch merely extends the ChaseDerivation with the condition that the head is the database from the knowledge base.

• branch : PossiblyInfiniteList (ChaseNode obs kb.rules)
• isSome_head : self.branch.head.isSome = true
• triggers_exist (n : Nat) (before : ChaseNode obs kb.rules) : before ∈ (self.branch.drop n).head → let after := (self.branch.drop n).tail.head; exists_trigger_opt_fs obs kb.rules before after
• triggers_active (n : Nat) (before : ChaseNode obs kb.rules) : before ∈ (self.branch.drop n).head → ∀ (after : ChaseNode obs kb.rules), after ∈ (self.branch.drop n).tail.head → ∃ (orig : (trg : RTrigger { cond := obs.cond, monotone := ⋯ } kb.rules) × Fin trg.val.mapped_head.length), orig ∈ after.origin ∧ orig.fst.val.active before.facts
• fairness (trg : RTrigger { cond := obs.cond, monotone := ⋯ } kb.rules) : ∃ (i : Nat), (∃ (node : ChaseNode obs kb.rules), node ∈ (self.branch.drop i).head ∧ ¬trg.val.active node.facts) ∧ ∀ (j : Nat) (node2 : ChaseNode obs kb.rules), node2 ∈ (self.branch.drop i).tail.get? j → ¬trg.val.active node2.facts
• database_first : self.branch.head = some { facts := kb.db.toFactSet.val, origin := none, facts_contain_origin_result := ⋯ }

theorem ChaseBranch.database_first' {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {kb : KnowledgeBase sig} {cb : ChaseBranch obs kb} : cb.head = { facts := kb.db.toFactSet.val, origin := none, facts_contain_origin_result := ⋯ }

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

theorem ChaseBranch.facts_finite_of_mem {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {kb : KnowledgeBase sig} {cb : ChaseBranch obs kb} (node : cb.Node) : Set.finite node.val.facts

Opposed to a ChaseDerivation, 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 ChaseBranch.func_term_not_mem_head {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {kb : KnowledgeBase sig} {cb : ChaseBranch 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 ∈ cb.head.facts.terms

The head of the ChaseBranch does not contain any function terms.

theorem ChaseBranch.result_models_kb {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {kb : KnowledgeBase sig} {cb : ChaseBranch obs kb} : cb.result.modelsKb kb

The result of a ChaseBranch not only models the rule set but the whole KnowledgeBase.

theorem ChaseBranch.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} {cb : ChaseBranch obs kb} {node : cb.Node} : node.val.facts.constants ⊆ kb.db.constants.val ∪ kb.rules.head_constants

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

theorem ChaseBranch.functional_term_originates_from_some_trigger {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {kb : KnowledgeBase sig} {cb : ChaseBranch obs kb} (node : cb.Node) {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.val.facts.terms) : ∃ (node2 : cb.Node), node2 ≼ node ∧ ∃ (orig : (trg : RTrigger { cond := obs.cond, monotone := ⋯ } kb.rules) × Fin trg.val.mapped_head.length), orig ∈ node2.val.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 ChaseBranch.trigger_introducing_functional_term_occurs_in_chase {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {kb : KnowledgeBase sig} {cb : ChaseBranch obs kb} (node : cb.Node) {t : GroundTerm sig} (t_mem_node : t ∈ node.val.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 : cb.Node), node2 ≼ node ∧ ∃ (orig : (trg : RTrigger { cond := obs.cond, monotone := ⋯ } kb.rules) × Fin trg.val.mapped_head.length), orig ∈ node2.val.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 ChaseBranch.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} {cb : ChaseBranch obs kb} (node : cb.Node) {t : GroundTerm sig} (t_mem_node : t ∈ node.val.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.val.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.