Model-Faithful Acyclicity and its Relatives

There is plenty of research around sufficient conditions for chase termination. These are usually conditions on RuleSets. If they are fulfilled, we know that the RuleSet.terminates. If they are not fulfilled, we gain nothing. Here, we consider variants of Model-Faithful Acyclicity (MFA) [CGHK+13], Disjunctive MFA (DMFA) [GC23b] and Restricted MFA (RMFA) [CDK17] essentially all at once. We should note though that technically DMFA and RMFA assume a so-called Datalog-first chase, which always prefers triggers with Datalog rules before all others. So far, we are not modelling this possibility in our chase definitions. Consequently, we also implement slightly different versions of DMFA and RMFA that simply drop the part that optimizes for Datalog-first sequences. The modified versions are of course still correct (as we prove) but lifting the restriction of Datalog-first chase comes at the cost of potentially marking fewer rule sets as terminating. Indeed there are rule sets that would terminate for all Datalog-first chases but not for all more liberal application strategies. In the future, we also aim to formalize the original Datalog-first version.

How does MFA work?

The idea is almost shockingly simple. First of all, for MFA, we turn all disjunctions in rules into conjunctions. Then, we compute the chase on the new rule set and a special database and stop as soon as we see a cyclic function term. If we see such a term, we do not learn anything about termination. If we do not see such a term, then the chase computed for MFA will terminate on its own, since there are only finitely many non-cyclic terms. But then, we can argue that any chase on any database also terminates since MFA basically generalizes all of them. MFA shows termination of a rule set for the so-called Skolem chase, i.e. if we consider SkolemObsolescence for the ObsolescenceCondition. But SkolemObsolescence is actually the "most non-terminating" of our ObsolescenceConditions so we really are able to show that MFA guarantees termination no matter which ObsolescenceCondition we choose. See terminates_of_isMfa_with_DeterministicSkolemObsolescence. Note what we call isMfa in our framework is already a generalized version of MFA that is also able to captures the (modified versions of) DMFA and RMFA by accepting something called MfaObsolescenceCondition. So what we call MFA here is really isMfa with the DeterministicSkolemObsolescence.

How do DMFA and RMFA work?

For MFA everything is comparibly simple since there are no disjunctions and we really only care about the Skolem chase. It is not obvious but in this setting no trigger is every really obsolete unless its exact result is already part of the chase. But then applying the trigger would not make a difference anyway. This is different if disjunctions are present or if we consider a stricter ObsolescenceCondition (or both). Less triggers might be active and therefore the chase may terminate in more cases. MFA would still work but maybe we can do better now. This is exactly the motivation behind DMFA and RMFA, where DMFA is optimized for Skolem chase on disjunctive rules and RMFA is designed for the restricted chase, potentially also with disjunctive rules.

The basic idea remains the same. We just simulate the chase on a special database. However, we now want to forbid certain trigger applications; ones that we call "blocked". Formally, we can say that a trigger is blocked if we know that whenever it is loaded in a chase, then it is necessarily already obsolete. To see why this may happen, remember that a trigger might require various facts to be introduced during the chase to become loaded. It can happen that the necessary facts at the same time also make the trigger obsolete, in which case we say that it is blocked. In our framework, we realize this by using BlockingObsolescence for the MfaObsolescenceCondition in isMfa. Blocking is very similar for DMFA and RMFA and essentially only differs in the ObsolescenceCondition that for DMFA would be SkolemObsolescence and for RMFA would be RestrictedObsolescence. So what we do is simple: BlockingObsolescence is simply defined taking a ObsolescenceCondition condition as a parameter. Thereby we obtain an MFA-like condition for any ObsolescenceCondition that one can imagine. So we can express DMFA, RMFA, and everything in-between. We show in terminates_of_isMfa_with_BlockingObsolescence that isMfa with any such BlockingObsolescence guarantees termination.

Our Framework

