Docs / Syntax / Minimalist / Workspace / Merge / SyntacticObject

Merge on the syntactic-object carrier

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

Merge on the carrier is the bare binary node SyntacticObject.merge with root label Vertex.bare. External Merge of two objects is the algebraic Merge operator on the two-object workspace, the book's operator at the deletion cuts (mergeOp_node) and Merge at the trace cuts (mergeOpC_node).

Internal Merge goes through the trace cuts. The trace of an extracted term is a label of the leaf it contracts to (Marcolli et al. 2025 Definition 1.2.4), here compressed to a token by a trace encoder: a moved object leaves the trace of its head under the encoder (headTrace), by default the head by selection (traceEncoder). A uniquely accessible mover is extracted by exactly one trace cut, whose trunk is the remainder deleteAccessible mover current (cutSummandsCN_filter_mover), and Internal Merge is the composition M_{T/β,β} ∘ M_{β,1} of Marcolli et al. 2025 Proposition 1.4.2 (mergeOpC_im).

The pruning cuts cannot carry Internal Merge on syntactic objects. A syntactic object is a full binary tree, so it has an odd number of vertices (numNodes_odd); a pruning cut removing one syntactic object conserves vertices, so it leaves an even number, and the remainder is never a syntactic object (not_isSyntacticObject_of_mem_cutSummandsN): the mover's parent is left unary. The deletion cuts contract that vertex, so a deletion cut extracting one syntactic object leaves one (isSyntacticObject_of_mem_cutSummandsDN), and the book's Merge carries Internal Merge from a syntactic object to a syntactic object (mergeOp_im).

Main definitions

Minimalist.SyntacticObject.traceEncoder

Main results

Minimalist.SyntacticObject.mergeOp_node, mergeOpC_node: External Merge on the carrier.
Minimalist.SyntacticObject.cutSummandsCN_filter_mover: the trace cut extracting a uniquely accessible mover leaves deleteAccessible.
Minimalist.SyntacticObject.mergeOpUnitC_current, mergeOpC_im: Internal Merge on the carrier.
Minimalist.SyntacticObject.mergeOpC_node_residual, mergeOpC_im_residual: both beside a spectator workspace.
Minimalist.SyntacticObject.mergeOpC_of'_merge: on External Merge the Merge operator computes MERGE (Workspace.merge).
mergeOpC_im_of'_merge, mergeOpC_sideward2b_of'_merge, mergeOpC_sideward3b_of'_merge: on Internal Merge and Sideward Merge of types 2(b) and 3(b) it computes MERGE leaving traces (Workspace.mergeWith).
Minimalist.SyntacticObject.numNodes_odd: a syntactic object has an odd number of vertices.
Minimalist.SyntacticObject.not_isSyntacticObject_of_mem_cutSummandsN: no pruning cut removing one syntactic object from another leaves a syntactic object.
Minimalist.SyntacticObject.isSyntacticObject_of_mem_cutSummandsDN, Minimalist.SyntacticObject.mergeOp_im: every deletion cut removing at most one tree does, and Internal Merge at the deletion cuts yields a syntactic object.

TODO

Sideward Merge of type 3(a), two terms of one member, needs the uniqueness of the cut whose crown is both terms. Where one target contains the other, as in Countercyclic Merge, no admissible cut has the pair as its crown, so the operator should vanish there.

References

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

Declarations

External Merge on the carrier is the algebraic Merge with the bare root label on the two-object workspace.

theorem mergeOp_node L81–88

