Extending arbitrary Homomorphisms along a Chase Branch

For some results about alternative matches, we need the ability to extend a homomorphisms from the chase node to the chase result into an endomorphism on the chase result (ChaseBranch.hom_for_node_extendable_to_result). We can do this in a step by step fashion along the chase. Although the result is sufficiently different, the construction, in spirit, is similar to the one used in the universality result (chaseTreeResultIsUniversal).

@[reducible, inline]

abbrev InductiveHomomorphismExtensionResult {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsoletenessCondition sig} {rules : RuleSet sig} (cd : ChaseDerivation obs rules) (h : GroundTermMapping sig) : Type (max 0 (max u_3 u_2) u_1)

To eventually create the extended homomorphism, we step-wise construct pairs of suffixes of the chase branch in question and GroundTermMappings such that mapping agrees with the initial one on the initial set of facts and the mapping is a homomorphism from the head of the current suffix into the chase result.

Equations

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

noncomputable def ChaseBranch.extend_hom_to_next_step_of_next_eq_some {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsoletenessCondition sig} {kb : KnowledgeBase sig} (cb : ChaseBranch obs kb) (det : kb.rules.isDeterministic) (cd : ChaseDerivation obs kb.rules) (suffix : cd <:+ cb.toChaseDerivation) (h : GroundTermMapping sig) (hom : h.isHomomorphism cd.head.facts cd.result) (next : ChaseNode obs kb.rules) (next_eq : cd.next = some next) : InductiveHomomorphismExtensionResult cd h

This function creates a new InductiveHomomorphismExtensionResult from an (unfolded) previous one given the fact that ChaseDerivation.next exists.

Equations

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

theorem ChaseBranch.node_is_next_in_extend_hom_to_next_step_next_eq_some {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsoletenessCondition sig} {kb : KnowledgeBase sig} {cb : ChaseBranch obs kb} {det : kb.rules.isDeterministic} {cd : ChaseDerivation obs kb.rules} {suffix : cd <:+ cb.toChaseDerivation} {h : GroundTermMapping sig} {hom : h.isHomomorphism cd.head.facts cd.result} {next : ChaseNode obs kb.rules} {next_eq : cd.next = some next} : (cb.extend_hom_to_next_step_of_next_eq_some det cd suffix h hom next next_eq).val.fst = cd.tail ⋯

The ChaseDerivation returned by extend_hom_to_next_step_of_next_eq_some is the ChaseDerivation.tail of the previous derivation.

theorem ChaseBranch.hom_extends_prev_in_extend_hom_to_next_step_of_next_eq_some {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsoletenessCondition sig} {kb : KnowledgeBase sig} {cb : ChaseBranch obs kb} {det : kb.rules.isDeterministic} {cd : ChaseDerivation obs kb.rules} {suffix : cd <:+ cb.toChaseDerivation} {h : GroundTermMapping sig} {hom : h.isHomomorphism cd.head.facts cd.result} {next : ChaseNode obs kb.rules} {next_eq : cd.next = some next} (t : GroundTerm sig) : t ∈ cd.head.facts.terms → (cb.extend_hom_to_next_step_of_next_eq_some det cd suffix h hom next next_eq).val.snd t = h t

The homomorphism returned by extend_hom_to_next_step_of_next_eq_some agrees with the previous one on all terms in the previous derivation head.

noncomputable def ChaseBranch.extend_hom_to_next_step {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsoletenessCondition sig} {kb : KnowledgeBase sig} (cb : ChaseBranch obs kb) (det : kb.rules.isDeterministic) (cd : ChaseDerivation obs kb.rules) (suffix : cd <:+ cb.toChaseDerivation) (h : GroundTermMapping sig) (prev_res : InductiveHomomorphismExtensionResult cd h) : Option (InductiveHomomorphismExtensionResult cd h)

We extend a given InductiveHomomorphismExtensionResult into the next one, mainly by calling extend_hom_to_next_step_of_next_eq_some. If ChaseDerivation.next is none, we also simply return none.

Equations

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

theorem ChaseBranch.node_is_next_in_extend_hom_to_next_step {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsoletenessCondition sig} {kb : KnowledgeBase sig} {cb : ChaseBranch obs kb} {det : kb.rules.isDeterministic} {cd : ChaseDerivation obs kb.rules} {suffix : cd <:+ cb.toChaseDerivation} {h : GroundTermMapping sig} {prev_res pair : InductiveHomomorphismExtensionResult cd h} (pair_mem : pair ∈ cb.extend_hom_to_next_step det cd suffix h prev_res) : pair.val.fst = prev_res.val.fst.tail ⋯

The ChaseDerivation returned by extend_hom_to_next_step is the ChaseDerivation.tail of the previous derivation.

theorem ChaseBranch.hom_extends_prev_in_extend_hom_to_next_step {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsoletenessCondition sig} {kb : KnowledgeBase sig} {cb : ChaseBranch obs kb} {det : kb.rules.isDeterministic} {cd : ChaseDerivation obs kb.rules} {suffix : cd <:+ cb.toChaseDerivation} {h : GroundTermMapping sig} {prev_res : InductiveHomomorphismExtensionResult cd h} (t : GroundTerm sig) : t ∈ prev_res.val.fst.head.facts.terms → ∀ (pair : InductiveHomomorphismExtensionResult cd h), pair ∈ cb.extend_hom_to_next_step det cd suffix h prev_res → pair.val.snd t = prev_res.val.snd t

The homomorphism returned by extend_hom_to_next_step agrees with the previous one on all terms in the previous derivation head.

theorem ChaseBranch.hom_for_node_extendable_to_result {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsoletenessCondition sig} {kb : KnowledgeBase sig} {cb : ChaseBranch obs kb} (det : kb.rules.isDeterministic) {node : ChaseNode obs kb.rules} (node_mem : node ∈ cb.toChaseDerivation) {h : GroundTermMapping sig} (hom : h.isHomomorphism node.facts cb.result) : ∃ (h' : GroundTermMapping sig), (∀ (t : GroundTerm sig), t ∈ node.facts.terms → h' t = h t) ∧ h'.isHomomorphism cb.result cb.result

Using extend_hom_to_next_step as a generator in PossiblyInfiniteList.generate we can create a possiblibly infinite list of homomorphisms that extend each other and all map to the result. We can combine them into a single function to have an endomorphism on the result. The idea is similar to the construction used in chaseTreeResultIsUniversal.