Obsolescence (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 obsolescence. 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 ObsolescenceCondition 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.

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

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

LaxObsolescenceCondition is a more liberal version of ObsolescenceCondition 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 ObsolescenceConditions 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 ObsolescenceCondition (sig : Signature) [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] extends LaxObsolescenceCondition sig : Type (max (max u_1 u_2) u_3)

An ObsolescenceCondition 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)

@[implicit_reducible]

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

Equations

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

SpecificConditions

We briefly define the ObsolescenceConditions 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 ObsolescenceCondition so the specific ones are rarely used throughout the code; only when results indeed do not hold for the generic case but only specific obsolescence conditions.

def SkolemObsolescence (sig : Signature) [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] : ObsolescenceCondition sig

Obsolescence for the Skolem chase is indeed a ObsolescenceCondition, 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 RestrictedObsolescence (sig : Signature) [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] : ObsolescenceCondition sig

Obsolescence for the restricted chase is indeed a ObsolescenceCondition, 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 obsolescence 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 : LaxObsolescenceCondition 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 := (SkolemObsolescence 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 := (RestrictedObsolescence sig).cond, monotone := ⋯ }

@[implicit_reducible]

instance instCoeOutTriggerPreTrigger {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : LaxObsolescenceCondition 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 : LaxObsolescenceCondition sig} (trg : Trigger obs) (F : FactSet sig) : Prop

Equations

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