Generate Branch in Tree Derivation from Sparse Sequence

The TreeDerivation already offers functionality for generating ChaseDerivation that correspond to branches in the tree. However, the generating function is forces to always yield an immediate child node, which is too restrictive for what we aim to do in the non-termination conditions like RPC. Instead, we get a generator that will always yield a node that occurs somewhere in the subtree of the previous node. We can then "fill in the gaps" to get the full branch. We do this by adjusting the generator function to fill in the blanks for us. This is a bit technical but hopefully abstracted away enough so that the internals are irrelevant outside of this file.

def TreeDerivation.generate_subderivation_from_sparse_of_total_generator {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {β : Type u} (td : TreeDerivation obs rules) (start : β) (generator : β → β) (mapper : β → td.NodeWithAddress) (next_is_succ : ∀ (b : β), mapper b ≺ mapper (generator b)) : ChaseDerivation obs rules

Given a sparse but total generator function, uses the original TreeDerivation.generate_subderivation function together with densify_generator and densify_mapper to generate a ChaseDerivation that corresponds to a branch in the tree. Since the generator function is total, the generated derivation is necessarily infinite.

Equations

• td.generate_subderivation_from_sparse_of_total_generator start generator mapper next_is_succ = TreeDerivation.generate_subderivation_from_sparse✝ td start (some ∘ generator) mapper ⋯ ⋯

theorem TreeDerivation.generate_subderivation_from_sparse_of_total_generator_mem_branches {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {β : Type u} {td : TreeDerivation obs rules} {start : β} {generator : β → β} {mapper : β → td.NodeWithAddress} {next_is_succ : ∀ (b : β), mapper b ≺ mapper (generator b)} (start_eq : mapper start = NodeWithAddress.root td) : td.generate_subderivation_from_sparse_of_total_generator start generator mapper next_is_succ ∈ td.branches

generate_subderivation_from_sparse_of_total_generator produces a tree branch because underneath it uses TreeDerivation.generate_subderivation, which already has this property.

theorem TreeDerivation.mem_generate_subderivation_from_sparse_of_total_generator_of_mem_original_generator {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {β : Type u} {td : TreeDerivation obs rules} {start : β} {generator : β → β} {mapper : β → td.NodeWithAddress} {next_is_succ : ∀ (b : β), mapper b ≺ mapper (generator b)} (b : β) : b ∈ InfiniteList.iterate start generator → (mapper b).node ∈ td.generate_subderivation_from_sparse_of_total_generator start generator mapper next_is_succ

Every node that is part of the original generator also occurs in the derivation produces by the densified version.