Docs / Syntax / Minimalist / Linearization / Replay

Replaying a derivation on linearized objects

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

Free symmetric Merge builds unordered objects, so the surface order is not recoverable from Derivation.final, but each step records the side its new daughter takes. Derivation.replay? replays the steps by Merge on linearized objects, and a successful replay forgets to the derivation's own configuration, so the readouts surfaceTokens, surfaceCats and surfacePhon are the word order of the derived object. The order is a datum of the derivation rather than of its object, and a derivation whose daughters take the head side exactly when they project records the harmonic linearization of its object.

Main definitions

Minimalist.Step.replay?, Minimalist.Derivation.replay?, externalize?: the replay.
Minimalist.Step.Harmonic, Step.HarmonicList: steps that place the projecting daughter on the head side.
Minimalist.Derivation.surfaceTokens, surfaceCats, surfacePhon.

Main results

Minimalist.Derivation.replay?_faithful, externalize?_faithful: a successful replay forgets to run and final.
Minimalist.Derivation.not_factorsThrough_final: the linearized object does not factor through the derived object.
Minimalist.Derivation.externalize?_eq_linearize?: a harmonic derivation records the harmonic linearization of its object.
Minimalist.Derivation.externalize?_map: a relabelled derivation externalizes to the relabelled object, under an injective relabelling the trace encoder commutes with.

Implementation notes

The replay is partial, none when the initial object is not a leaf, when a mover is absent, or when nothing is left to merge back. An externally merged item replays in the order it was built in. Traces are unpronounced.
Sibling accounts of linearization are the selection-induced harmonic order (Linearization/Externalization.lean) and cyclic linearization (Linearization/Cyclic.lean).

References

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

Declarations

L62–65

L67–70

The replay

A step on a linearized configuration, Step.run with each new daughter on its side. Internal Merge raises the leftmost occurrence of the mover, leaving the trace of its head under τ, and an extraction stacks it; none when the mover is absent or the stack is empty.

def Step.replay?L77–90

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

Option (Derivation.Cfg LinearizedSyntacticObject)

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

Used by Derivation.replay?_append_singleton, Step.replay?_map, Step.replay?_of_harmonic, foldlM_replay?_of_harmonicList

Used in Syntax/Minimalist/Copy/Replay

The derivation's linearized configuration under the trace encoder τ, or none if the initial object is not a leaf, a mover is absent, or remerge finds the stack empty.

def Derivation.replay?L94–98

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

Option (Cfg LinearizedSyntacticObject)

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

Used by Derivation.externalize?, Derivation.replay?_append_singleton, Derivation.stack_eq_nil_of_replay?, Derivation.replay?_map, Derivation.replay?_faithful

Used in Syntax/Minimalist/Copy/Replay, Syntax/Minimalist/Derivation/Licensing, Syntax/Minimalist/Derivation/Reconstruction, Syntax/Minimalist/Linearization/ChainReduction, Privizentseva2026

The derivation's linearized object under the trace encoder τ; copies still on the stack are not part of it.

def Derivation.externalize?L100–104

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

Option LinearizedSyntacticObject

d.externalize? τ = Option.map (fun (x : Derivation.Cfg LinearizedSyntacticObject) => x.current) (d.replay? τ)

Built from

Used by Derivation.surfaceTokens, Derivation.externalize?_map, Derivation.externalize?_faithful, Derivation.externalize?_take_faithful, Derivation.externalize?_eq_linearize?, Derivation.not_factorsThrough_final

Used in Syntax/Minimalist/Copy/Replay, Syntax/Minimalist/Copy/ToTree, Syntax/Minimalist/Derivation/Reconstruction, Syntax/Minimalist/Linearization/SpelloutDomain, Syntax/Minimalist/Locality/Freezing and 5 more

The pronounced tokens, left to right; empty if the replay fails.

def Derivation.surfaceTokens L106–108

(d : Derivation) :

List LexicalItem.Token

d.surfaceTokens = (Option.map (fun (x : LinearizedSyntacticObject) => x.yield) d.externalize?).getD []

Built from

Used by Derivation.surfaceCats, Derivation.surfacePhon

Used in Syntax/Minimalist/Linearization/ChainReduction, Syntax/Minimalist/Linearization/SpelloutDomain, ColeHermon2008

