Docs / Syntax / Minimalist / Copy / Replay

Derivations with copies

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

Under the copy theory Internal Merge merges a copy of the mover and leaves the mover in place. The replay of a derivation with copies builds its linearized copy object with the lower copies marked, and contracting them gives the replay with traces. The copy object is a syntactic object, on which Internal Merge is Merge with one of the object's own terms, the terms of each stage are terms of every later one, and only the tokens the derivation merges are pronounced.

Main definitions

Minimalist.Step.replayWithCopies?, Minimalist.Derivation.replayWithCopies?: the replay with copies.
Minimalist.Derivation.copyObject?: the copy object.

Main results

Minimalist.Derivation.map_contract_replayWithCopies?: contracting the lower copies gives the replay with traces.
Minimalist.Step.replayWithCopies?_im_eq_merge: Internal Merge with copies is MERGE leaving copies on the copy object and MERGE leaving traces on its contraction.
Minimalist.Step.count_terms_replayWithCopies?_im: it adds a position to the chain it moves.
Minimalist.Step.unmark_replayWithCopies?_im: Extension and No Tampering.
Minimalist.Derivation.copyObject?_append_em, copyObject?_append_im: External Merge merges the copy object with an item from outside, Internal Merge with one of its own terms.
Minimalist.Derivation.copyRel_copyObject?_append_im: Internal Merge leaves a copy in the sense of Form Copy.
Minimalist.Derivation.terms_subset_copyObject?_append: preservation of terms.
Minimalist.Derivation.mem_lexTokens_of_mem_yield_copyObject?: Inclusiveness.

TODO

Steps name their movers in the replay with traces, so a remnant mover carries traces and the copy object depends on the trace encoder τ; and each lower copy is marked, so deleted, at the step that moves it, which leaves no room for externalizations that pronounce several copies. Name movers independently of traces and decide deletion at externalization.

References

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

The replay with copies

A step on a marked configuration, Step.replay? keeping the copies. Internal Merge merges a copy of the leftmost outermost occurrence of the mover and marks the occurrences it leaves as lower copies, each with the trace of the mover's head under τ; an extraction stacks the copy.

def Step.replayWithCopies?L66–77

(step : Step) (c : Derivation.Cfg LinearizedSyntacticObject.Marked) (τ : SyntacticObject → Option LexicalItem.Token := SyntacticObject.selHead) :

Option (Derivation.Cfg LinearizedSyntacticObject.Marked)

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

Used by Step.map_contract_replayWithCopies?, Step.unmark_replayWithCopies?_im, Step.replayWithCopies?_im_eq_merge, Derivation.replayWithCopies?_append, Derivation.replayWithCopies?_append_singleton, Step.toSyntacticObject_replayWithCopies?_em, Step.toSyntacticObject_replayWithCopies?_im, Step.count_terms_replayWithCopies?_im, Step.mem_terms_replayWithCopies?

The derivation's marked configuration under the trace encoder τ, none exactly when Derivation.replay? is.

def Derivation.replayWithCopies?L79–84

(d : Derivation) (τ : SyntacticObject → Option LexicalItem.Token := SyntacticObject.selHead) :

Option (Cfg LinearizedSyntacticObject.Marked)

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

Used by Derivation.map_contract_replayWithCopies?, Derivation.externalize?_eq_map_replayWithCopies?, Derivation.isSome_replayWithCopies?, Derivation.copyObject?, Derivation.replayWithCopies?_append, Derivation.replayWithCopies?_append_singleton

Used in Syntax/Minimalist/Copy/BindingAtReading, Syntax/Minimalist/Copy/ToTree, Collins2005, Collins2026

L88–108

Contracting the copies of the replay with copies gives the replay with traces.

theorem Derivation.map_contract_replayWithCopies?L110–118

{τ : SyntacticObject → Option LexicalItem.Token} (d : Derivation) :

Option.map (Cfg.map LinearizedSyntacticObject.Marked.contract) (d.replayWithCopies? τ) = d.replay? τ

Built from

L120–123

L125–127

Internal Merge with copies merges a copy of a subtree of the copy object onto the object unchanged: Extension and No Tampering.

theorem Step.unmark_replayWithCopies?_im L129–139

{τ : SyntacticObject → Option LexicalItem.Token} {mover : SyntacticObject} {side : Edge} {c c' : Derivation.Cfg LinearizedSyntacticObject.Marked} (h : (im mover side).replayWithCopies? c τ = some c') :

