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). The book's Δ is the deletion coproduct Δ^d, and mergeOp is Merge at the deletion cuts; mergeOpC is Merge at the trace cuts. 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 deletion cuts, and at the trace cuts.
• Minimalist.Merge.mergeOpUnitG, mergeOpUnit, mergeOpUnitC: the unit stage M_{β,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.
• Minimalist.Merge.mergeOp_eq_comp_comulAlgHomN: Merge at Δ^d through the pruning coproduct, the book's (1.3.10).
• Minimalist.Merge.mergeOp_eq_rename_contractUnary_comp, mergeOpUnit_eq_rename_contractUnary_comp: on objects without unary vertices, Merge at the deletion cuts is Merge at the pruning cuts followed by contracting unary vertices.

Implementation notes

Definition 1.3.4 fixes the deletion coproduct Δ^d, which contracts the unary vertex a cut leaves, and mergeOp is Merge at the deletion cuts. The pruning coproduct Δ^ρ keeps that vertex. The two extract the same accessible terms, but ⊔ multiplies the remainder into the result, so Merge at the pruning cuts (mergeOpG cutSummandsN) is not the book's operator: its Internal Merge leaves a unary vertex, which no syntactic object has. The book writes (1.3.7) through Δ^ρ only with the right channel contracted after the matching (mergeOp_eq_comp_comulAlgHomN).

The deletion cuts do not admit Merge in the sense of IsMergeCuts: on a tree with a unary vertex the trunk of the empty cut is the contracted tree, not the tree. The book's objects are binary trees, which have none, and on them mergeOp is Merge at the pruning cuts followed by the contraction (mergeOp_eq_rename_contractUnary_comp).

References

• Marcolli et al. 2025, Mathematical Structure of Syntactic Merge: An Algebraic Model for Generative Linguistics formalized