(S S' : SyntacticObject) :

(Merge.mergeOp Vertex.bare ↑S ↑S') (ConnesKreimer.of' {↑S, ↑S'}) = ConnesKreimer.of' {↑(S.merge S')}

External Merge on the carrier is the trace-cut Merge with the bare root label on the two-object workspace, for any trace encoder.

theorem mergeOpC_node L90–97

(τ : UnorderedTree Vertex → Option LexicalItem.Token) (S S' : SyntacticObject) :

(Merge.mergeOpC τ Vertex.bare ↑S ↑S') (ConnesKreimer.of' {↑S, ↑S'}) = ConnesKreimer.of' {↑(S.merge S')}

Internal Merge through the trace cuts

The trace encoder of derivations sends a tree to its head by selection.

def traceEncoder L101–102

(t : UnorderedTree Vertex) :

Option LexicalItem.Token

traceEncoder t = (Minimalist.selCheckN t).head

Used by cutSummandsCN_filter_mover, mergeOpUnitC_current, mergeOpC_im, mergeOpC_im_residual, mergeOpC_im_of'_merge, mergeOpC_sideward2b_of'_merge, mergeOpC_sideward3b_of'_merge

Used in Syntax/Minimalist/Derivation/Basic

A uniquely accessible mover that is not a trace is extracted by exactly one trace cut, whose trunk is the remainder deleteAccessible mover current.

theorem cutSummandsCN_filter_mover L106–115

{mover current : SyntacticObject} (hm : Sum.isLeft (↑mover).value = true) (h : Multiset.count mover current.terms = 1) (hne : current ≠ mover) :

Multiset.filter (fun (p : Multiset (UnorderedTree (Option LexicalItem.Token ⊕ Option LexicalItem.Token)) × UnorderedTree (Option LexicalItem.Token ⊕ Option LexicalItem.Token)) => p.1 = {↑mover}) (ConnesKreimer.cutSummandsCN traceEncoder ↑current) = {({↑mover}, ↑(mover.deleteAccessible current))}

Built from

The unit stage M_{β,1} on the current object splits off a uniquely accessible mover beside the remainder.

theorem mergeOpUnitC_current L117–128

{mover current : SyntacticObject} (hm : Sum.isLeft (↑mover).value = true) (h : Multiset.count mover current.terms = 1) (hne : current ≠ mover) :

(Merge.mergeOpUnitC traceEncoder ↑mover) (ConnesKreimer.of' {↑current}) = ConnesKreimer.of' {↑mover, ↑(mover.deleteAccessible current)}

Built from

Internal Merge of a uniquely accessible mover is the composition M_{T/β,β} ∘ M_{β,1} of trace-cut Merges (Marcolli et al. 2025 Proposition 1.4.2).

theorem mergeOpC_im L130–140

{mover current : SyntacticObject} (hm : Sum.isLeft (↑mover).value = true) (h : Multiset.count mover current.terms = 1) (hne : current ≠ mover) :

(Merge.mergeOpC traceEncoder Vertex.bare ↑(mover.deleteAccessible current) ↑mover) ((Merge.mergeOpUnitC traceEncoder ↑mover) (ConnesKreimer.of' {↑current})) = ConnesKreimer.of' {↑((mover.deleteAccessible current).merge mover)}

Built from

Merge beside a spectator workspace

External Merge on the carrier beside a spectator workspace none of whose components contains S or S'.

theorem mergeOpC_node_residual L153–162

(τ : UnorderedTree Vertex → Option LexicalItem.Token) (S S' : SyntacticObject) {W : Workspace} (hW : ∀ U ∈ W, S ∉ U.terms ∧ S' ∉ U.terms) :

(Merge.mergeOpC τ Vertex.bare ↑S ↑S') (ConnesKreimer.of' (Multiset.map Subtype.val ({S, S'} + W))) = ConnesKreimer.of' (Multiset.map Subtype.val ({S.merge S'} + W))

Internal Merge of a uniquely accessible mover beside a spectator workspace none of whose components contains the mover or the remainder.

theorem mergeOpC_im_residual L164–178

{mover current : SyntacticObject} (hm : Sum.isLeft (↑mover).value = true) (h : Multiset.count mover current.terms = 1) (hne : current ≠ mover) {W : Workspace} (hW : ∀ U ∈ W, mover.deleteAccessible current ∉ U.terms ∧ mover ∉ U.terms) :

(Merge.mergeOpC traceEncoder Vertex.bare ↑(mover.deleteAccessible current) ↑mover) ((Merge.mergeOpUnitC traceEncoder ↑mover) (ConnesKreimer.of' (Multiset.map Subtype.val ({current} + W)))) = ConnesKreimer.of' (Multiset.map Subtype.val ({(mover.deleteAccessible current).merge mover} + W))

Built from

MERGE computed by the Merge operator

External Merge: the Merge operator at the trace cuts computes MERGE on a workspace of which S and S' are members, when no other member contains them.

theorem mergeOpC_of'_merge L182–190

(τ : UnorderedTree Vertex → Option LexicalItem.Token) {S S' : SyntacticObject} {W : Workspace} (hle : {S, S'} ≤ W) (hW : ∀ U ∈ W - {S, S'}, S ∉ U.terms ∧ S' ∉ U.terms) :

(Merge.mergeOpC τ Vertex.bare ↑S ↑S') (ConnesKreimer.of' (Multiset.map Subtype.val W)) = ConnesKreimer.of' (Multiset.map Subtype.val (W.merge S S'))

Internal Merge (Marcolli et al. 2025 Proposition 1.4.2): the Merge operator at the trace cuts computes MERGE of a uniquely accessible mover with the member containing it, leaving the trace of its head.

theorem mergeOpC_im_of'_merge L192–204

(Merge.mergeOpC traceEncoder Vertex.bare ↑(mover.deleteAccessible current) ↑mover) ((Merge.mergeOpUnitC traceEncoder ↑mover) (ConnesKreimer.of' (Multiset.map Subtype.val ({current} + W)))) = ConnesKreimer.of' (Multiset.map Subtype.val (Workspace.mergeWith (fun (x : SyntacticObject) => x.headTrace) ({current} + W) mover current))

Built from

Sideward Merge of type 2(b) (Marcolli et al. 2025 Lemma 1.4.4): merging a member T with the only occurrence of a term S' of another member T', the Merge operator at the trace cuts computes MERGE leaving the trace of the head of S' in T', when S' is no term of T.

theorem mergeOpC_sideward2b_of'_merge L206–232

{T T' S' : SyntacticObject} {W : Workspace} (hS' : Sum.isLeft (↑S').value = true) (hc : Multiset.count S' T'.terms = 1) (hne : T' ≠ S') (hT : T ∉ T'.terms) (hS'T : S' ∉ T.terms) (hW : ∀ U ∈ W, T ∉ U.terms ∧ S' ∉ U.terms) :

(Merge.mergeOpC traceEncoder Vertex.bare ↑T ↑S') (ConnesKreimer.of' (Multiset.map Subtype.val ({T, T'} + W))) = ConnesKreimer.of' (Multiset.map Subtype.val (Workspace.mergeWith (fun (x : SyntacticObject) => x.headTrace) ({T, T'} + W) T S'))

Built from

Sideward Merge of type 3(b) (Marcolli et al. 2025 Lemma 1.4.4): merging the only occurrences of a term S of a member T and a term S' of another member T', the Merge operator at the trace cuts computes MERGE leaving the traces of their heads.

theorem mergeOpC_sideward3b_of'_merge L234–262

{T T' S S' : SyntacticObject} {W : Workspace} (hS : Sum.isLeft (↑S).value = true) (hS' : Sum.isLeft (↑S').value = true) (hcS : Multiset.count S T.terms = 1) (hcS' : Multiset.count S' T'.terms = 1) (hneS : T ≠ S) (hneS' : T' ≠ S') (hST' : S ∉ T'.terms) (hS'T : S' ∉ T.terms) (hW : ∀ U ∈ W, S ∉ U.terms ∧ S' ∉ U.terms) :

(Merge.mergeOpC traceEncoder Vertex.bare ↑S ↑S') (ConnesKreimer.of' (Multiset.map Subtype.val ({T, T'} + W))) = ConnesKreimer.of' (Multiset.map Subtype.val (Workspace.mergeWith (fun (x : SyntacticObject) => x.headTrace) ({T, T'} + W) S S'))

Built from

The pruning cuts on syntactic objects

A syntactic object, being a full binary tree, has an odd number of vertices.

theorem numNodes_odd L298–302

(s : SyntacticObject) :

Odd (↑s).numNodes

A pruning cut removing one syntactic object from another leaves no syntactic object, since the remainder has an even number of vertices.

theorem not_isSyntacticObject_of_mem_cutSummandsN L304–315

{T mover : SyntacticObject} {p : UnorderedTree.Forest (UnorderedTree Vertex) × UnorderedTree Vertex} (hp : p ∈ ConnesKreimer.cutSummandsN ↑T) (hcrown : p.1 = {↑mover}) :

¬IsSyntacticObject p.2

A deletion cut extracting at most one tree from a syntactic object leaves a syntactic object, the vertex the extraction leaves unary being contracted.

theorem isSyntacticObject_of_mem_cutSummandsDN L383–399

{T : SyntacticObject} {p : UnorderedTree.Forest (UnorderedTree Vertex) × UnorderedTree Vertex} (hp : p ∈ ConnesKreimer.cutSummandsDN ↑T) (hcard : Multiset.card p.1 ≤ 1) :

IsSyntacticObject p.2

Internal Merge at the deletion cuts carries a syntactic object to a syntactic object: when one deletion cut extracts the mover, its trunk is a syntactic object Q, and the composition M_{Q,β} ∘ M_{β,1} of Proposition 1.4.2 yields the one object merge Q mover.

theorem mergeOp_im L401–416

{current mover : SyntacticObject} {p0 : UnorderedTree.Forest (UnorderedTree Vertex) × UnorderedTree Vertex} (h : Multiset.filter (fun (p : Multiset (UnorderedTree Vertex) × UnorderedTree Vertex) => p.1 = {↑mover}) (ConnesKreimer.cutSummandsDN ↑current) = {p0}) (hne : current ≠ mover) :

∃ (Q : SyntacticObject), ↑Q = p0.2 ∧ (Merge.mergeOp Vertex.bare ↑Q ↑mover) ((Merge.mergeOpUnit ↑mover) (ConnesKreimer.of' {↑current})) = ConnesKreimer.of' {↑(Q.merge mover)}