The Merge operator on workspaces #
The Merge operator of Marcolli, Chomsky and Berwick (their Definition 1.3.4) acts on the workspace
algebra ConnesKreimer R (UnorderedTree α). For a pair S, S' of accessible terms,
M_{S,S'} = ⊔ ∘ (B ⊗ id) ∘ δ_{S,S'} ∘ Δ,
where Δ is a coproduct extracting accessible terms, δ_{S,S'} keeps the terms whose left
channel is the forest {S, S'} (Definition 1.3.1), B grafts that forest under a new root
(Definition 1.3.2), and ⊔ multiplies the two channels back into one workspace. Only Δ depends
on how accessible terms are cut out, so the operator is defined over an arbitrary cut enumeration
cuts (mergeOpG), with the pruning instance mergeOp and the trace instance mergeOpC. The
unit stage M_{β,1} of Internal Merge (Proposition 1.4.2) has no grafting step (mergeOpUnitG).
On a workspace F, Merge grafts {S, S'} beside the trunk of each forest cut of F whose crown
is {S, S'}, summed over all such cuts (mergeOpG_apply_of', the book's (1.3.11)). Each form of
Merge in their §1.4 is this sum on a particular workspace.
External, Internal and Sideward Merge are in Merge/External.lean, Merge/Internal.lean and
Merge/Sideward.lean; the Minimal-Search weighting is in Merge/MinimalSearch.lean.
Main definitions #
Minimalist.Merge.mergeOpG,mergeOp,mergeOpC: Merge over a cut enumeration, at the pruning cuts, and at the trace cuts.Minimalist.Merge.mergeOpUnitG,mergeOpUnit,mergeOpUnitC: the unit stageM_{β,1}.Minimalist.Merge.IsMergeCuts: cut enumerations whose nonempty crowns have fewer edges than their tree.
Main results #
Minimalist.Merge.mergeOpG_apply_of',mergeOpG_apply_of'_eq_sum: Merge on a workspace is a sum over its forest cuts, or over a choice of cut for each of its trees.Minimalist.Merge.mergeOpG_comm: Merge does not depend on the order of the pair.
Implementation notes #
Definition 1.3.4 uses the deletion coproduct Δ^d, which contracts the unary vertex a cut leaves.
mergeOp uses the pruning coproduct Δ^ρ, which keeps it. The two extract the same accessible
terms and differ only in the remainder, so the forest B grafts is the same.
References #
Cut enumerations that admit Merge #
A cut enumeration admits Merge when its crowns are subtrees with fewer edges in total than
their tree, and its only empty cut is the tree itself. The edge bound makes External Merge of
a pair exact (mergeOpG_pair); the other two let a spectator component pass through
(mergeOpG_ofTree_mul).
- crown_numEdges_lt {T : UnorderedTree α} {p : UnorderedTree.Forest (UnorderedTree α) × UnorderedTree α} : p ∈ cuts T → p.1 ≠ 0 → (Multiset.map UnorderedTree.numEdges p.1).sum < T.numEdges
- mem_subtrees_of_mem_crown {T : UnorderedTree α} {p : UnorderedTree.Forest (UnorderedTree α) × UnorderedTree α} {x : UnorderedTree α} : p ∈ cuts T → x ∈ p.1 → x ∈ T.subtrees
- filter_empty (T : UnorderedTree α) : Multiset.filter (fun (p : UnorderedTree.Forest (UnorderedTree α) × UnorderedTree α) => Multiset.card p.1 = 0) (cuts T) = {(0, T)}
Instances
No cut of an enumeration admitting Merge has its own tree in the crown.
No cut of an enumeration admitting Merge extracts the whole tree.
Every crown member of a cut in treeCutsG cuts T, the whole tree included, is a subtree of
T.
Products in the two channels #
The matching projections #
The projection onto the basis element F₀ keeps its coefficient and sends every other basis
element to zero.
Equations
- Minimalist.Merge.forestProj F₀ = ConnesKreimer.linearLift fun (F : UnorderedTree.Forest (UnorderedTree α)) => if F = F₀ then ConnesKreimer.of' F else 0
Instances For
The projection onto F₀ kills every product with a forest that does not fit inside F₀.
The matching projection γ_{S,S'} ([MCB25] Definition 1.3.1) is the
projection onto {S, S'}.
Equations
- Minimalist.Merge.gammaMatch S S' = Minimalist.Merge.forestProj {S, S'}
Instances For
The matching operator δ_{S,S'} = γ_{S,S'} ⊗ id acts on the left channel of a coproduct.
Equations
- Minimalist.Merge.deltaMatch S S' = TensorProduct.map (Minimalist.Merge.gammaMatch S S') LinearMap.id
Instances For
Grafting #
The grafting operator B at the pair S, S' sends the basis element {S, S'} to the tree
node lbl {S, S'} and every other basis element to zero. Merge applies it only after
δ_{S,S'}, so this restriction of [MCB25]'s B suffices.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The Merge operator #
The post-coproduct chain ⊔ ∘ (B ⊗ id) ∘ δ_{S,S'}, shared by every cut enumeration.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The Merge operator M_{S,S'} of [MCB25] Definition 1.3.4 at the
pruning coproduct, with root label lbl.
Equations
- Minimalist.Merge.mergeOp lbl S S' = Minimalist.Merge.mergePost lbl S S' ∘ₗ ConnesKreimer.comulAlgHomN.toLinearMap
Instances For
On a basis tensor of' F ⊗ r, the post-coproduct chain grafts F if it is {S, S'} and
vanishes otherwise.
γ_{S,S'} kills every product with a forest F that does not fit inside {S, S'}.
γ_{S,S'} kills every product with a tree other than S and S'.
The post-coproduct chain kills every term whose left channel carries a forest that does not
fit inside {S, S'}.
The post-coproduct chain commutes with right multiplication by a right-channel factor
1 ⊗ y, so a spectator workspace passes through it unchanged.
The unit stage M_{β,1} #
The first stage of Internal Merge (Proposition 1.4.2) moves an accessible term β to the left
channel and leaves T/β on the right. Its grafting step is the identity, since
B(β ⊔ 1) = M(β, 1) = β. It is not a Merge in its own right: it occurs only composed with
M_{T/β,β} ([MCB25] Remark 1.4.3).
The single-tree matching projection γ_{β,1} keeps the coefficient of the basis element
{β}.
Equations
Instances For
The matching operator δ_{β,1} = γ_{β,1} ⊗ id.
Equations
- Minimalist.Merge.deltaMatchSingle β = TensorProduct.map (Minimalist.Merge.gammaMatchSingle β) LinearMap.id
Instances For
The post-coproduct chain ⊔ ∘ δ_{β,1} of the unit stage.
Equations
- Minimalist.Merge.mergePostUnit β = LinearMap.mul' R (ConnesKreimer R (UnorderedTree α)) ∘ₗ Minimalist.Merge.deltaMatchSingle β
Instances For
The unit stage M_{β,1} at the pruning coproduct.
Equations
- Minimalist.Merge.mergeOpUnit β = Minimalist.Merge.mergePostUnit β ∘ₗ ConnesKreimer.comulAlgHomN.toLinearMap
Instances For
The unit chain kills every term whose left channel carries a forest that does not fit inside
{β}.
The unit chain commutes with right multiplication by a right-channel factor 1 ⊗ y.
Merge over a cut enumeration #
Merge M_{S,S'} over a cut enumeration cuts, whose coproduct is comulAlgHomNG cuts.
Equations
- Minimalist.Merge.mergeOpG cuts lbl S S' = Minimalist.Merge.mergePost lbl S S' ∘ₗ (ConnesKreimer.comulAlgHomNG cuts).toLinearMap
Instances For
The unit stage M_{β,1} over a cut enumeration cuts.
Equations
- Minimalist.Merge.mergeOpUnitG cuts β = Minimalist.Merge.mergePostUnit β ∘ₗ (ConnesKreimer.comulAlgHomNG cuts).toLinearMap
Instances For
Merge on a workspace F grafts {S, S'} beside the trunk of each forest cut of F with crown
{S, S'} ([MCB25] (1.3.11)).
Merge on a workspace F is a sum of workspaces, one for each choice of a cut of each tree of
F whose crowns together are {S, S'}.
The unit stage on a workspace F is a sum of workspaces, one for each choice of a cut of each
tree of F whose crowns together are {β}.
Merge does not depend on the order of the pair.
The unit stage vanishes on the empty workspace, which has no β to extract.
Merge at the trace cuts #
The trace Merge operator is Merge at the trace cuts cutSummandsCN τ, whose trunks carry a
trace leaf at each cut site.
Equations
- Minimalist.Merge.mergeOpC τ lbl S S' = Minimalist.Merge.mergeOpG (ConnesKreimer.cutSummandsCN τ) lbl S S'
Instances For
The unit stage M_{S,1} at the trace cuts cutSummandsCN τ.