Form Copy

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.copyRel: the copy relation Form Copy assigns in an object

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: the copy Internal Merge leaves is related to its antecedent

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

• [CSB+23]
• [MCB25]

Structural identity

def Minimalist.SyntacticObject.erase (s : SyntacticObject) : UnorderedTree (Option LexicalItem ⊕ Option LexicalItem)

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

Equations

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

@[simp]

theorem Minimalist.SyntacticObject.erase_leaf (tok : LexicalItem.Token) : (↑tok).erase = UnorderedTree.leaf (Sum.inl (some tok.item))

@[simp]

theorem Minimalist.SyntacticObject.erase_traceOf (tok : LexicalItem.Token) : (traceOf tok).erase = UnorderedTree.leaf (Sum.inr (some tok.item))

@[simp]

theorem Minimalist.SyntacticObject.erase_merge (l r : SyntacticObject) : (l.merge r).erase = UnorderedTree.node (Sum.inl none) {l.erase, r.erase}

def Minimalist.SyntacticObject.StructurallyIdentical (x y : SyntacticObject) : Prop

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

Equations

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

@[instance_reducible]

instance Minimalist.SyntacticObject.instDecidableRelStructurallyIdentical : DecidableRel StructurallyIdentical

Equations

• x.instDecidableRelStructurallyIdentical y = Minimalist.SyntacticObject.instDecidableRelStructurallyIdentical._aux_1 x y

theorem Minimalist.SyntacticObject.structurallyIdentical_equivalence : Equivalence StructurallyIdentical

theorem Minimalist.SyntacticObject.StructurallyIdentical.refl (x : SyntacticObject) : x.StructurallyIdentical x

theorem Minimalist.SyntacticObject.StructurallyIdentical.symm {x y : SyntacticObject} (h : x.StructurallyIdentical y) : y.StructurallyIdentical x

theorem Minimalist.SyntacticObject.StructurallyIdentical.trans {t x y : SyntacticObject} (h : x.StructurallyIdentical y) (h' : y.StructurallyIdentical t) : x.StructurallyIdentical t

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

Structural identity is a congruence for Merge.

theorem Minimalist.SyntacticObject.StructurallyIdentical.numNodes_eq {x y : SyntacticObject} (h : x.StructurallyIdentical y) : (↑x).numNodes = (↑y).numNodes

Structurally identical inscriptions have the same size.

def Minimalist.SyntacticObject.IsRepetition (x y : SyntacticObject) : Prop

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

Equations

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

@[instance_reducible]

instance Minimalist.SyntacticObject.instDecidableRelIsRepetition : DecidableRel IsRepetition

Equations

• x✝¹.instDecidableRelIsRepetition x✝ = { decide := decide (x✝¹.StructurallyIdentical x✝) && decide (x✝¹ ≠ x✝), reflects_decide := ⋯ }

The copy relation

def Minimalist.SyntacticObject.copyRel (s : SyntacticObject) : SetRel SyntacticObject SyntacticObject

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

Equations

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

@[simp]

theorem Minimalist.SyntacticObject.mem_copyRel {s x y : SyntacticObject} : (x, y) ∈ s.copyRel ↔ s.CCommands x y ∧ x.StructurallyIdentical y

@[instance_reducible]

instance Minimalist.SyntacticObject.instDecidableMemProdSetRelCopyRel (s : SyntacticObject) (p : SyntacticObject × SyntacticObject) : Decidable (p ∈ s.copyRel)

Equations

• s.instDecidableMemProdSetRelCopyRel p = { decide := decide (s.CCommands p.1 p.2) && decide (p.1.StructurallyIdentical p.2), reflects_decide := ⋯ }

theorem Minimalist.SyntacticObject.cCommands_merge {t x y : SyntacticObject} (hne : x ≠ t) (h : t.ContainsOrEq y) : (x.merge t).CCommands x y

An object merged with a term c-commands everything that term reflexively contains.

theorem Minimalist.SyntacticObject.mk_mem_copyRel_merge {t x y : SyntacticObject} (h : t.Contains y) (hxy : x.StructurallyIdentical y) : (x, y) ∈ (x.merge t).copyRel

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 Minimalist.SyntacticObject.self_mem_copyRel_merge {t x : SyntacticObject} (h : t.Contains x) : (x, x) ∈ (x.merge t).copyRel

The copy Internal Merge leaves is related to its antecedent: an object merged with a term containing it c-commands its own lower occurrence.