The deletion coproduct and the erasure of traces

Marcolli, Chomsky and Berwick extract accessible terms from a syntactic object with three coproducts, which differ in the remainder an extraction leaves. Δ^c contracts each extracted term to a trace leaf, Δ^ρ leaves the remainder of the admissible cut, and Δ^d deletes the term and contracts the vertices left with a single child. They relate the three by projections of the right channel: Π_{ρ,c} deletes the trace leaves, Π_{d,ρ} contracts the non-branching vertices, and Δ^d = (id ⊗ Π_{d,ρ}) ∘ Δ^ρ = (id ⊗ Π_{d,ρ} ∘ Π_{ρ,c}) ∘ Δ^c, displayed before their (1.3.10). Here Δ^d is defined by the first expression, and the second is proved for trees without traces.

Main definitions

• ConnesKreimer.eraseTraces: the projection that deletes every trace vertex.
• ConnesKreimer.cutSummandsDN: the deletion cuts, the pruning cuts with the unary vertices of each trunk contracted.
• ConnesKreimer.comulDAlgHomN: the deletion coproduct, which sums them (comulDAlgHomN_apply_ofTree, comulAlgHomNG_cutSummandsDN).

Main results

• ConnesKreimer.eraseTraces_comp_rename_inl: erasure is a retraction of the embedding of the trees without traces.
• ConnesKreimer.eraseTraces_comulCAlgHomN: on trees without traces, erasing the traces that the trace coproduct leaves gives the pruning coproduct.
• ConnesKreimer.contractUnary_eraseTraces_comulCAlgHomN: erasing them and contracting the unary vertices gives the deletion coproduct.
• ConnesKreimer.cutSummandsDN_numEdges: in a full binary tree, deleting one accessible term costs two accessible terms besides its own, the book's (1.6.7).

Implementation notes

• Trees without traces are UnorderedTree α and trees with traces are UnorderedTree (α ⊕ β), so the relations hold along the embedding rename (UnorderedTree.map Sum.inl). The left channel of Δ^c on an embedded tree is embedded and the right channel is not, which is why the projections act on the right channel alone.
• The book's Π_{d,ρ} takes a tree whose vertices have at most two children to the maximal binary tree obtained by contracting edges. Here it is UnorderedTree.contractUnary, on trees of any arity.
• Δ^d carries no Bialgebra structure: its coassociativity holds only up to the multiplicity of some terms (the book's Lemma 1.2.12).
• (1.6.7) extends to a cut extracting several terms only when no two of them are sisters. A cut extracting both children of a vertex leaves it a leaf, with nothing to contract, so the two cost one accessible term each (cutSummandsN_numUnary).

References

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