Sideward Merge

Sideward Merge is Merge M_{S,S'} where at least one of S, S' is an accessible term of a component of the workspace, other than in Internal Merge. Marcolli, Chomsky and Berwick distinguish three cases (their §1.4.1): in 2(b) S is a component and S' an accessible term of another component; in 3(a) both are accessible terms of one component; in 3(b) they are accessible terms of two different components. Lemmas 1.4.4 and 1.4.5 show that the Merge operator of Definition 1.3.4 realizes all three, so Merge alone does not rule them out.

Each case evaluates the Merge formula mergeOpG_apply_of' on the workspace. On a single tree the matching cuts are the cuts with crown {S, S'}, since the tree itself is a one-element crown. On two trees the hypotheses force each matching forest cut to take S from the first tree and S' from the second, so the sum factors through the two one-tree sums. A spectator workspace passes through unchanged (mergeOpG_of'_mul).

Main results

• Minimalist.Merge.mergeOpG_sideward_2b: a component merged with an accessible term of another component, beside the remainder of that component.
• Minimalist.Merge.mergeOpG_sideward_3a: two accessible terms of one component, beside its remainder after both are cut.
• Minimalist.Merge.mergeOpG_sideward_3b: accessible terms of two components, beside both remainders.

Implementation notes

The book states each lemma for the term that extracts the matching objects. With several occurrences Merge sums over them, as (1.3.11) does, so the results are sums over the cuts with the matching crown, and a workspace without one is sent to 0.

References

• [MCB25]

theorem Minimalist.Merge.mergeOpG_sideward_3a {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq (UnorderedTree α)] {cuts : UnorderedTree α → Multiset (UnorderedTree.Forest (UnorderedTree α) × UnorderedTree α)} (lbl : α) (S S' T : UnorderedTree α) : (mergeOpG cuts lbl S S') (ConnesKreimer.of' {T}) = ConnesKreimer.of' {UnorderedTree.node lbl {S, S'}} * (Multiset.map (fun (p : UnorderedTree.Forest (UnorderedTree α) × UnorderedTree α) => ConnesKreimer.ofTree p.2) (Multiset.filter (fun (x : UnorderedTree.Forest (UnorderedTree α) × UnorderedTree α) => x.1 = {S, S'}) (cuts T))).sum

Merge on a one-tree workspace grafts {S, S'} beside the remainder of each cut with crown {S, S'}, which is Sideward Merge of type 3(a) ([MCB25] Lemma 1.4.5).

theorem Minimalist.Merge.mergeOpG_sideward_2b {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq (UnorderedTree α)] {cuts : UnorderedTree α → Multiset (UnorderedTree.Forest (UnorderedTree α) × UnorderedTree α)} [IsMergeCuts cuts] (lbl : α) {T T' S' : UnorderedTree α} (hT : T ∉ T'.subtrees) (hS' : S' ≠ T') : (mergeOpG cuts lbl T S') (ConnesKreimer.of' {T, T'}) = ConnesKreimer.of' {UnorderedTree.node lbl {T, S'}} * (Multiset.map (fun (p : UnorderedTree.Forest (UnorderedTree α) × UnorderedTree α) => ConnesKreimer.ofTree p.2) (Multiset.filter (fun (x : UnorderedTree.Forest (UnorderedTree α) × UnorderedTree α) => x.1 = {S'}) (cuts T'))).sum

In Sideward Merge of type 2(b) ([MCB25] Lemma 1.4.4), a component T merged with a term S' of another component T' sits beside the remainder of each cut of T' with crown {S'}.

theorem Minimalist.Merge.mergeOpG_sideward_3b {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq (UnorderedTree α)] {cuts : UnorderedTree α → Multiset (UnorderedTree.Forest (UnorderedTree α) × UnorderedTree α)} [IsMergeCuts cuts] (lbl : α) {T T' S S' : UnorderedTree α} (hST : S ≠ T) (hS'T' : S' ≠ T') (hST' : S ∉ T'.subtrees) (hS'T : S' ∉ T.subtrees) : (mergeOpG cuts lbl S S') (ConnesKreimer.of' {T, T'}) = ConnesKreimer.of' {UnorderedTree.node lbl {S, S'}} * (Multiset.map (fun (p : UnorderedTree.Forest (UnorderedTree α) × UnorderedTree α) => ConnesKreimer.ofTree p.2) (Multiset.filter (fun (x : UnorderedTree.Forest (UnorderedTree α) × UnorderedTree α) => x.1 = {S}) (cuts T))).sum * (Multiset.map (fun (p : UnorderedTree.Forest (UnorderedTree α) × UnorderedTree α) => ConnesKreimer.ofTree p.2) (Multiset.filter (fun (x : UnorderedTree.Forest (UnorderedTree α) × UnorderedTree α) => x.1 = {S'}) (cuts T'))).sum

In Sideward Merge of type 3(b) ([MCB25] Lemma 1.4.4), terms S of T and S' of T' are merged beside the remainders of each pair of cuts with crowns {S} and {S'}.