Docs / Syntax / Minimalist / Workspace / Coproduct / TraceCut

Cuts that leave traces

import Linglib.Syntax.Minimalist.Workspace.Coproduct.TraceCut · namespace ConnesKreimer

Marcolli, Chomsky and Berwick's coproduct Δ^c cuts accessible terms out of a syntactic object and leaves a trace in place of each. On trees labelled α ⊕ β, the trace of a cut subtree t is a leaf inr (τ t) whose label is computed by a trace encoder τ, and cuts at trace leaves are forbidden, since a trace is not an accessible term. This is the admissible-cut enumeration cutSummandsG at the extraction policy extractC τ.

Main definitions

ConnesKreimer.traceLeaf: the trace leaf with a given label.
ConnesKreimer.extractC: the trace extraction policy.
ConnesKreimer.cutSummandsCP, ConnesKreimer.cutSummandsCN: the trace cut summands, and their descent to UnorderedTree.

Main results

ConnesKreimer.cutSummandsCN_filter_empty: the empty cut is the unique cut with empty crown.
ConnesKreimer.cutSummandsCN_filter_crown_eq_singleton: a lexical subtree occurring once is extracted by one cut, whose trunk replaces it by its trace.

References

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

traceLeaf — placeholder for a cut subtree

The trace-marker placeholder leaf carrying the encoded label b : β.

def traceLeaf L47–48

{α : Type u_1} {β : Type u_2} (b : β) :

RoseTree (α ⊕ β)

traceLeaf b = RoseTree.node (Sum.inr b) []

Used by extractC, extractC_inl

Δ^c extraction policy

The Δ^c extraction policy cuts a Sum.inl-rooted subtree t whole, leaving the trace leaf traceLeaf (τ t) in its slot, and never cuts a trace, which is not an accessible term (Marcolli et al. 2025, proof of Lemma 1.6.3, p. 65). Cutting traces would also break coassociativity, since iterated Δ^c would then leave traces of traces.

def extractC L52–59

{α : Type u_1} {β : Type u_2} (τ : RoseTree (α ⊕ β) → β) :

RoseTree (α ⊕ β) → Option (List (RoseTree (α ⊕ β)))

extractC τ (RoseTree.node (Sum.inl val) children) = some [traceLeaf (τ (RoseTree.node (Sum.inl val) children))]
extractC τ (RoseTree.node (Sum.inr val) children) = none

Built from

Used by extractC_inl, extractC_inr, cutSummandsCP, cutSummandsCP_def, cutSummandsCP_node, extractC_mkComp_invariant

Used in Syntax/Minimalist/Copy/Cut, Syntax/Minimalist/Workspace/Coproduct/DoubleCut

L61–64

L66–68

cutSummandsCP — Δ^c cut enumeration via the generic cutSummandsG

Defined as cutSummandsG (extractC τ). The generic-side simp lemmas (cutSummandsG_node, cutListSummandsG_*, augActionG_*) compose with extractC_inl/extractC_inr to give the Δ^c-specific reductions.

The Δ^c cut summands cut at non-trace subtrees, leaving trace placeholders, and skip cuts at trace leaves.

def cutSummandsCP L76–80

{α : Type u_1} {β : Type u_2} (τ : RoseTree (α ⊕ β) → β) :

RoseTree (α ⊕ β) → Multiset (Multiset (RoseTree (α ⊕ β)) × RoseTree (α ⊕ β))

cutSummandsCP τ = cutSummandsG (extractC τ)

Built from

Used by cutSummandsCP_def, cutSummandsCP_node, cutSummandsCP_proj_perm, cutSummandsCN, cutSummandsCN_mk

Used in Syntax/Minimalist/Workspace/Coproduct/DoubleCut

L82–83

L85–89

Descent to UnorderedTree

L131–139

L141–146

The UnorderedTree Δ^c cut summands, descended from cutSummandsCP via Quotient.lift using the descent invariance cutSummandsCP_proj_perm.

cutSummandsCN L148–156

noncomputable def ConnesKreimer.cutSummandsCN {α : Type u_1} {β : Type u_2} (τ : UnorderedTree (α ⊕ β) → β) :

UnorderedTree (α ⊕ β) → Multiset (Multiset (UnorderedTree (α ⊕ β)) × UnorderedTree (α ⊕ β))

cutSummandsCN τ = Quotient.lift (fun (T : RoseTree (α ⊕ β)) => Multiset.map projSummand (cutSummandsCP (τ ∘ UnorderedTree.mk) T)) ⋯

Built from

Instances ConnesKreimer.instIsAdmissibleCutsCN, Minimalist.Merge.instIsMergeCutsSumCutSummandsCN

Used by cutSummandsCN_mk, cutSummandsCN_filter_empty, zero_mem_cutSummandsCN, cutSummandsCN_mem_subtrees_of_mem_crown, cutSummandsCN_filter_crown_eq_singleton

Used in Syntax/Minimalist/Copy/Cut, Syntax/Minimalist/Workspace/Coproduct/CutFilterMap, Syntax/Minimalist/Workspace/Coproduct/Trace, Syntax/Minimalist/Workspace/Coproduct/TraceConservation, Syntax/Minimalist/Workspace/Merge/Basic and 7 more

L158–161

The empty cut (0, T) is the unique cut summand of cutSummandsCN τ T with empty crown.

theorem cutSummandsCN_filter_empty L163–174

{α : Type u_1} {β : Type u_2} (τ : UnorderedTree (α ⊕ β) → β) (T : UnorderedTree (α ⊕ β)) :

Multiset.filter (fun (p : Multiset (UnorderedTree (α ⊕ β)) × UnorderedTree (α ⊕ β)) => p.1.card = 0) (cutSummandsCN τ T) = {(0, T)}

Built from

L176–181

L183–195

A lexical subtree M occurring exactly once below the root of T is extracted by exactly one Δ^c cut, whose trunk is T with M replaced by its trace.

theorem cutSummandsCN_filter_crown_eq_singleton L197–224

{α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] (τ : UnorderedTree (α ⊕ β) → β) {M T : UnorderedTree (α ⊕ β)} (hM : M.value.isLeft = true) (hcount : Multiset.count M T.subtrees = 1) (hTM : T ≠ M) :

Multiset.filter (fun (p : Multiset (UnorderedTree (α ⊕ β)) × UnorderedTree (α ⊕ β)) => p.1 = {M}) (cutSummandsCN τ T) = {({M}, M.replace (UnorderedTree.leaf (Sum.inr (τ M))) T)}

Built from