Despite the differences between MFA and DMFA/RMFA, you may realize that terminates_of_isMfa_with_DeterministicSkolemObsolescence and terminates_of_isMfa_with_BlockingObsolescence essentially use the same proof, namely they just call terminates_of_isMfa. This result is generic over all possible MfaObsolescenceConditions and just demands that the given MfaObsolescenceCondition has the blocks_obs property with respect to the target ObsolescenceCondition. For example, the DeterministicSkolemObsolescence used for (the original) MFA has the blocks_obs property with respect to all ObsolescenceConditions and the BlockingObsolescence for a given ObsolescenceCondition $o$ has the blocks_obs property with respect to $o$. Of course, this is something we need to prove and we do this in DeterministicSkolemObsolescence.blocks_each_obs and BlockingObsolescence.blocks_corresponding_obs, respectively.

How to actually check if a trigger is blocked?

The definition of BlockingObsolescence and also the proof of BlockingObsolescence.blocks_corresponding_obs is awefully technical. To check if a trigger is blocked, we backtrack where the functional terms involved in its mapped body come from. We can do this, since each function symbol has a rule and disjunct id. Based on this information, we know which trigger must have been applied to make our target trigger loaded. At least almost. The functional terms contain the mapped frontier, which we can use for reconstruction, but we do not know the mapping for the remaining body variables. This could be anything. To not cause any interference there, we map them to fresh constants. While this is simply stated on paper, it is quite an effort to do formally. And there is yet another place where we require fresh constants. For reasons beyond what I want to discuss here, to check if a trigger is blocked, we first need to rename all of its constant occurrences apart, which again uses fresh constants.

If you actually aim to understand all the details, then good luck! There are a few doc comments on what happens in the individual files so you can dig into those a bit more. You can also have a look at the papers introducing the notions but this is likely still mind-boggling. Feel free to reach out to me at any point. I will try my best to explain and answer your questions!

