Chase Termination

We introduce basic definitions and theorems around chase termination.

@[implicit_reducible]

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

A ChaseDerivationSkeleton terminates if the underlying PossiblyInfiniteList is finite.

Equations

• cds.terminates = cds.branch.finite

theorem ChaseDerivationSkeleton.terminates_iff_terminates_suffix {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {N : Type u} [CN : ChaseNode N obs rules] {cd cd2 : ChaseDerivationSkeleton N obs rules} (suf : cd2 <:+ cd) : cd.terminates ↔ cd2.terminates

A ChaseDerivationSkeleton terminates if and only if its suffixes terminate.

@[implicit_reducible]

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

A ChaseDerivation terminates if the underlying ChaseDerivationSkeleton is finite.

Equations

• cd.terminates = cd.terminates

@[implicit_reducible]

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

A TreeDerivation terminates if all of its branches terminate.

Equations

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

@[implicit_reducible]

def KnowledgeBase.terminates {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (kb : KnowledgeBase sig) (obs : ObsolescenceCondition sig) (N : Type u) [CN : ChaseNode N obs kb.rules] : Prop

A KnowledgeBase terminates if all of its ChaseTrees terminate.

Equations

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

@[implicit_reducible]

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

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

Equations

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

Last Chase Element

For terminating derivations, we define machinery to get the last chase node from the derivation.

def ChaseDerivationSkeleton.last {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {N : Type u} [CN : ChaseNode N obs rules] (cd : ChaseDerivationSkeleton N obs rules) (term : cd.terminates) : N

For terminating derivations, we define the last chase node via turning the derivation into a finite list and then retreiving the last element.

Equations

• cd.last term = (cd.branch.toList_of_finite term).getLast ⋯

theorem ChaseDerivationSkeleton.last_mem {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {N : Type u} [CN : ChaseNode N obs rules] {cd : ChaseDerivationSkeleton N obs rules} (term : cd.terminates) : cd.last term ∈ cd

The last node is a member of the derivation.

theorem ChaseDerivationSkeleton.last_eq_of_suffix {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {N : Type u} [CN : ChaseNode N obs rules] {cd cd2 : ChaseDerivationSkeleton N obs rules} (suf : cd2 <:+ cd) (term : cd.terminates) : cd.last term = cd2.last ⋯

All suffixes have the same last node.

theorem ChaseDerivationSkeleton.each_prec_last {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {N : Type u} [CN : ChaseNode N obs rules] {cd : ChaseDerivationSkeleton N obs rules} (term : cd.terminates) (node : cd.Node) : node ≼ ⟨cd.last term, ⋯⟩

Every node is a predecessor of the last one.

theorem RegularChaseDerivationSkeleton.result_eq_facts_last {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {cd : RegularChaseDerivationSkeleton obs rules} (term : ChaseDerivationSkeleton.terminates cd) : cd.result = (ChaseDerivationSkeleton.last cd term).facts

For terminating derivations, the result is equal to the facts of the last node.

theorem ChaseDerivation.trg_inactive_for_last {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {N : Type u} [CN : ChaseNode N obs rules] {cd : ChaseDerivation N obs rules} (term : cd.terminates) (trg : RTrigger { cond := obs.cond, monotone := ⋯ } rules) : ¬trg.val.active (ChaseNode.outgoingFacts obs rules (cd.last term))

No trigger is active on the last node.

We now show some general results mainly relating termination and finiteness of the chase result.

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

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

theorem RegularChaseBranch.terminates_iff_result_finite {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {kb : KnowledgeBase sig} (cb : RegularChaseBranch 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} {N : Type u} [CN : ChaseNode N obs rules] (td : TreeDerivation N obs rules) : td.terminates → td.branches.finite

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

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

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

theorem RegularChaseTree.terminates_iff_result_finite {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {kb : KnowledgeBase sig} (ct : RegularChaseTree 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.