Chase Termination

We introduce basic definitions and theorems around chase termination.

def ChaseDerivationSkeleton.terminates {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} (cds : ChaseDerivationSkeleton obs rules) : Prop

A ChaseDerivationSkeleton terminates if the underlying PossiblyInfiniteList is finite.

Equations

• cds.terminates = cds.branch.finite

def ChaseDerivation.terminates {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} (cd : ChaseDerivation obs rules) : Prop

A ChaseDerivation terminates if the underlying ChaseDerivationSkeleton is finite.

Equations

• cd.terminates = cd.terminates

def TreeDerivation.terminates {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} (td : TreeDerivation obs rules) : Prop

A TreeDerivation terminates if all of its branches terminate.

Equations

• td.terminates = ∀ (branch : ChaseDerivation obs rules), branch ∈ td.branches → branch.terminates

def KnowledgeBase.terminates {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (kb : KnowledgeBase sig) (obs : ObsolescenceCondition sig) : Prop

A KnowledgeBase terminates if all of its ChaseTrees terminate.

Equations

• kb.terminates obs = ∀ (ct : ChaseTree obs kb), ct.terminates

def RuleSet.terminates {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (rs : RuleSet sig) (obs : ObsolescenceCondition sig) : Prop

A RuleSet terminates if all knowledge bases featuring this rule set terminate.

Equations

• rs.terminates obs = ∀ (db : Database sig), { db := db, rules := rs }.terminates obs

theorem ChaseDerivationSkeleton.has_last_node_of_terminates {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} (cds : ChaseDerivationSkeleton obs rules) : cds.terminates → ∃ (node : cds.Node), ∀ (node2 : cds.Node), node2 ≼ node

If a ChaseDerivationSkeleton terminates, then there is a maximal node according to the ≼ relation.

theorem ChaseDerivation.terminating_has_last_node {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} (cd : ChaseDerivation obs rules) : cd.terminates ↔ ∃ (node : cd.Node), ∀ (node2 : cd.Node), node2 ≼ node

A ChaseDerivation terminates if and only if there is a maximal node according to the ≼ relation.

theorem ChaseBranch.terminates_iff_result_finite {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {kb : KnowledgeBase sig} (cb : ChaseBranch obs kb) : cb.terminates ↔ Set.finite cb.result

A ChaseBranch terminates if and only if its result is Set.finite.

theorem TreeDerivation.branches_finite_of_terminates {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} (td : TreeDerivation obs rules) : td.terminates → td.branches.finite

A terminating TreeDerivation only has finitely many branches. We show this using König's Lemma.

theorem TreeDerivation.result_finite_of_branches_finite {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} (td : TreeDerivation obs rules) : td.branches.finite → td.result.finite

A TreeDerivation with finitely many branches only has finitely many fact sets in its result.

theorem ChaseTree.terminates_iff_result_finite {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {kb : KnowledgeBase sig} (ct : ChaseTree obs kb) : ct.terminates ↔ ∀ (fs : FactSet sig), fs ∈ ct.result → Set.finite fs

A ChaseTree terminates if and only if each fact set in its result is finite.