Docs / Syntax / Minimalist / Copy / Marked

Linearized objects with their lower copies marked

import Linglib.Syntax.Minimalist.Copy.Marked · namespace Minimalist

Under the copy theory a moved constituent leaves a copy of itself, and externalization pronounces only the highest. A linearized syntactic object with its lower copies marked carries both: forgetting the marks gives the copy object, and contracting each marked subtree to the trace leaf of its mark gives the object externalization reads, its traces silent. Marking the outermost copies of a term mirrors replacing them in the contraction, and a c-command between pronounced leaves of the contraction holds in the copy object.

Main definitions

Minimalist.CopyMark, Minimalist.LinearizedSyntacticObject.Marked: marks and marked objects.
Minimalist.LinearizedSyntacticObject.Marked.unmark, contract: the copy object and its contraction.
Minimalist.LinearizedSyntacticObject.Marked.mark, find?: marking the lower copies of a term, and the occurrence of a term outside the lower copies.

Main results

Minimalist.LinearizedSyntacticObject.Marked.contract_mark: marking contracts to replacement.
Minimalist.LinearizedSyntacticObject.Marked.map_contract_find?: the occurrence found contracts to the occurrence found in the contraction.

Implementation notes

The contraction has the shape of the contraction quotient of Marcolli, Chomsky and Berwick, but plays a different role. Their account sends that quotient to the semantic interface and its deletion to externalization; here externalization reads the contraction, and binding at LF reads the copy object, as Collins argues it must.

References

Marcolli et al. 2025, Mathematical Structure of Syntactic Merge: An Algebraic Model for Generative Linguistics formalized
Collins 2026, Reconstruction and the New Minimalism formalized

Declarations

The mark on a vertex of a linearized copy object: some l on the root of a lower copy, l the label of the trace that stands for it, and none elsewhere.

@[reducible, inline] abbrev CopyMark L54–56

Type

CopyMark = Option (Option LexicalItem.Token)

Used in Syntax/Minimalist/Copy/BindingAtReading, Syntax/Minimalist/Copy/Cut, Syntax/Minimalist/Copy/Reading

A linearized syntactic object with its lower copies marked, the datum externalization reads. The copy object itself is a syntactic object, order and marks forgotten.

def LinearizedSyntacticObject.Marked L58–61

Type

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

Used in Syntax/Minimalist/Copy/BindingAtReading, Syntax/Minimalist/Copy/Cut, Syntax/Minimalist/Copy/Reading, Syntax/Minimalist/Copy/Replay, Syntax/Minimalist/Copy/ToTree

L63

Contraction

The copy object, the marks forgotten.

def LinearizedSyntacticObject.Marked.unmark L99–100

(t : Marked) :

LinearizedSyntacticObject

t.unmark = ⟨RoseTree.map Prod.snd ↑t, ⋯⟩

Built from

Used by LinearizedSyntacticObject.Marked.unmark_ofLinearized, LinearizedSyntacticObject.Marked.unmark_attach, LinearizedSyntacticObject.Marked.unmark_mark, LinearizedSyntacticObject.Marked.mem_terms_of_find?, LinearizedSyntacticObject.Marked.exists_val_eq_of_unmark_eq_leaf, LinearizedSyntacticObject.Marked.contract_eq_leaf_of_unmark_eq_leaf, LinearizedSyntacticObject.Marked.eq_leaf_of_find?

Used in Syntax/Minimalist/Copy/Cut, Syntax/Minimalist/Copy/Reading, Syntax/Minimalist/Copy/Replay, Collins2026

The contraction: each lower copy becomes the trace that stands for it, the form externalization reads. It has the shape of the contraction quotient $T/^c F$ of Marcolli et al. 2025 (Definition 1.2.4), though the book sends that quotient to the Conceptual-Intensional interface and its deletion $T/^d F$ to externalization (pp. 33, 82).

def LinearizedSyntacticObject.Marked.contract L102–106

(t : Marked) :

LinearizedSyntacticObject