Chase Tree Result is Universal Model Set

This whole file is dedicated to showing that the result of a ChaseTree is a universal model set. More precisely, we want to show the universality part as we have already shown in ChaseTree.result_models_kb that each element of the result is a model. So what exactly remains to be shown?

We aim to show that for a given ChaseTree for a KnowledgeBase and any model $M$ of the KnowledgeBase, we can pick a fact set $F$ from the result of the chase tree such that there is a homomorphism from $F$ to $M$. This result is shown in chaseTreeResultIsUniversal.

The proof works by step-wise construction of both a branch in the chase tree as well as a suitable homomorphism. The constructions builds both at the same time. One step of the construction is done by the hom_step function below, which calls hom_step_of_trg_ex for the heavy lifting. The base of the construction is simply an empty branch and the id mapping. In each step of the construction, we consider an InductiveHomomorphismResult, which we define to be a pair of a node in the chase tree and a GroundTermMapping such that the mapping is a homomorphism from the node into the model $M$.

In the proof of chaseTreeResultIsUniversal, we leverage the FiniteDegreeTree.generate_branch function with hom_step as the generator function. By that, with a bit of massage, we can easily show that the constructed branch is indeed a branch in the tree using FiniteDegreeTree.generate_branch_mem_branches. Besides that, all the homomorphisms from the individual steps need to be combined into a single function. The definition is not too hard and all relevant properties are also not too hard to show once we can establish that the homomorphisms for each step always extend the previous one.

@[reducible, inline]

abbrev InductiveHomomorphismResult {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsoletenessCondition sig} {kb : KnowledgeBase sig} (ct : ChaseTree obs kb) (m : FactSet sig) : Type (max 0 (max u_3 u_2) u_1)

The InductiveHomomorphismResult is used for the step-wise construction is forms the element that is the input and output of the generator function used in FiniteDegreeTree.generate_branch later. It consists of a node in the chase tree and a GroundTermMapping that is a homomorphism from the node to the target model. The generated branch is the chain of all the generated nodes.

Equations

