Docs / Syntax / Minimalist / Workspace / Merge / Internal

Internal Merge

import Linglib.Syntax.Minimalist.Workspace.Merge.Internal · namespace Minimalist.Merge

Source

Internal Merge (Proposition 1.4.2 of Marcolli, Chomsky and Berwick) is the composition M_{T/β,β} ∘ M_{β,1}. The unit stage selects a cut of T with crown {β}, giving the two-object workspace {β, T/β}, and External Merge then merges β with the quotient. When one cut extracts β, the composition yields node lbl {T/β, β} over every cut enumeration admitting Merge (mergeOpG_im_composition). At the deletion cuts of the book's Merge the quotient is the remainder with its unary vertex contracted (mergeOp_im_composition); at the pruning cuts that vertex stays, and at the trace cuts a trace takes the place of β (mergeOpC_im_composition).

Main results

Implementation notes

The composition theorems assume a single cut extracting β, as in the book's worked example. Proposition 1.4.2 does not; with several occurrences of β the unit stage is a sum over them (mergeOpUnitG_apply_singleton).

References

Declarations

On one tree T, the primitive term of the unit stage contributes β if T = β, and each cut with crown {β} contributes β beside its trunk.

theorem mergeOpUnitG_apply_singletonL52–69
{R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq (UnorderedTree α)] {cuts : UnorderedTree α → Multiset (UnorderedTree.Forest (UnorderedTree α) × UnorderedTree α)} (β T : UnorderedTree α) :
(mergeOpUnitG cuts β) (ConnesKreimer.of' {T}) = (if T = β then ConnesKreimer.of' {β} else 0) + (Multiset.map (fun (p : UnorderedTree.Forest (UnorderedTree α) × UnorderedTree α) => if p.1 = {β} then ConnesKreimer.of' {β} * ConnesKreimer.ofTree p.2 else 0) (cuts T)).sum

When T ≠ β and exactly one cut of T has crown {β}, the unit stage moves β to its own component beside that cut's trunk.

theorem mergeOpUnitG_apply_singleton_uniqueL71–87
{R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq (UnorderedTree α)] {cuts : UnorderedTree α → Multiset (UnorderedTree.Forest (UnorderedTree α) × UnorderedTree α)} (β T : UnorderedTree α) (p0 : UnorderedTree.Forest (UnorderedTree α) × UnorderedTree α) (h_filter : Multiset.filter (fun (p : UnorderedTree.Forest (UnorderedTree α) × UnorderedTree α) => p.1 = {β}) (cuts T) = {p0}) (hTβ : T ≠ β) :
(mergeOpUnitG cuts β) (ConnesKreimer.of' {T}) = ConnesKreimer.of' {β} * ConnesKreimer.ofTree p0.2

The unit stage commutes with a spectator component T that does not have β as a subtree.

theorem mergeOpUnitG_ofTree_mulL89–119
{R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq (UnorderedTree α)] {cuts : UnorderedTree α → Multiset (UnorderedTree.Forest (UnorderedTree α) × UnorderedTree α)} [IsMergeCuts cuts] {β T : UnorderedTree α} (hT : β ∉ T.subtrees) (w : ConnesKreimer R (UnorderedTree α)) :
(mergeOpUnitG cuts β) (ConnesKreimer.ofTree T * w) = ConnesKreimer.ofTree T * (mergeOpUnitG cuts β) w

With a residual workspace F̂ none of whose components has β as a subtree, the unit stage on {T} + F̂ splits β off T and leaves F̂ unchanged.

theorem mergeOpUnitG_apply_singleton_unique_residualL121–137
{R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq (UnorderedTree α)] {cuts : UnorderedTree α → Multiset (UnorderedTree.Forest (UnorderedTree α) × UnorderedTree α)} [IsMergeCuts cuts] (β T : UnorderedTree α) (p0 : UnorderedTree.Forest (UnorderedTree α) × UnorderedTree α) (h_filter : Multiset.filter (fun (p : UnorderedTree.Forest (UnorderedTree α) × UnorderedTree α) => p.1 = {β}) (cuts T) = {p0}) (hTβ : T ≠ β) {Fhat : UnorderedTree.Forest (UnorderedTree α)} (hF : ∀ U ∈ Fhat, β ∉ U.subtrees) :
(mergeOpUnitG cuts β) (ConnesKreimer.of' ({T} + Fhat)) = ConnesKreimer.of' ({β, p0.2} + Fhat)

Internal Merge as the composition M_{T/β,β} ∘ M_{β,1} over a cut enumeration admitting Merge, for β extracted from T by a single cut with trunk Q.

theorem mergeOpG_im_compositionL139–150
{R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq (UnorderedTree α)] {cuts : UnorderedTree α → Multiset (UnorderedTree.Forest (UnorderedTree α) × UnorderedTree α)} [IsMergeCuts cuts] (lbl : α) (β T Q : UnorderedTree α) (p0 : UnorderedTree.Forest (UnorderedTree α) × UnorderedTree α) (h_filter : Multiset.filter (fun (p : UnorderedTree.Forest (UnorderedTree α) × UnorderedTree α) => p.1 = {β}) (cuts T) = {p0}) (h_remainder : p0.2 = Q) (hTβ : T ≠ β) :
(mergeOpG cuts lbl Q β) ((mergeOpUnitG cuts β) (ConnesKreimer.of' {T})) = ConnesKreimer.of' {UnorderedTree.node lbl {Q, β}}

Internal Merge with a residual workspace F̂, none of whose components has β or the trunk Q as a subtree.

theorem mergeOpG_im_composition_residualL152–165
{R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq (UnorderedTree α)] {cuts : UnorderedTree α → Multiset (UnorderedTree.Forest (UnorderedTree α) × UnorderedTree α)} [IsMergeCuts cuts] (lbl : α) (β T Q : UnorderedTree α) (p0 : UnorderedTree.Forest (UnorderedTree α) × UnorderedTree α) (h_filter : Multiset.filter (fun (p : UnorderedTree.Forest (UnorderedTree α) × UnorderedTree α) => p.1 = {β}) (cuts T) = {p0}) (h_remainder : p0.2 = Q) (hTβ : T ≠ β) {Fhat : UnorderedTree.Forest (UnorderedTree α)} (hF : ∀ U ∈ Fhat, Disjoint {Q, β} U.subtrees) :
(mergeOpG cuts lbl Q β) ((mergeOpUnitG cuts β) (ConnesKreimer.of' ({T} + Fhat))) = ConnesKreimer.of' ({UnorderedTree.node lbl {Q, β}} + Fhat)

Internal Merge at the deletion cuts, for a mover β without unary vertices extracted by a single deletion cut with trunk Q.

theorem mergeOp_im_compositionL167–180
{R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq (UnorderedTree α)] (lbl : α) (β T Q : UnorderedTree α) (p0 : UnorderedTree.Forest (UnorderedTree α) × UnorderedTree α) (h_filter : Multiset.filter (fun (p : Multiset (UnorderedTree α) × UnorderedTree α) => p.1 = {β}) (ConnesKreimer.cutSummandsDN T) = {p0}) (h_remainder : p0.2 = Q) (hTβ : T ≠ β) (hβ : β.numUnary = 0) :
(mergeOp lbl Q β) ((mergeOpUnit β) (ConnesKreimer.of' {T})) = ConnesKreimer.of' {UnorderedTree.node lbl {Q, β}}

At the trace cuts Internal Merge merges the mover m with the trunk Q, which keeps a trace in its place.

theorem mergeOpC_im_compositionL184–195
{R : Type u_1} [CommSemiring R] {α : Type u_2} {β : Type u_3} [DecidableEq (UnorderedTree (α ⊕ β))] (τ : UnorderedTree (α ⊕ β) → β) (lbl : α ⊕ β) (m T Q : UnorderedTree (α ⊕ β)) (p0 : UnorderedTree.Forest (UnorderedTree (α ⊕ β)) × UnorderedTree (α ⊕ β)) (h_filter : Multiset.filter (fun (p : Multiset (UnorderedTree (α ⊕ β)) × UnorderedTree (α ⊕ β)) => p.1 = {m}) (ConnesKreimer.cutSummandsCN τ T) = {p0}) (h_remainder : p0.2 = Q) (hTm : T ≠ m) :
(mergeOpC τ lbl Q m) ((mergeOpUnitC τ m) (ConnesKreimer.of' {T})) = ConnesKreimer.of' {UnorderedTree.node lbl {Q, m}}