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 : ObsoletenessCondition 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 ∨ not_exists_trigger_opt_fs obs kb.rules before after
• 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 : ObsoletenessCondition 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 : ObsoletenessCondition 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 : ObsoletenessCondition 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 : ObsoletenessCondition 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 : ObsoletenessCondition 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 : ObsoletenessCondition 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 : ObsoletenessCondition 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 : ObsoletenessCondition 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.