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) : Prop

A KnowledgeBase never-terminates if none of its ChaseTrees terminates.

Equations

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

def RuleSet.neverTerminates {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (rs : RuleSet sig) (obs : ObsolescenceCondition sig) : 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 = ∃ (db : Database sig), { db := db, rules := rs }.neverTerminates obs

def Trigger.unblockable {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} (trg : Trigger obs.toLaxObsolescenceCondition) (disjIdx : Fin trg.mapped_head.length) (rules : RuleSet sig) : Prop

A trigger is unblockable if its result necessarily occurs in every derivation where the trigger is loaded. In the introducing paper this is called g-unblockable.

Equations

• One or more equations did not get rendered due to their size.

structure CyclicityDerivation {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (obs : ObsolescenceCondition sig) (rules : RuleSet sig) extends ChaseDerivationSkeleton 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 (ChaseNode obs rules)
• isSome_head : self.branch.head.isSome = true
• triggers_exist (n : Nat) (before : ChaseNode obs rules) : before ∈ (self.branch.drop n).head → let after := (self.branch.drop n).tail.head; exists_trigger_opt_fs obs rules before after
• triggers_loaded (n : Nat) (before : ChaseNode obs rules) : before ∈ (self.branch.drop n).head → ∀ (after : ChaseNode obs rules), after ∈ (self.branch.drop n).tail.head → ∃ (orig : (trg : RTrigger { cond := obs.cond, monotone := ⋯ } rules) × Fin trg.val.mapped_head.length), orig ∈ after.origin ∧ orig.fst.val.loaded before.facts
• growing (n : Nat) : ∃ (m : Nat), ∃ (t : GroundTerm sig), (∀ (node : ChaseNode obs rules), node ∈ (self.branch.drop n).head → ¬t ∈ node.facts.terms) ∧ ∃ (node : ChaseNode obs rules), node ∈ (self.branch.drop (n + m)).head ∧ t ∈ node.facts.terms
• unblockable (node : ChaseNode obs rules) : node ∈ self.branch → ∀ (orig : (trg : RTrigger { cond := obs.cond, monotone := ⋯ } rules) × Fin trg.val.mapped_head.length), orig ∈ node.origin → orig.fst.val.unblockable orig.snd rules

@[implicit_reducible]

instance CyclicityDerivation.instMembershipChaseNode {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} : Membership (ChaseNode obs rules) (CyclicityDerivation obs rules)

Equations

• CyclicityDerivation.instMembershipChaseNode = { mem := fun (cd : CyclicityDerivation obs rules) (node : ChaseNode obs rules) => node ∈ cd.toChaseDerivationSkeleton }

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

Each suffix of the underlying ChaseDerivationSkeleton is itself a CyclicityDerivation.

Equations

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

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

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

theorem CyclicityDerivation.growing'_for_list {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} (cd : CyclicityDerivation obs rules) (l : List (GroundTerm sig)) : ∃ (cd2 : CyclicityDerivation obs rules), cd2.toChaseDerivationSkeleton <:+ cd.toChaseDerivationSkeleton ∧ ∃ (t : GroundTerm sig), ¬t ∈ cd.head.facts.terms ∧ t ∈ cd2.head.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} {cd : CyclicityDerivation obs rules} (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} {cd : CyclicityDerivation obs rules} : 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} (cd : CyclicityDerivation obs rules) : ChaseNode 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} {cd : CyclicityDerivation obs rules} : 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} {cd : CyclicityDerivation obs rules} : 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} {cd : CyclicityDerivation obs rules} : cd.next.facts = cd.head.facts ∪ (cd.next.origin_result ⋯).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} {cd : CyclicityDerivation obs rules} : (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} (cd : CyclicityDerivation obs rules) : CyclicityDerivation obs rules

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} {cd : CyclicityDerivation obs rules} : cd.tail.head = cd.next

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

theorem CyclicityDerivation.result_infinite {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {cd : CyclicityDerivation obs rules} : ¬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} {cd : CyclicityDerivation obs rules} : ¬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.corresponding_tree_branch_exists {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {cd : CyclicityDerivation obs rules} (td : TreeDerivation obs rules) (same_start : cd.head.facts = td.root.facts) : ∃ (deriv : ChaseDerivation obs rules), deriv ∈ td.branches ∧ cd.result ⊆ deriv.result

In every TreeDerivation that starts on the same initial fact set as the CyclicityDerivation, there exists a branch that corresponds to the CyclicityDerivation, meaning that it has the same result.

structure CyclicityBranch {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (obs : ObsolescenceCondition sig) (kb : KnowledgeBase sig) extends CyclicityDerivation obs kb.rules : 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 (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_loaded (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.loaded before.facts
• growing (n : Nat) : ∃ (m : Nat), ∃ (t : GroundTerm sig), (∀ (node : ChaseNode obs kb.rules), node ∈ (self.branch.drop n).head → ¬t ∈ node.facts.terms) ∧ ∃ (node : ChaseNode obs kb.rules), node ∈ (self.branch.drop (n + m)).head ∧ t ∈ node.facts.terms
• unblockable (node : ChaseNode obs kb.rules) : node ∈ self.branch → ∀ (orig : (trg : RTrigger { cond := obs.cond, monotone := ⋯ } kb.rules) × Fin trg.val.mapped_head.length), orig ∈ node.origin → orig.fst.val.unblockable orig.snd kb.rules
• database_first : self.branch.head = some { facts := kb.db.toFactSet.val, origin := none, facts_contain_origin_result := ⋯ }

theorem CyclicityBranch.database_first' {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {kb : KnowledgeBase sig} {cb : CyclicityBranch 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 CyclicityDerivation vocabulary.

theorem CyclicityBranch.corresponding_tree_branch_exists {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {kb : KnowledgeBase sig} {cb : CyclicityBranch obs kb} (ct : ChaseTree obs kb) : ∃ (branch : ChaseBranch obs kb), branch.toChaseDerivation ∈ ct.branches ∧ cb.result ⊆ branch.result

In every ChaseTree, there exists a branch that corresponds to the CyclicityBranch, meaning that it has the same result.

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

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