RPC-like Non-Termination

We are going to formalize sufficient conditions for chase non-termination. Mainly, we will introduce the necessary machinery from Restricted Prefix Cyclicity (RPC) [GC23a] but we also aim to generalize this to capture (Disjunctive) Model-Faithful Cyclicity ((D)MFC) [GC23b] [CDK17] at the same time.

SO FAR, WE ONLY HAVE A FEW VERY BASIC DEFINITIONS. THERE IS A LONG WAY TO GO.

def KnowledgeBase.neverTerminates {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 never-terminates if none of its ChaseTrees terminates.

Equations

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

def RuleSet.neverTerminates {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

Maybe this seems counterintuitive but a RuleSet never-terminates if for at least one Database the corresponding KnowledgeBase.neverTerminates. Asking this question for all Databases would be trivial, at least for the restricted chase, since for every rule set there is a database that satisfies all the rules directly and therefore only has terminating restricted chase trees.

Equations

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

structure CyclicityDerivation {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (obs : ObsolescenceCondition sig) (rules : RuleSet sig) (hc : HeadChoice sig) extends ChaseDerivationSkeleton (RegularChaseNode obs rules) obs rules : Type (max (max u_1 u_2) u_3)

A CyclicityDerivation is an infinite list of ChaseNodes. We demand only that triggers are loaded, new terms keep being added (growing) and that triggers are unblockable. This is much different from a ChaseDerivation but intuitively, we can view a CyclicityDerivation as a very special non-continuous subderivation of a suitable ChaseDerivation.

• branch : PossiblyInfiniteList (RegularChaseNode obs rules)
• isSome_head : self.branch.head.isSome = true
• triggers_exist (b2 : PossiblyInfiniteList (RegularChaseNode obs rules)) : b2 <:+ self.branch → ∀ (before : RegularChaseNode obs rules), before ∈ b2.head → ∀ (after : RegularChaseNode obs rules), after ∈ b2.tail.head → ChaseNode.succ before after
• adheres_to_headChoice : self.adheres_to_headChoice hc
• triggers_loaded (cd2 : ChaseDerivationSkeleton (RegularChaseNode obs rules) obs rules) : cd2 <:+ self.toChaseDerivationSkeleton → ∀ (next : RegularChaseNode obs rules), next ∈ cd2.next → ∃ (orig : (trg : RTrigger { cond := obs.cond, monotone := ⋯ } rules) × Fin trg.val.rule.head.length), orig ∈ next.origin ∧ orig.fst.val.loaded cd2.head.facts
• growing (cd2 : ChaseDerivationSkeleton (RegularChaseNode obs rules) obs rules) : cd2 <:+ self.toChaseDerivationSkeleton → ∃ (node : RegularChaseNode obs rules), node ∈ cd2 ∧ ∃ (t : GroundTerm sig), ¬t ∈ cd2.head.facts.terms ∧ t ∈ node.facts.terms
• unblockable (node : RegularChaseNode obs rules) : node ∈ self.toChaseDerivationSkeleton → ∀ (orig : (trg : RTrigger { cond := obs.cond, monotone := ⋯ } rules) × Fin trg.val.rule.head.length), orig ∈ node.origin → Trigger.unblockable rules hc orig.fst.val

@[instance_reducible]

instance CyclicityDerivation.instMembershipRegularChaseNode {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {hc : HeadChoice sig} : Membership (RegularChaseNode obs rules) (CyclicityDerivation obs rules hc)

Equations

• CyclicityDerivation.instMembershipRegularChaseNode = { mem := fun (cd : CyclicityDerivation obs rules hc) (node : RegularChaseNode obs rules) => node ∈ cd.toChaseDerivationSkeleton }

theorem CyclicityDerivation.mem_iff {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {hc : HeadChoice sig} {cd : CyclicityDerivation obs rules hc} {e : RegularChaseNode obs rules} : e ∈ cd ↔ ∃ (n : Nat), cd.branch.get? n = some e

An element is a member of the derivation iff it occurs at some index in the underlying branch.

def CyclicityDerivation.derivation_for_skeleton {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {hc : HeadChoice sig} (cd : CyclicityDerivation obs rules hc) (l2 : RegularChaseDerivationSkeleton obs rules) (suffix : l2 <:+ cd.toChaseDerivationSkeleton) : CyclicityDerivation obs rules hc

Each suffix of the underlying ChaseDerivationSkeleton is itself a CyclicityDerivation.

Equations

• cd.derivation_for_skeleton l2 suffix = { toChaseDerivationSkeleton := l2, adheres_to_headChoice := ⋯, triggers_loaded := ⋯, growing := ⋯, unblockable := ⋯ }

theorem CyclicityDerivation.growing' {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {hc : HeadChoice sig} {cd : CyclicityDerivation obs rules hc} : ∃ (node : RegularChaseNode obs rules), node ∈ cd ∧ ∃ (t : GroundTerm sig), ¬t ∈ cd.head.facts.terms ∧ t ∈ node.facts.terms

We state a simplified version of the growing property.

theorem CyclicityDerivation.growing'_for_list {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {hc : HeadChoice sig} (cd : CyclicityDerivation obs rules hc) (l : List (GroundTerm sig)) : ∃ (node : RegularChaseNode obs rules), node ∈ cd ∧ ∃ (t : GroundTerm sig), ¬t ∈ cd.head.facts.terms ∧ t ∈ node.facts.terms ∧ ¬t ∈ l

Given a list of terms, we can find a suffix that contains a term that is not part of this list because of the growing property. This result is closest to the growing' statement.

theorem CyclicityDerivation.growing'' {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {hc : HeadChoice sig} {cd : CyclicityDerivation obs rules hc} (node : cd.Node) : ∃ (node2 : cd.Node), node ≺ node2 ∧ ∃ (t : GroundTerm sig), ¬t ∈ node.val.facts.terms ∧ t ∈ node2.val.facts.terms

We restate the growing property using predecessor vocabulary available for ChaseDerivationSkeletons.

theorem CyclicityDerivation.isSome_next {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {hc : HeadChoice sig} {cd : CyclicityDerivation obs rules hc} : cd.next.isSome = true

Since the derivation is growing, a next node always exists.

def CyclicityDerivation.next {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {hc : HeadChoice sig} (cd : CyclicityDerivation obs rules hc) : RegularChaseNode obs rules

Lifting ChaseDerivationSkeleton.next to the CyclicityDerivation.

Equations

• cd.next = cd.next.get ⋯

theorem CyclicityDerivation.next_mem {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {hc : HeadChoice sig} {cd : CyclicityDerivation obs rules hc} : cd.next ∈ cd

The next node is a member.

theorem CyclicityDerivation.isSome_origin_next {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {hc : HeadChoice sig} {cd : CyclicityDerivation obs rules hc} : cd.next.origin.isSome = true

The origin of the next ChaseNode needs to be set.

theorem CyclicityDerivation.facts_next {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {hc : HeadChoice sig} {cd : CyclicityDerivation obs rules hc} : cd.next.facts = cd.head.facts ∪ (ChaseNode.origin_result cd.next ⋯).toSet

The fact set of the next ChaseNode consists exactly of the facts from head and the result of the trigger that introduces next.

theorem CyclicityDerivation.loaded_trigger_origin_next {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {hc : HeadChoice sig} {cd : CyclicityDerivation obs rules hc} : (cd.next.origin.get ⋯).fst.val.loaded cd.head.facts

The trigger used to derive ChaseDerivationSkeleton.next is loaded for ChaseDerivationSkeleton.head.

def CyclicityDerivation.tail {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {hc : HeadChoice sig} (cd : CyclicityDerivation obs rules hc) : CyclicityDerivation obs rules hc

The tail of a CyclicityDerivation is again a CyclicityDerivation.

Equations

• cd.tail = cd.derivation_for_skeleton (cd.tail ⋯) ⋯

@[simp]

theorem CyclicityDerivation.head_tail {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {hc : HeadChoice sig} {cd : CyclicityDerivation obs rules hc} : cd.tail.head = cd.next

The ChaseDerivationSkeleton.head of the tail is ChaseDerivationSkeleton.next.

@[reducible, inline]

abbrev CyclicityDerivation.result {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {hc : HeadChoice sig} (cd : CyclicityDerivation obs rules hc) : FactSet sig

We define a shortcut for RegularChaseDerivationSkeleton.result.

Equations

• cd.result = RegularChaseDerivationSkeleton.result cd.toChaseDerivationSkeleton

theorem CyclicityDerivation.result_infinite {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {hc : HeadChoice sig} {cd : CyclicityDerivation obs rules hc} : ¬Set.finite cd.result

The result of a CyclicityDerivation is infinite due to the growing property.

theorem CyclicityDerivation.infinite {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {hc : HeadChoice sig} {cd : CyclicityDerivation obs rules hc} : ¬cd.terminates

Each CyclicityDerivation is infinite because it is growing. It might surprise that this is independant from the above result. However, note that we can only relate finiteness of the result and termination for proper ChaseBranches so corresponding results are not applicable here.

theorem CyclicityDerivation.mem_subderivation_for_headChoice_of_mem {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {hc : HeadChoice sig} {cd : CyclicityDerivation obs rules hc} (kb : KnowledgeBase sig) (rules_eq : kb.rules = rules) (ct : RegularChaseTree obs kb) (same_start : cd.head.facts = ct.root.facts) (node : RegularChaseNode obs rules) : node ∈ cd → ∃ (node' : RegularChaseNode obs kb.rules), node' ∈ (ChaseTree.subderivation_for_headChoice ct hc).toChaseDerivation ∧ node.facts ⊆ node'.facts

For each node in the CyclicityDerivation, there is a node in the subderivation_for_headChoice for every TreeDerivation subsumes the facts.

theorem CyclicityDerivation.result_subset_result_subderivation_for_headChoice {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {hc : HeadChoice sig} {cd : CyclicityDerivation obs rules hc} (kb : KnowledgeBase sig) (rules_eq : kb.rules = rules) (ct : RegularChaseTree obs kb) (same_start : cd.head.facts = ct.root.facts) : cd.result ⊆ RegularChaseBranch.result (ChaseTree.subderivation_for_headChoice ct hc)

The result of a CyclicityDerivation is a subset of the result of the subderivation_for_headChoice for every TreeDerivation.

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

This is the CyclicitySequence from the RPC paper. For us, it is a CyclicityDerivation that starts on a database.

• branch : PossiblyInfiniteList (RegularChaseNode obs kb.rules)
• isSome_head : self.branch.head.isSome = true
• triggers_exist (b2 : PossiblyInfiniteList (RegularChaseNode obs kb.rules)) : b2 <:+ self.branch → ∀ (before : RegularChaseNode obs kb.rules), before ∈ b2.head → ∀ (after : RegularChaseNode obs kb.rules), after ∈ b2.tail.head → ChaseNode.succ before after
• adheres_to_headChoice : self.adheres_to_headChoice hc
• triggers_loaded (cd2 : ChaseDerivationSkeleton (RegularChaseNode obs kb.rules) obs kb.rules) : cd2 <:+ self.toChaseDerivationSkeleton → ∀ (next : RegularChaseNode obs kb.rules), next ∈ cd2.next → ∃ (orig : (trg : RTrigger { cond := obs.cond, monotone := ⋯ } kb.rules) × Fin trg.val.rule.head.length), orig ∈ next.origin ∧ orig.fst.val.loaded cd2.head.facts
• growing (cd2 : ChaseDerivationSkeleton (RegularChaseNode obs kb.rules) obs kb.rules) : cd2 <:+ self.toChaseDerivationSkeleton → ∃ (node : RegularChaseNode obs kb.rules), node ∈ cd2 ∧ ∃ (t : GroundTerm sig), ¬t ∈ cd2.head.facts.terms ∧ t ∈ node.facts.terms
• unblockable (node : RegularChaseNode obs kb.rules) : node ∈ self.toChaseDerivationSkeleton → ∀ (orig : (trg : RTrigger { cond := obs.cond, monotone := ⋯ } kb.rules) × Fin trg.val.rule.head.length), orig ∈ node.origin → Trigger.unblockable kb.rules hc orig.fst.val
• database_first : self.head.facts = kb.db.toFactSet.val ∧ self.head.origin = none

theorem CyclicityBranch.result_subset_result_subderivation_for_headChoice {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {kb : KnowledgeBase sig} {hc : HeadChoice sig} {cb : CyclicityBranch obs kb hc} (ct : RegularChaseTree obs kb) : cb.result ⊆ RegularChaseBranch.result (ChaseTree.subderivation_for_headChoice ct hc)

The result of a CyclicityBranch is a subset of the result of the subderivation_for_headChoice for every ChaseTree.

theorem CyclicityBranch.neverTerminates_of_cyclicityBranch {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {hc : HeadChoice sig} {obs : ObsolescenceCondition sig} {kb : KnowledgeBase sig} (cb : CyclicityBranch obs kb hc) : kb.rules.neverTerminates obs (RegularChaseNode obs kb.rules)

If a KB admist a CyclicityBranch, then its rule set neverTerminates.