Derivation-grounded externalization

[marcolli-chomsky-berwick-2025] §1.12. SyntacticObject.Derivation.final is an unordered object, so the surface left-to-right order is not recoverable from it, but a Derivation records the planarization choices: em .left and im place material on the left edge, em .right on the right, MCB's externalization section σ_L fixed by the derivation rather than by a noncanonical choice of representative. Derivation.externalize? replays the steps on an ordered accumulator, a PlanarSyntacticObject, so surface orders decide; it is partial by design, none when a merged item is complex or a mover is absent. Traces are unpronounced, dropped by the yield. The faithfulness theorem externalize?_faithful says the replay commutes with forgetting the order: whenever it succeeds, its result is the derived object itself, so the surface readouts surfaceTokens, surfaceCats and surfacePhon are the word order of the actual derived syntactic object. Sibling accounts of linearization: the selection-induced harmonic order (Linearization/Externalization.lean) and Fox–Pesetsky cyclic linearization (Linearization/Cyclic.lean).

Main definitions

• Minimalist.PlanarSyntacticObject.moveLeft, Minimalist.externStep, Minimalist.SyntacticObject.Derivation.externalize?: the replay.
• Minimalist.SyntacticObject.Derivation.surfaceTokens, surfaceCats, surfacePhon.

Main results

• Minimalist.SyntacticObject.Derivation.externalize?_faithful: a successful replay forgets to final.

References

• [marcolli-chomsky-berwick-2025], §1.12

Operations on ordered trees

def Minimalist.SyntacticObject.toPlanarLeaf? (s : SyntacticObject) : Option PlanarSyntacticObject

The ordered leaf of a leaf object; none on a complex object.

Equations

• s.toPlanarLeaf? = match s.getLIToken with | some tok => some ↑tok | none => if s = Minimalist.SyntacticObject.trace then some Minimalist.PlanarSyntacticObject.trace else none

def Minimalist.planarYield : RoseTree SyntacticObject.Vertex → List LIToken

Left-to-right token yield of an ordered tree; traces are unpronounced.

Equations

• Minimalist.planarYield (RoseTree.node (Sum.inl tok) children) = [tok]
• Minimalist.planarYield (RoseTree.node (Sum.inr none) [l, r]) = Minimalist.planarYield l ++ Minimalist.planarYield r
• Minimalist.planarYield (RoseTree.node (Sum.inr val) children) = []

def Minimalist.projEqP (target : SyntacticObject) (s : RoseTree SyntacticObject.Vertex) : Bool

The subtree projects to target: its unordered tree is target's.

Equations

• Minimalist.projEqP target s = decide (UnorderedTree.mk s = ↑target)

def Minimalist.planarFindP? (p : RoseTree SyntacticObject.Vertex → Bool) : RoseTree SyntacticObject.Vertex → Option (RoseTree SyntacticObject.Vertex)

The leftmost, root-first subtree satisfying p.

Equations

• One or more equations did not get rendered due to their size.
• Minimalist.planarFindP? p (RoseTree.node value []) = if p (RoseTree.node value []) = true then some (RoseTree.node value []) else none
• Minimalist.planarFindP? p (RoseTree.node value children) = if p (RoseTree.node value children) = true then some (RoseTree.node value children) else none

def Minimalist.planarReplaceWhereP (p : RoseTree SyntacticObject.Vertex → Bool) (rep : RoseTree SyntacticObject.Vertex) : RoseTree SyntacticObject.Vertex → RoseTree SyntacticObject.Vertex

Replace every subtree satisfying p by rep.

Equations

• One or more equations did not get rendered due to their size.
• Minimalist.planarReplaceWhereP p rep (RoseTree.node value []) = if p (RoseTree.node value []) = true then rep else RoseTree.node value []
• Minimalist.planarReplaceWhereP p rep (RoseTree.node value children) = if p (RoseTree.node value children) = true then rep else RoseTree.node value children

The replay on ordered objects

def Minimalist.PlanarSyntacticObject.find? (target : SyntacticObject) (acc : PlanarSyntacticObject) : Option PlanarSyntacticObject

The leftmost subtree projecting to target.

Equations

• One or more equations did not get rendered due to their size.

def Minimalist.PlanarSyntacticObject.replaceWhere (target : SyntacticObject) (rep acc : PlanarSyntacticObject) : PlanarSyntacticObject

Every subtree projecting to target replaced by the leaf rep.

Equations

