Alternative Matches and the Chase

In this file, we relate alternative matches to ChaseDerivation and ChaseBranch. All of this considers the deterministic setting, i.e. only rule sets where each rule has exactly one head disjunct. One of the main result is result_isStrongCore_of_noAltMatch, which states that the result of a ChaseBranch without alternative matches is always a strong core.

def GroundTermMapping.is_alt_match_for_chase_derivation_and_fs {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [DecidableEq sig.P] {obs : ObsoletenessCondition sig} {rules : RuleSet sig} (h : GroundTermMapping sig) (cd : ChaseDerivation obs rules) (fs : FactSet sig) : Prop

A GroundTermMapping is an alternative for a ChaseDerivation and a FactSet if it is an alternative match into the fact set for the trigger is used to derive ChaseDerivation.next.

Equations

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

def ChaseDerivation.has_alt_match_for_next_and_fs {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [DecidableEq sig.P] {obs : ObsoletenessCondition sig} {rules : RuleSet sig} (cd : ChaseDerivation obs rules) (fs : FactSet sig) : Prop

A ChaseDerivation has an alternative match into a FactSet simply if there is a GroundTermMapping that is such an alternative match for ChaseDerivation.next.

Equations

• cd.has_alt_match_for_next_and_fs fs = ∃ (h : GroundTermMapping sig), h.is_alt_match_for_chase_derivation_and_fs cd fs

def ChaseDerivation.has_alt_match_for_fs {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [DecidableEq sig.P] {obs : ObsoletenessCondition sig} {rules : RuleSet sig} (cd : ChaseDerivation obs rules) (fs : FactSet sig) : Prop

More generally, a ChaseDerivation has an alternative match into a FactSet if one of its subderivations has an alternative match for ChaseDerivation.next (according to the above definition) into the fact set.

Equations

• cd.has_alt_match_for_fs fs = ∃ (cd2 : ChaseDerivation obs rules), cd2 <:+ cd ∧ cd2.has_alt_match_for_next_and_fs fs

def ChaseDerivation.has_alt_match {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [DecidableEq sig.P] {obs : ObsoletenessCondition sig} {rules : RuleSet sig} (cd : ChaseDerivation obs rules) : Prop

Finally, a ChaseDerivation has an alternative match, if it has an alternative match into its own result.

Equations

• cd.has_alt_match = cd.has_alt_match_for_fs cd.result

theorem ChaseBranch.result_isWeakCore_of_noAltMatch {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [DecidableEq sig.P] {obs : ObsoletenessCondition sig} {kb : KnowledgeBase sig} {cb : ChaseBranch obs kb} (det : kb.isDeterministic) : ¬cb.has_alt_match → cb.result.isWeakCore

If a ChaseBranch has no alternative match (into its own result), then the result is a weak core.

theorem ChaseBranch.non_id_endomorphism_of_altMatch {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [DecidableEq sig.P] {obs : ObsoletenessCondition sig} {kb : KnowledgeBase sig} {cb : ChaseBranch obs kb} (det : kb.isDeterministic) (altMatch : cb.has_alt_match) : ∃ (endo : GroundTermMapping sig), endo.isHomomorphism cb.result cb.result ∧ ∃ (t : GroundTerm sig), endo t ≠ t

If a ChaseBranch has an alternative match (into its own result), then there is an non-trivial endomorphism on the result, i.e. an endomorphism that is not the identity.

theorem ChaseBranch.altMatch_of_some_not_reaches_self {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [DecidableEq sig.P] {obs : ObsoletenessCondition sig} {kb : KnowledgeBase sig} (cb : ChaseBranch obs kb) (fs : FactSet sig) (h : GroundTermMapping sig) (hom_res : h.isHomomorphism cb.result fs) (hom_fs : h.isHomomorphism fs fs) (t : GroundTerm sig) (t_mem : t ∈ cb.result.terms) (t_not_reaches_self : ∀ (j : Nat), 1 ≤ j → h.repeat_hom j t ≠ t) : cb.has_alt_match_for_fs fs

This is more of a lemma quite technical unfortunately. Take a ChaseBranch, a FactSet and a homomorphism $h$ from the chase result into the fact set that is at the same time an endomorphism on the fact set. If there is a term $t$ in the chase result such that no non-zero repetition of $h$ maps $t$ to itself, then the chase branch must have an alternative match for the fact set. Intuitively this is because $t$ is apparently a redundant term.

theorem ChaseBranch.every_endo_surjective_of_noAltMatch {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [DecidableEq sig.P] {obs : ObsoletenessCondition sig} {kb : KnowledgeBase sig} (cb : ChaseBranch obs kb) : ¬cb.has_alt_match → ∀ (h : GroundTermMapping sig), h.isHomomorphism cb.result cb.result → Function.surjective_for_domain_and_image_set h cb.result.terms cb.result.terms

For a ChaseBranch without alternative match, every endomorphism on the result is surjective. This is shown by contradiction using altMatch_of_some_not_reaches_self.

theorem ChaseBranch.result_isStrongCore_of_noAltMatch {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [DecidableEq sig.P] {obs : ObsoletenessCondition sig} {kb : KnowledgeBase sig} (cb : ChaseBranch obs kb) (det : kb.isDeterministic) : ¬cb.has_alt_match → cb.result.isStrongCore

From result_isWeakCore_of_noAltMatch and every_endo_surjective_of_noAltMatch, we get that the result of a ChaseBranch without alternative matches is a strong core.

The following is a quite technical result, which is designed to act as a lemma for further theorems that we did not formalize yet. To give a teaser, there are related to interleaving the restricted and core chase, basically using the restricted chase as long as alternative matches can be avoided and only in the end falling back to computing the rest with the core chase.

Take a ChaseBranch and a FactSet $F$ that is a superset of the chase result. Furthermore assume that the chase branch has no alternative match in $F$. For every homomorphic subset of $F$, we know that it must still be a superset of the chase result. On a higher level, imagine that $F$ is some fact set that might be computed using a core chase that started on the previous chase result. Then by this result we know that the core computation of the core chase will never remove a term that was introduced by our initial restricted chase branch. Part of the proof again uses altMatch_of_some_not_reaches_self.

Personal note: When I was thinking about this theorem on paper, I ended up confusing myself again and again doubting if this even holds. Finally, I had enough of it and invested (a lot of) time to formalize this in Lean and get some peace of mind. Of course it still remains to show the theorems where this would actually be used.

theorem ChaseBranch.core_superset_of_chase_result {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [DecidableEq sig.P] {obs : ObsoletenessCondition sig} {kb : KnowledgeBase sig} (cb : ChaseBranch obs kb) (fs : FactSet sig) (fs_super : cb.result ⊆ fs) (noAltMatch : ¬cb.has_alt_match_for_fs fs) (sub_fs : FactSet sig) : sub_fs.homSubset fs → cb.result ⊆ sub_fs