Docs / Syntax / Minimalist / Copy / FormCopy

Form Copy

import Linglib.Syntax.Minimalist.Copy.FormCopy · namespace Minimalist.SyntacticObject

Two inscriptions of a syntactic object are structurally identical when they coincide once the identity of their tokens is forgotten. By default structurally identical inscriptions are repetitions, each interpreted on its own, as the two inscriptions of many people in many people praised many people. Form Copy assigns the copy relation to such a pair when one c-commands the other, and copies are interpreted as one element, as in the passive many people were praised. Form Copy builds no structure: it is a relation on the inscriptions of an object.

Internal Merge leaves a copy in this sense, one object at two positions. Obligatory control is Form Copy between an inscription merged into the controlling verb's theta position and a repetition merged independently as the embedded subject, so that at Transfer control and raising present the same configuration. Marcolli, Chomsky and Berwick model Form Copy as the restriction of the operad action of Merge to a diagonal, the inputs at the identified positions being one object, so that the coproduct extracts identified copies only together.

Main definitions

SyntacticObject.erase: the tree of lexical items an object inscribes, forgetting its tokens
SyntacticObject.StructurallyIdentical: two inscriptions with one erasure
SyntacticObject.IsRepetition: structurally identical inscriptions that are distinct objects
SyntacticObject.renumber: an inscription of an object from fresh tokens
SyntacticObject.copyRel: the copy relation Form Copy assigns in an object
SyntacticObject.HasDistinctItems: no two tokens of an object inscribe one lexical item

Main results

SyntacticObject.StructurallyIdentical.merge: structural identity is a congruence for Merge
SyntacticObject.mk_mem_copyRel_merge: Form Copy relates an object merged with a term to every structurally identical inscription inside that term
SyntacticObject.self_mem_copyRel_merge_iff: the copy Internal Merge leaves is related to its antecedent, unless the whole object moves
SyntacticObject.structurallyIdentical_renumber: a fresh inscription is structurally identical to the original
SyntacticObject.copyRel_subset_id: in an object whose tokens inscribe distinct items, Form Copy relates each inscription only to itself

Implementation notes

Syntactic objects are values, so a copy is one object at two vertices and a repetition two objects with one erasure. Form Copy applies at the phase level, and the Phase Impenetrability Condition bounds its reach further; that timing is not modelled.

TODO

The modified coproduct on the diagonal, whose coassociativity Marcolli, Chomsky and Berwick sketch through a Hopf algebra of graphs, and the deletion of the lower copy at externalization.

References

Chomsky et al. 2023, Merge and the Strong Minimalist Thesis
Marcolli et al. 2025, Mathematical Structure of Syntactic Merge: An Algebraic Model for Generative Linguistics formalized

Structural identity

The tree of lexical items and traces an object inscribes, forgetting which token fills each leaf.

def erase L71–74

(s : SyntacticObject) :

UnorderedTree (Option LexicalItem ⊕ Option LexicalItem)

s.erase = UnorderedTree.map (Sum.map (Option.map Minimalist.LexicalItem.Token.item) (Option.map Minimalist.LexicalItem.Token.item)) ↑s

Used by erase_leaf, erase_trace, erase_traceOf, erase_merge, StructurallyIdentical, erase_map

Two inscriptions are structurally identical when they coincide once token identity is forgotten.

def StructurallyIdentical L95–97

(x y : SyntacticObject) :

Prop

x.StructurallyIdentical y = (x.erase = y.erase)

Built from

Used by instDecidableRelTokenStructurallyIdentical, structurallyIdentical_equivalence, StructurallyIdentical.refl, StructurallyIdentical.symm, StructurallyIdentical.trans, StructurallyIdentical.merge, StructurallyIdentical.numNodes_eq, IsRepetition, instDecidableRelTokenIsRepetition, structurallyIdentical_renumber, copyRel, mem_copyRel, instDecidableMemProdTokenSetRelCopyRel, mk_mem_copyRel_merge, StructurallyIdentical.eq_of_mem_terms

Used in Manzini2026

Structural identity is a congruence for Merge.

theorem StructurallyIdentical.merge L115–119

{l r l' r' : SyntacticObject} (hl : l.StructurallyIdentical l') (hr : r.StructurallyIdentical r') :

(l.merge r).StructurallyIdentical (l'.merge r')

Built from

L121–123

Two inscriptions are repetitions when they are structurally identical but distinct objects, built from different tokens: the default relation between identical inscriptions.

def IsRepetition L125–127

(x y : SyntacticObject) :

Prop

x.IsRepetition y = (x.StructurallyIdentical y ∧ x ≠ y)

Built from

Used by instDecidableRelTokenIsRepetition

Used in Landau2024b, MarcolliChomskyBerwick2025

L129

Fresh inscriptions

L135–140

The inscription of s from fresh tokens, each index raised by k, as External Merge introduces a second inscription of an object.

def renumber L142–145

(k : ℕ) :

SyntacticObject → SyntacticObject

renumber k = map fun (t : Minimalist.LexicalItem.Token) => { item := t.item, id := t.id + k }

Used by structurallyIdentical_renumber

Used in Landau2024b, Manzini2026, MarcolliChomskyBerwick2025

A renumbered inscription is structurally identical to the original.

theorem structurallyIdentical_renumber L147–150

(k : ℕ) (s : SyntacticObject) :

s.StructurallyIdentical (renumber k s)

Built from ,

The copy relation

The copy relation Form Copy assigns in s holds of a pair of structurally identical inscriptions, the first c-commanding the second.

def copyRel L154–157

(s : SyntacticObject) :

SetRel SyntacticObject SyntacticObject

s.copyRel = {p : Minimalist.SyntacticObject × Minimalist.SyntacticObject | s.CCommands p.1 p.2 ∧ p.1.StructurallyIdentical p.2}

Built from

Used by mem_copyRel, instDecidableMemProdTokenSetRelCopyRel, mk_mem_copyRel_merge, self_mem_copyRel_merge, self_mem_copyRel_merge_iff, copyRel_subset_id

Used in Syntax/Minimalist/Copy/Chain, Syntax/Minimalist/Copy/Replay, Landau2024b, Manzini2026, MarcolliChomskyBerwick2025

L159–161

L163–165

Form Copy relates an object merged with a term to every structurally identical inscription inside that term: the configuration of control, where the lower inscription is a repetition.

theorem mk_mem_copyRel_merge L167–173

{t x y : SyntacticObject} (h : t.Contains y) (hxy : x.StructurallyIdentical y) :

(x, y) ∈ (x.merge t).copyRel

Built from ,

L175–176

A term merged with the object it is a term of is related to itself exactly when it is a proper term: an object merged with itself c-commands nothing.

theorem self_mem_copyRel_merge_iff L178–188

{t x : SyntacticObject} (hx : x ∈ t.terms) :

(x, x) ∈ (x.merge t).copyRel ↔ x ≠ t

Built from

Objects without repetitions

No two distinct tokens of s inscribe one lexical item, at a leaf or at a trace.

def HasDistinctItems L192–195

(s : SyntacticObject) :

Prop

The definition is too large to print here; read it in the source.

Used by StructurallyIdentical.eq_of_mem_terms, copyRel_subset_id

Used in Landau2024b, Manzini2026

L197–221

In such an object Form Copy relates each inscription only to itself: its copies are those Internal Merge leaves.

theorem copyRel_subset_id L223–226

{s : SyntacticObject} (hs : s.HasDistinctItems) :

s.copyRel ⊆ SetRel.id

Built from ,