noncomputable def RuleSet.mfaConstantMapping {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (rs : RuleSet sig) (special_const : sig.C) : StrictConstantMapping sig

At some point we need to map constants from arbitrary chases to the ones in the special database. For this, we map all rule set constants to themselves and all others to the single special_const.

Equations

• rs.mfaConstantMapping special_const c = if c ∈ rs.constants then c else special_const

theorem RuleSet.mfaConstantMapping_id_on_rs_constants {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (rs : RuleSet sig) (special_const c : sig.C) : c ∈ rs.constants → rs.mfaConstantMapping special_const c = c

Indeed the mfaConstantMapping is the id on all rule set constants.

theorem RuleSet.mfaConstantMapping_id_on_atom_from_rule {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (rs : RuleSet sig) (special_const : sig.C) (r : Rule sig) (r_mem : r ∈ rs.rules) (a : FunctionFreeAtom sig) : a ∈ r.body ++ r.head.flatten → (rs.mfaConstantMapping special_const).apply_function_free_atom a = a

The mfaConstantMapping is even the id on all rule atoms. (Constant mappings leave variables untouched.)

structure MfaObsolescenceCondition (sig : Signature) [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] extends LaxObsolescenceCondition sig : Type (max (max u_1 u_2) u_3)

A MfaObsolescenceCondition is simply a LaxObsolescenceCondition, i.e. besides the actual condition it only has subset monotonicity as its only condition.

• cond : PreTrigger sig → FactSet sig → Prop
• monotone {trg : PreTrigger sig} {A B : FactSet sig} : A ⊆ B → self.cond trg A → self.cond trg B

@[implicit_reducible]

instance instCoeMfaObsolescenceConditionLaxObsolescenceCondition {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] : Coe (MfaObsolescenceCondition sig) (LaxObsolescenceCondition sig)

Equations

• instCoeMfaObsolescenceConditionLaxObsolescenceCondition = { coe := fun (obs : MfaObsolescenceCondition sig) => { cond := obs.cond, monotone := ⋯ } }

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

Here we define what it means for a MfaObsolescenceCondition to block a ObsolescenceCondition. Essentially, we say that if the mfa obsolescence is fulfilled and the trigger is loaded, then also the real obsolescence condition is fulfilled. Before that, we filter trggers where already every head result occurs in in the mfa set of facts anyway. This is safe to do since applying these again would not make a difference. The necessesity for doing this comes from DeterministicSkolemObsolescence.blocks_each_obs. BlockingObsolescence.blocks_corresponding_obs works without.

Equations

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

def DeterministicSkolemObsolescence (sig : Signature) [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] : MfaObsolescenceCondition sig

A trigger fulfills DeterministicSkolemObsolescence if each of its derived heads is already in the fact set in question. Note that this captures the idea of replacing disjunctions with conjunctions, which is part of MFA. We do this nowhere explicitely, so disjunctions always remain in rules, but we implicitly treat them like conjunctions when necessary (like here).

Equations

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

theorem DeterministicSkolemObsolescence.blocks_each_obs {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (obs : ObsolescenceCondition sig) (special_const : sig.C) (rs : RuleSet sig) : (DeterministicSkolemObsolescence sig).blocks_obs obs rs special_const

DeterministicSkolemObsolescence has the blocks_obs property for each ObsolescenceCondition.

def Trigger.blocked_for_backtracking {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [GetFreshInhabitant sig.C] [Inhabited sig.C] {obs : LaxObsolescenceCondition sig} (trg : Trigger obs) (rl : RuleList sig) : Prop

A trigger is blocked for its own backtracking if it is obsolete for its own backtracking. Note that the backtracking always requires us to prove that Skolem function terms are well-formed, which is what the additional conditions are for.

Equations

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

def BlockingObsolescence {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [GetFreshInhabitant sig.C] [Inhabited sig.C] (obs : ObsolescenceCondition sig) (rs : RuleSet sig) : MfaObsolescenceCondition sig

A trigger fulfills BlockingObsolescence if the trigger with renamed-apart constants is blocked for its own backtracking. Note that BlockingObsolescence only depends on the trigger. The passed fact set is ignored.

Equations

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

theorem BlockingObsolescence.blocks_corresponding_obs {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [GetFreshInhabitant sig.C] [Inhabited sig.C] (obs : ObsolescenceCondition sig) (obs_propagates_under_const_mapping : obs.propagates_under_constant_mapping) (rs : RuleSet sig) (rs_finite : rs.rules.finite) (special_const : sig.C) : (BlockingObsolescence obs rs).blocks_obs obs rs special_const

BlockingObsolescence has the blocks_obs condition for the ObsolescenceCondition it was defined for.

theorem KnowledgeBase.parallelDeterminizedChase_result_eq_every_chase_branch_result {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (kb : KnowledgeBase sig) (det : kb.rules.isDeterministic) (cb : ChaseBranch (SkolemObsolescence sig) kb) : cb.result = parallelDeterminizedChase_result kb { cond := (DeterministicSkolemObsolescence sig).cond, monotone := ⋯ }

This result is not necessary for MFA-like conditions but still interesting, also as a sanity check: The result of every deterministic Skolem ChaseBranch is the same as the parallelDeterminizedChase_result.

def RuleSet.criticalInstance {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (rs : RuleSet sig) (finite : rs.rules.finite) (special_const : sig.C) : Database sig

The MFA-like conditions all start on a special database, called the "critical instance". We define this here. It consists of all facts that can be build from predicates in the rule set and constants from the ruleset plus a "special constant". Intuitively, this generalizes all possible databases.

Equations

• rs.criticalInstance finite special_const = ⟨fun (f : FunctionFreeFact sig) => f.predicate ∈ rs.predicates ∧ ∀ (t : sig.C), t ∈ f.terms → t = special_const ∨ t ∈ rs.constants, ⋯⟩

def RuleSet.mfaKb {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (rs : RuleSet sig) (finite : rs.rules.finite) (special_const : sig.C) : KnowledgeBase sig

The KnowledgeBase for the MFA-like checks consists of the rule set in question and the criticalInstance.

Equations

• rs.mfaKb finite special_const = { db := rs.criticalInstance finite special_const, rules := rs }

theorem RuleSet.mfaKb_db_constants {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (rs : RuleSet sig) (finite : rs.rules.finite) (special_const c : sig.C) : c ∈ (rs.mfaKb finite special_const).db.constants.val → c = special_const ∨ c ∈ rs.constants

Constants in the mfaKb are either the special constants or they come from the rule set.

def RuleSet.mfaSet {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (rs : RuleSet sig) (finite : rs.rules.finite) (special_const : sig.C) (obs : MfaObsolescenceCondition sig) : FactSet sig

The fact set computed in the MFA-like checks is the parallel determinized chase result (defined in a separete file) for the mfaKb.

Equations

• rs.mfaSet finite special_const obs = parallelDeterminizedChase_result (rs.mfaKb finite special_const) { cond := obs.cond, monotone := ⋯ }

theorem RuleSet.mfaSet_contains_every_chase_step_for_every_kb_except_for_facts_with_predicates_not_from_rs {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (rs : RuleSet sig) (finite : rs.rules.finite) (special_const : sig.C) (mfa_obs : MfaObsolescenceCondition sig) {db : Database sig} {obs : ObsolescenceCondition sig} : mfa_obs.blocks_obs obs rs special_const → ∀ (cb : ChaseBranch obs { db := db, rules := rs }) (node : cb.Node) (f : Fact sig), f.predicate ∈ rs.predicates → f ∈ node.val.facts → (rs.mfaConstantMapping special_const).toConstantMapping.apply_fact f ∈ rs.mfaSet finite special_const mfa_obs

We can map every possible ChaseBranch into the mfaSet by replacing all (non-ruleset) constants by the special constant. At least this is the intuition for this behemoth of a theorem statement.

theorem RuleSet.filtered_cb_result_subset_mfaSet {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (rs : RuleSet sig) (finite : rs.rules.finite) (special_const : sig.C) (mfa_obs : MfaObsolescenceCondition sig) {db : Database sig} {obs : ObsolescenceCondition sig} : mfa_obs.blocks_obs obs rs special_const → ∀ (cb : ChaseBranch obs { db := db, rules := rs }), ((rs.mfaConstantMapping special_const).toConstantMapping.apply_fact_set fun (f : Fact sig) => f.predicate ∈ rs.predicates ∧ f ∈ cb.result) ⊆ rs.mfaSet finite special_const mfa_obs

We can extend the result above to the whole result of the ChaseBranch.

theorem RuleSet.terminates_of_mfaSet_finite {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [Inhabited sig.C] (rs : RuleSet sig) (rs_finite : rs.rules.finite) (mfa_obs : MfaObsolescenceCondition sig) {obs : ObsolescenceCondition sig} : mfa_obs.blocks_obs obs rs default → Set.finite (rs.mfaSet rs_finite default mfa_obs) → rs.terminates obs

If the mfaSet is finite, then the rule set terminates. The argument is that if the mfaSet is finite and every ChaseBranch can be embedded into this set, then each of these ChaseBranches also needs to be finite. This is still a bit involved since we need to show that only finitely many terms can collapse to the same on in the mfaSet.

def RuleSet.isMfa {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [Inhabited sig.C] (rs : RuleSet sig) (finite : rs.rules.finite) (mfa_obs : MfaObsolescenceCondition sig) : Prop

A rule set isMfa if its mfaSet does not contain a cyclic term.

Equations

• rs.isMfa finite mfa_obs = ∀ (t : GroundTerm sig), t ∈ (rs.mfaSet finite default mfa_obs).terms → ¬PreGroundTerm.cyclic t.val = true

theorem RuleSet.terminates_of_isMfa {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [Inhabited sig.C] (rs : RuleSet sig) (rs_finite : rs.rules.finite) (mfa_obs : MfaObsolescenceCondition sig) {obs : ObsolescenceCondition sig} : mfa_obs.blocks_obs obs rs default → rs.isMfa rs_finite mfa_obs → rs.terminates obs

A rule set terminates if it isMfa. What mainly remains to be shown here is that only finitely many terms are non-cyclic.

theorem RuleSet.terminates_of_isMfa_with_DeterministicSkolemObsolescence {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [Inhabited sig.C] (rs : RuleSet sig) (rs_finite : rs.rules.finite) : rs.isMfa rs_finite (DeterministicSkolemObsolescence sig) → ∀ (obs : ObsolescenceCondition sig), rs.terminates obs

MFA correctness - If a rule set is MFA (isMfa with DeterministicSkolemObsolescence), then it terminates.

theorem RuleSet.terminates_of_isMfa_with_BlockingObsolescence {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [GetFreshInhabitant sig.C] [Inhabited sig.C] (rs : RuleSet sig) (rs_finite : rs.rules.finite) (obs : ObsolescenceCondition sig) (obs_propagates_under_const_mapping : obs.propagates_under_constant_mapping) : rs.isMfa rs_finite (BlockingObsolescence obs rs) → rs.terminates obs

DMFA/RMFA correctness - If a rule set is DMFA/RMFA or anything in between (isMfa with BlockingObsolescence), then it terminates for the respective ObsolescenceCondition.