∃ (s : LinearizedSyntacticObject.Marked), (↑s.unmark).IsSubtree ↑c.current.unmark ∧ c'.current.unmark = c.current.unmark.attach side s.unmark

Built from

Internal Merge with copies is MERGE leaving copies of a copy of the mover on the copy object, and MERGE leaving traces of the mover on the contraction.

theorem Step.replayWithCopies?_im_eq_merge L141–164

∃ (s : LinearizedSyntacticObject.Marked), ↑s.contract = mover ∧ {↑c'.current.unmark} = {↑c.current.unmark}.merge ↑s.unmark ↑c.current.unmark ∧ {↑c'.current.contract} = Workspace.mergeWith (fun (x : SyntacticObject) => x.headTrace τ) {↑c.current.contract} mover ↑c.current.contract

Built from

The copy object

The derivation's copy object, the syntactic object with every copy in place and neither order nor marks: the form the semantic interface receives.

def Derivation.copyObject?L168–172

(d : Derivation) (τ : SyntacticObject → Option LexicalItem.Token := SyntacticObject.selHead) :

Option SyntacticObject

d.copyObject? τ = Option.map (fun (x : Derivation.Cfg LinearizedSyntacticObject.Marked) => ↑x.current.unmark) (d.replayWithCopies? τ)

Built from

Used by Derivation.terms_subset_copyObject?_append, Derivation.copyObject?_append_em, Derivation.copyObject?_append_im, Derivation.copyRel_copyObject?_append_im, Derivation.mem_lexTokens_of_mem_yield_copyObject?

Used in Syntax/Minimalist/Derivation/Reconstruction

Internal Merge with copies adds a position to the chain of the copy it merges (LinearizedSyntacticObject.card_chainRel).

theorem Step.count_terms_replayWithCopies?_im L205–213

∃ u ∈ (↑c.current.unmark).terms, Multiset.count u (↑c'.current.unmark).terms = Multiset.count u (↑c.current.unmark).terms + 1

Built from

L215–236

Preservation of terms: the terms of the copy object at a stage are terms of the copy object at every later stage.

theorem Derivation.terms_subset_copyObject?_append L248–257

{τ : SyntacticObject → Option LexicalItem.Token} {d : Derivation} {steps : List Step} {C' : SyntacticObject} (h : (d.append steps).copyObject? τ = some C') :

∃ C ∈ d.copyObject? τ, C.terms ⊆ C'.terms

Built from

External Merge merges the copy object with the item, built outside.

theorem Derivation.copyObject?_append_em L259–264

{τ : SyntacticObject → Option LexicalItem.Token} (d : Derivation) (side : Edge) (item : LinearizedSyntacticObject) :

(d.append [Step.em side item]).copyObject? τ = Option.map (↑item).merge (d.copyObject? τ)

Built from

Internal Merge merges the copy object with one of its own terms, so Internal and External Merge are one operation, differing in where its object comes from.

theorem Derivation.copyObject?_append_im L266–275

{τ : SyntacticObject → Option LexicalItem.Token} {d : Derivation} {mover : SyntacticObject} {side : Edge} {C' : SyntacticObject} (h : (d.append [Step.im mover side]).copyObject? τ = some C') :

∃ C ∈ d.copyObject? τ, ∃ u ∈ C.terms, C' = u.merge C

Built from

The occurrence Internal Merge leaves is a copy of the one it merges, in the sense of Form Copy, unless the whole object moves.

theorem Derivation.copyRel_copyObject?_append_im L277–283

{τ : SyntacticObject → Option LexicalItem.Token} {d : Derivation} {mover : SyntacticObject} {side : Edge} {C' : SyntacticObject} (h : (d.append [Step.im mover side]).copyObject? τ = some C') :

∃ C ∈ d.copyObject? τ, ∃ u ∈ C.terms, C' = u.merge C ∧ ((u, u) ∈ C'.copyRel ↔ u ≠ C)

Built from

Inclusiveness

Inclusiveness: the copy object pronounces only tokens the derivation merges.

theorem Derivation.mem_lexTokens_of_mem_yield_copyObject?L341–350

{τ : SyntacticObject → Option LexicalItem.Token} {d : Derivation} {C : SyntacticObject} {tok : LexicalItem.Token} (h : d.copyObject? τ = some C) (ht : tok ∈ C.yield) :

tok ∈ d.lexTokens

Built from