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), Disjunctive MFA (DMFA) and Restricted MFA (RMFA) 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 SkolemObsoleteness for the ObsoletenessCondition. But SkolemObsoleteness is actually the "most non-terminating" of our ObsoletenessConditions so we really are able to show that MFA guarantees termination no matter which ObsoletenessCondition we choose. See terminates_of_isMfa_with_DeterministicSkolemObsoleteness. 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 MfaObsoletenessCondition. So what we call MFA here is really isMfa with the DeterministicSkolemObsoleteness.

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 ObsoletenessCondition (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 BlockingObsoleteness for the MfaObsoletenessCondition in isMfa. Blocking is very similar for DMFA and RMFA and essentially only differs in the ObsoletenessCondition that for DMFA would be SkolemObsoleteness and for RMFA would be RestrictedObsoleteness. So what we do is simple: BlockingObsoleteness is simply defined taking a ObsoletenessCondition condition as a parameter. Thereby we obtain an MFA-like condition for any ObsoletenessCondition that one can imagine. So we can express DMFA, RMFA, and everything in-between. We show in terminates_of_isMfa_with_BlockingObsoleteness that isMfa with any such BlockingObsoleteness guarantees termination.

Our Framework

Despite the differences between MFA and DMFA/RMFA, you may realize that terminates_of_isMfa_with_DeterministicSkolemObsoleteness and terminates_of_isMfa_with_BlockingObsoleteness essentially use the same proof, namely they just call terminates_of_isMfa. This result is generic over all possible MfaObsoletenessConditions and just demands that the given MfaObsoletenessCondition has the blocks_obs property with respect to the target ObsoletenessCondition. For example, the DeterministicSkolemObsoleteness used for (the original) MFA has the blocks_obs property with respect to all ObsoletenessConditions and the BlockingObsoleteness for a given ObsoletenessCondition $o$ has the blocks_obs property with respect to $o$. Of course, this is something we need to prove and we do this in DeterministicSkolemObsoleteness.blocks_each_obs and BlockingObsoleteness.blocks_corresponding_obs, respectively.

How to actually check if a trigger is blocked?

The definition of BlockingObsoleteness and also the proof of BlockingObsoleteness.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 MfaObsoletenessCondition (sig : Signature) [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] extends LaxObsoletenessCondition sig : Type (max (max u_1 u_2) u_3)

A MfaObsoletenessCondition is simply a LaxObsoletenessCondition, 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

instance instCoeMfaObsoletenessConditionLaxObsoletenessCondition {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] : Coe (MfaObsoletenessCondition sig) (LaxObsoletenessCondition sig)

Equations

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

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

Here we define what it means for a MfaObsoletenessCondition to block a ObsoletenessCondition. Essentially, we say that if the mfa obsoleteness is fulfilled and the trigger is loaded, then also the real obsoleteness 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 DeterministicSkolemObsoleteness.blocks_obs. BlockingObsoleteness.blocks_obs works without.

Equations

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

def DeterministicSkolemObsoleteness (sig : Signature) [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] : MfaObsoletenessCondition sig

A trigger fulfills DeterministicSkolemObsoleteness 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 DeterministicSkolemObsoleteness.blocks_each_obs {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (obs : ObsoletenessCondition sig) (special_const : sig.C) (rs : RuleSet sig) : (DeterministicSkolemObsoleteness sig).blocks_obs obs rs special_const

DeterministicSkolemObsoleteness has the blocks_obs property for each ObsoletenessCondition.

def Trigger.blocked_for_backtracking {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [GetFreshInhabitant sig.C] [Inhabited sig.C] {obs : LaxObsoletenessCondition 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 BlockingObsoleteness {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [GetFreshInhabitant sig.C] [Inhabited sig.C] (obs : ObsoletenessCondition sig) (rs : RuleSet sig) : MfaObsoletenessCondition sig

A trigger fulfills BlockingObsoleteness if the trigger with renamed-apart constants is blocked for its own backtracking. Note that BlockingObsoleteness 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 BlockingObsoleteness.blocks_corresponding_obs {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [GetFreshInhabitant sig.C] [Inhabited sig.C] (obs : ObsoletenessCondition sig) (obs_propagates_under_const_mapping : obs.propagates_under_constant_mapping) (rs : RuleSet sig) (rs_finite : rs.rules.finite) (special_const : sig.C) : (BlockingObsoleteness obs rs).blocks_obs obs rs special_const

BlockingObsoleteness has the blocks_obs condition for the ObsoletenessCondition 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 (SkolemObsoleteness sig) kb) : cb.result = parallelDeterminizedChase_result kb { cond := (DeterministicSkolemObsoleteness 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 : MfaObsoletenessCondition 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 : MfaObsoletenessCondition sig) {db : Database sig} {obs : ObsoletenessCondition 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 : MfaObsoletenessCondition sig) {db : Database sig} {obs : ObsoletenessCondition 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 : MfaObsoletenessCondition sig) {obs : ObsoletenessCondition 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 : MfaObsoletenessCondition sig) : Prop

A rule set isMfa if its mfsSet 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 : MfaObsoletenessCondition sig) {obs : ObsoletenessCondition 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_DeterministicSkolemObsoleteness {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 (DeterministicSkolemObsoleteness sig) → ∀ (obs : ObsoletenessCondition sig), rs.terminates obs

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

theorem RuleSet.terminates_of_isMfa_with_BlockingObsoleteness {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 : ObsoletenessCondition sig) (obs_propagates_under_const_mapping : obs.propagates_under_constant_mapping) : rs.isMfa rs_finite (BlockingObsoleteness obs rs) → rs.terminates obs

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