The surface category sequence, the readout of word-order studies.

def Derivation.surfaceCats L110–111

(d : Derivation) :

List Cat

d.surfaceCats = List.map (fun (x : LexicalItem.Token) => x.item.cat) d.surfaceTokens

Built from

Used in Cinque2005

The surface string lists the pronounced forms left to right, dropping empty forms.

def Derivation.surfacePhon L113–115

(d : Derivation) :

List String

d.surfacePhon = List.filterMap (fun (x : LexicalItem.Token) => x.item.phonForm?) d.surfaceTokens

Built from

Used in Boskovic2018, ColeHermon2008, Collins2005, Storment2026

Faithfulness

L125–133

L135–156

Relabelling

L167–174

L178–188

theorem Derivation.externalize?_map L190–194

{τ : SyntacticObject → Option LexicalItem.Token} {f : LexicalItem.Token → LexicalItem.Token} {τ' : SyntacticObject → Option LexicalItem.Token} (hf : Function.Injective f) (hτ : ∀ (s : SyntacticObject), τ' (SyntacticObject.map f s) = Option.map f (τ s)) (d : Derivation) :

(map f d).externalize? τ' = Option.map (LinearizedSyntacticObject.map f) (d.externalize? τ)

Built from

A successful replay forgets to the configuration of the derivation (Marcolli et al. 2025 Lemma 1.13.1).

theorem Derivation.replay?_faithful L223–233

{τ : SyntacticObject → Option LexicalItem.Token} (d : Derivation) {c : Cfg LinearizedSyntacticObject} (h : d.replay? τ = some c) :

Cfg.map LinearizedSyntacticObject.toSyntacticObject c = d.run τ

Built from

A successful externalization forgets to the derived object, so the surface readouts are the word order of final itself.

theorem Derivation.externalize?_faithful L235–240

{τ : SyntacticObject → Option LexicalItem.Token} (d : Derivation) {p : LinearizedSyntacticObject} (h : d.externalize? τ = some p) :

↑p = d.final τ

Built from

L242–245

Harmonic derivations

A derivation is harmonic for a head side when each daughter it merges projects exactly if it takes the head side, and each mover leaves a trace with its selection state. Its recorded order is then the harmonic linearization of its object (Derivation.externalize?_eq_linearize?).

L281–316

L318–322

A step is harmonic for the head side side at a configuration when each daughter it merges projects exactly if it takes the head side, an externally merged item is built in its harmonic order, and a mover is a term of the object whose trace keeps its selection state.

def Step.Harmonic L326–338

(side : Edge) (τ : SyntacticObject → Option LexicalItem.Token) (c : Derivation.Cfg SyntacticObject) :

Step → Prop

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

Used by Step.HarmonicList, Step.replay?_of_harmonic

Each step of a list is harmonic at the configuration it applies to.

def Step.HarmonicList L340–344

(side : Edge) (τ : SyntacticObject → Option LexicalItem.Token) :

List Step → Derivation.Cfg SyntacticObject → Prop

Step.HarmonicList side τ [] x✝ = True
Step.HarmonicList side τ (step :: steps) x✝ = (Step.Harmonic side τ x✝ step ∧ Step.HarmonicList side τ steps (step.run x✝ τ))

Built from

Used by foldlM_replay?_of_harmonicList, Derivation.externalize?_eq_linearize?

L356–402

L404–414

A derivation from a leaf whose every step is harmonic externalizes to the harmonic linearization of its object: the order the derivation records is the one the head function determines.

theorem Derivation.externalize?_eq_linearize?L416–428

{side : Edge} {τ : SyntacticObject → Option LexicalItem.Token} {d : Derivation} (hi : d.initial.toLinearizedLeaf?.isSome = true) (hd : Step.HarmonicList side τ d.steps { current := d.initial, stack := [] }) :

d.externalize? τ = SyntacticObject.linearize? side (d.final τ)

Built from ,

The linearized object is a datum of the derivation, not of the object it derives: merging a second leaf on the left and on the right derives one object in two orders.

theorem Derivation.not_factorsThrough_final L430–437

¬Function.FactorsThrough (fun (x : Derivation) => x.externalize?) fun (x : Derivation) => x.final

Built from