• InductiveHomomorphismResult ct m = { pair : ct.NodeWithAddress × GroundTermMapping sig // pair.snd.isHomomorphism pair.fst.node.facts m }

noncomputable def hom_step_of_trg_ex {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsoletenessCondition sig} {kb : KnowledgeBase sig} (ct : ChaseTree obs kb) (m : FactSet sig) (m_is_model : m.modelsKb kb) (node : ct.NodeWithAddress) (prev_hom : GroundTermMapping sig) (prev_hom_is_homomorphism : prev_hom.isHomomorphism node.node.facts m) (trg_ex : exists_trigger_list obs kb.rules node.node node.subderivation.childNodes) : InductiveHomomorphismResult ct m

Consider any node in the chase tree together with a homomorphism from this node to the target model. Given that there is an active trigger for the node, we return one of its child nodes together with an extended homomorphism. How do we know that such a node and homomorphism exist? This is because the existing trigger is loaded for the target model but since it is a model, we can also show that it also needs to be satisfied for the model. The way in which the trigger is satisfied in the model dictates which child node we pick and how we define the homomorphisms for the fresh terms introduced by the trigger. This is already all that happens here but it is not quite trivial to show that the constructed GroundTermMapping is indeed a homomorphism.

Equations

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

theorem mem_childNodes_of_mem_hom_step_of_trg_ex {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsoletenessCondition sig} {kb : KnowledgeBase sig} {ct : ChaseTree obs kb} {m : FactSet sig} {m_is_model : m.modelsKb kb} {node : ct.NodeWithAddress} {prev_hom : GroundTermMapping sig} {prev_hom_is_homomorphism : prev_hom.isHomomorphism node.node.facts m} {trg_ex : exists_trigger_list obs kb.rules node.node node.subderivation.childNodes} : (hom_step_of_trg_ex ct m m_is_model node prev_hom prev_hom_is_homomorphism trg_ex).val.fst ∈ List.map (fun (c : node.subderivation.NodeWithAddress) => node.cast_for_new_root_node c) (TreeDerivation.NodeWithAddress.childNodes node.subderivation)

The node that we pick in hom_step_of_trg_ex is in the childNodes of the previous node. This is trivial.

theorem hom_extends_prev_in_hom_step_of_trg_ex {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsoletenessCondition sig} {kb : KnowledgeBase sig} {ct : ChaseTree obs kb} {m : FactSet sig} {m_is_model : m.modelsKb kb} {node : ct.NodeWithAddress} {prev_hom : GroundTermMapping sig} {prev_hom_is_homomorphism : prev_hom.isHomomorphism node.node.facts m} {trg_ex : exists_trigger_list obs kb.rules node.node node.subderivation.childNodes} (t : GroundTerm sig) : t ∈ node.node.facts.terms → prev_hom t = (hom_step_of_trg_ex ct m m_is_model node prev_hom prev_hom_is_homomorphism trg_ex).val.snd t

The homomorphisms that we construct in hom_step_of_trg_ex agrees with the previous one on all terms in the previous node. This is also trivial.

noncomputable def hom_step {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsoletenessCondition sig} {kb : KnowledgeBase sig} (ct : ChaseTree obs kb) (m : FactSet sig) (m_is_model : m.modelsKb kb) (prev_res : InductiveHomomorphismResult ct m) : Option (InductiveHomomorphismResult ct m)

When extending the InductiveHomomorphismResult from one step to the next, we do not necessarily know that a trigger is active for the current node. Indeed the chase might just have already finished. So we do a simple case distinction here and return an Option either with the result from hom_step_of_trg_ex or simply none.

Equations

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

theorem mem_childNodes_of_mem_hom_step {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsoletenessCondition sig} {kb : KnowledgeBase sig} {ct : ChaseTree obs kb} {m : FactSet sig} {m_is_model : m.modelsKb kb} {prev_res : InductiveHomomorphismResult ct m} (res : InductiveHomomorphismResult ct m) : res ∈ hom_step ct m m_is_model prev_res → res.val.fst ∈ List.map (fun (c : prev_res.val.fst.subderivation.NodeWithAddress) => prev_res.val.fst.cast_for_new_root_node c) (TreeDerivation.NodeWithAddress.childNodes prev_res.val.fst.subderivation)

If there is a new node returned by hom_step, then it is in the childNodes of the current node.

theorem childNodes_empty_of_hom_step_none {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsoletenessCondition sig} {kb : KnowledgeBase sig} {ct : ChaseTree obs kb} {m : FactSet sig} {m_is_model : m.modelsKb kb} {prev_res : InductiveHomomorphismResult ct m} : hom_step ct m m_is_model prev_res = none → TreeDerivation.NodeWithAddress.childNodes prev_res.val.fst.subderivation = []

If hom_step returns none, then the current node does not have any children.

theorem hom_extends_prev_in_hom_step {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsoletenessCondition sig} {kb : KnowledgeBase sig} {ct : ChaseTree obs kb} {m : FactSet sig} {m_is_model : m.modelsKb kb} {prev_res : InductiveHomomorphismResult ct m} (pair : InductiveHomomorphismResult ct m) : pair ∈ hom_step ct m m_is_model prev_res → ∀ (t : GroundTerm sig), t ∈ prev_res.val.fst.node.facts.terms → prev_res.val.snd t = pair.val.snd t

The homomorphism returns in hom_step agrees with the current one on all terms from the current node.

theorem chaseTreeResultIsUniversal {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsoletenessCondition sig} {kb : KnowledgeBase sig} (ct : ChaseTree obs kb) (m : FactSet sig) : m.modelsKb kb → ∃ (fs : FactSet sig), ∃ (h : GroundTermMapping sig), fs ∈ ct.result ∧ h.isHomomorphism fs m

As outlined at the very top of this file, we now use FiniteDegreeTree.generate_branch with the hom_step generator to obtain the branch in the tree that yields the result FactSet for which the combined GroundTermMappings form a homomorphism into the target model.