• Minimalist.PlanarSyntacticObject.replaceWhere target rep acc = ⟨Minimalist.planarReplaceWhereP (Minimalist.projEqP target) ↑rep ↑acc, ⋯⟩

theorem Minimalist.PlanarSyntacticObject.toSyntacticObject_find? {target : SyntacticObject} {acc s : PlanarSyntacticObject} (h : find? target acc = some s) : ↑s = target

theorem Minimalist.PlanarSyntacticObject.toSyntacticObject_replaceWhere (target : SyntacticObject) (rep acc : PlanarSyntacticObject) : ↑(replaceWhere target rep acc) = (↑acc).replace target ↑rep

Replacement forgets to the structural substitution SyntacticObject.replace.

def Minimalist.SyntacticObject.tracePlanar (s : SyntacticObject) : PlanarSyntacticObject

The ordered trace a moved object leaves, SyntacticObject.headTrace with its order.

Equations

• s.tracePlanar = s.selHead.elim Minimalist.PlanarSyntacticObject.trace Minimalist.PlanarSyntacticObject.traceOf

@[simp]

theorem Minimalist.SyntacticObject.toSyntacticObject_tracePlanar (s : SyntacticObject) : ↑s.tracePlanar = s.headTrace

def Minimalist.PlanarSyntacticObject.moveLeft (acc : PlanarSyntacticObject) (mover : SyntacticObject) : Option PlanarSyntacticObject

Internal Merge on the ordered accumulator: the leftmost subtree projecting to mover is raised to the left edge, leaving the trace of its head; none if absent.

Equations

• One or more equations did not get rendered due to their size.

theorem Minimalist.PlanarSyntacticObject.toSyntacticObject_moveLeft {acc p' : PlanarSyntacticObject} {mover : SyntacticObject} (h : acc.moveLeft mover = some p') : ↑p' = (mover.deleteAccessible ↑acc).merge mover

Internal Merge on the ordered accumulator forgets to Internal Merge on the object.

def Minimalist.externStep (acc? : Option PlanarSyntacticObject) (step : SyntacticObject.Step) : Option PlanarSyntacticObject

One replay step, mirroring SyntacticObject.Step.apply.

Equations

• One or more equations did not get rendered due to their size.

def Minimalist.SyntacticObject.Derivation.externalize? (d : Derivation) : Option PlanarSyntacticObject

The derivation's ordered object, MCB's σ_L for this derivation, or none if a merged item is complex or a mover is absent.

Equations

• d.externalize? = d.initial.toPlanarLeaf?.bind fun (init : Minimalist.PlanarSyntacticObject) => List.foldl Minimalist.externStep (some init) d.steps

def Minimalist.SyntacticObject.Derivation.surfaceTokens (d : Derivation) : List LIToken

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

Equations

• d.surfaceTokens = (Option.map (fun (x : Minimalist.PlanarSyntacticObject) => Minimalist.planarYield ↑x) d.externalize?).getD []

def Minimalist.SyntacticObject.Derivation.surfaceCats (d : Derivation) : List Cat

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

Equations

• d.surfaceCats = List.map (fun (x : Minimalist.LIToken) => x.item.outerCat) d.surfaceTokens

def Minimalist.SyntacticObject.Derivation.surfacePhon (d : Derivation) : List String

The surface string: pronounced forms left to right, empty forms dropped.

Equations

• d.surfacePhon = List.filterMap Minimalist.LIToken.phonForm? d.surfaceTokens

Faithfulness

theorem Minimalist.SyntacticObject.Derivation.externalize?_faithful (d : Derivation) {p : PlanarSyntacticObject} (h : d.externalize? = some p) : ↑p = d.final

Faithfulness ([marcolli-chomsky-berwick-2025] §1.12): a successful replay forgets to the derived object, so the surface readouts are the word order of final itself.

theorem Minimalist.SyntacticObject.Derivation.externalize?_take_faithful (d : Derivation) (n : ℕ) {p : PlanarSyntacticObject} (h : (d.take n).externalize? = some p) : ↑p = d.stageAt n

Faithfulness for a prefix: a successful replay of the first n steps forgets to stage n.

The [cinque-2005] pied-piping contrast

Phrasal pied-piping preserves the moved constituent's internal order: raising N around A and pied-piping [N A] around Num gives Dem-N-A-Num, pied-piping [A N] around Num gives Dem-A-N-Num. .D stands in for the demonstrative.