Obsoleteness (Conditions)

For the chase, we need to be able to define when a trigger should not be applied even though it might be loaded. In such a case (even when not loaded), we say that the trigger is "obsolete". We make this decision based on a given PreTrigger and a FactSet. Different chase variants use different notions of obsoleteness. For example the restricted (aka. standard) chase says that a trigger is obsolete when it is satisfied. On the other hand, the Skolem chase says that a trigger is obsolete when its excat result is already present. We aim to capture both of these notions and everything in-between using a generic ObsoletenessCondition that conveys the necessary properties.

The condition itself is a function taking a PreTrigger and a FactSet returning a Prop indicating if the trigger is obsolete for the fact set or not. Then, we require 4 conditions:

1. The condition is subset monotone. That is, if a trigger is obsolete for a fact set, it is also obsolete for all supersets.
2. If a trigger is obsolete then it is also satisfied.
3. If the exact trigger result already occurs in the fact set, then the trigger is obsolete.
4. Equivalent triggers are obsolete on exactly the same fact sets.

RestrictedObsoleteness and SkolemObsoleteness are the two extremes of what is allowed according to these conditions, SkolemObsoleteness being the most liberal and RestrictedObsoleteness being, quite expectedly, the most restricted.

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

LaxObsoletenessCondition is a more liberal version of ObsoletenessCondition enforcing only subset monotonicity (i.e. condition 1 above). We use such a more liberal condition for MFA later. For the most part, you can completely ignore that this exists and only consider ObsoletenessConditions instead.

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

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

An ObsoletenessCondition is a function from PreTrigger and FactSet into Prop with the 4 conditions mentioned above.

• cond : PreTrigger sig → FactSet sig → Prop
• monotone {trg : PreTrigger sig} {A B : FactSet sig} : A ⊆ B → self.cond trg A → self.cond trg B
• cond_implies_trg_is_satisfied {trg : PreTrigger sig} {fs : FactSet sig} : self.cond trg fs → trg.satisfied fs
• contains_trg_result_implies_cond {trg : PreTrigger sig} {fs : Set (Fact sig)} (disj_index : Fin trg.mapped_head.length) : trg.mapped_head[↑disj_index].toSet ⊆ fs → self.cond trg fs
• preserved_under_equiv {trg trg2 : PreTrigger sig} {fs : FactSet sig} : trg.equiv trg2 → (self.cond trg fs ↔ self.cond trg2 fs)

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

Equations

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

SpecificConditions

We briefly define the ObsoletenessConditions for Skolem and restricted chase to show that these indeed have the 4 necessary properties. However, most definitions are still expressed in terms of the generic ObsoletenessCondition so the specific ones are rarely used throughout the code; only when results indeed do not hold for the generic case but only specific obsoleteness conditions.

def SkolemObsoleteness (sig : Signature) [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] : ObsoletenessCondition sig

Obsoleteness for the Skolem chase is indeed a ObsoletenessCondition, i.e. it has all 4 properties. According to this condition, a trigger is obsolete if its exact result, for one of the head disjuncts, already occurs in the fact set.

Equations

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

def RestrictedObsoleteness (sig : Signature) [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] : ObsoletenessCondition sig

Obsoleteness for the restricted chase is indeed a ObsoletenessCondition, i.e. it has all 4 properties. According to this condition, a trigger is obsolete if it is satisfied.

Equations

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

(Proper) Triggers

A Trigger is a PreTrigger that has a fixed obsoleteness condition. We say that a Trigger is active if it is loaded and not obsolete.

SkolemTrigger and RestrictedTrigger are just defined as examples.

structure Trigger {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (obsolete : LaxObsoletenessCondition sig) extends PreTrigger sig : Type (max (max u_1 u_2) u_3)

• rule : Rule sig
• subs : GroundSubstitution sig

def SkolemTrigger {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] : Type (max (max u_1 u_2) u_3)

Equations

• SkolemTrigger = Trigger { cond := (SkolemObsoleteness sig).cond, monotone := ⋯ }

def RestrictedTrigger {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] : Type (max (max u_1 u_2) u_3)

Equations

• RestrictedTrigger = Trigger { cond := (RestrictedObsoleteness sig).cond, monotone := ⋯ }

instance instCoeOutTriggerPreTrigger {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : LaxObsoletenessCondition sig} : CoeOut (Trigger obs) (PreTrigger sig)

Equations

• instCoeOutTriggerPreTrigger = { coe := fun (trigger : Trigger obs) => trigger.toPreTrigger }

def Trigger.active {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : LaxObsoletenessCondition sig} (trg : Trigger obs) (F : FactSet sig) : Prop

Equations

• trg.active F = (trg.loaded F ∧ ¬obs.cond trg.toPreTrigger F)