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 }

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 vocabulary available for ChaseDerivationSkeletons.

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.

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 := ⋯ }