Externalization on the SyntacticObject carrier

This file defines the selection-induced linearization of syntactic objects ([MCB25] §1.12.1, §1.13): the surface token order obtained by placing the projecting daughter's yield on a language's harmonic head side. Lemma 1.13.5 identifies head functions on a binary tree with its planar embeddings, and Lemma 1.13.7 identifies head functions with bare-phrase-structure projection ([Cho95a]); composed with [Adg03]'s identification of the projecting item as the selecting item (a synthesis step of this formalization, not a claim of the book), c-selection computes the planar order.

Main declarations

• Minimalist.LinearizationState: the value of the book's head function in its two descriptions — the selection state enriched with the yield, 0 off Dom(h); a CommMagma and MulZeroClass under the side-indexed Merge-local product.
• Minimalist.LinearizationState.sel: the projection morphism to SelectionState.
• Minimalist.SyntacticObject.headHom: the head function as a morphism of magmas SyntacticObject →ₙ* LinearizationState side, refining selCheckHom.
• Minimalist.SyntacticObject.linearize, Minimalist.SyntacticObject.phonYield: the yield readout and the pronounced surface forms.

Main results

• Minimalist.SyntacticObject.sel_comp_headHom: fusion — the selection component of the head function's value is the selection check, by SyntacticObject.hom_ext.

Implementation notes

Head functions are partial ([MCB25] §1.13.2): at exocentric nodes no daughter projects and no order is determined — the book rejects inducing one from a total order on labels as "not a realistic linguistic assumption" — so the state is 0 there, the absorbing element of the book's renormalization reading of partial head functions. The selection state and the yield are the book's two descriptions of one head function: eq. (1.13.3) reads h(T) as "a single leaf (the head)" or as the ordered leaf sequence, "switch[ing] between these two descriptions without changing the notation". LinearizationState fuses them into one partial value, making Dom(yield) = Dom(h) true by construction. Naming: the head-function maps (headHom and the leaf data it lifts) carry the book's name for h; the value type does not — the book restricts "the term head to terminal elements" (quoting [Cho95a] §4), and the strict head is recovered via sel. SyntacticObject.linearize is the harmonic candidate for the externalization section σ_L, defined on Dom(h) only — the book's σ_L must extend it noncanonically off Dom(h). Conceptually the yield component is WithZero (FreeMonoid LIToken): a silent trace is the unit, exocentricity the absorbing zero, and head-final placement is multiplication in the opposite monoid.

Only the two harmonic sections are realized: uniform head-side placement is right for head–complement structure but does not model specifier placement (that needs the headSide : Cat → ConventionDir refinement noted at ConventionDir).

def Minimalist.placeYield : ConventionDir → List LIToken → List LIToken → List LIToken

Place the head daughter's yield on the convention side: .initial → head-yield first, .final → head-yield last.

Equations

• Minimalist.placeYield Minimalist.ConventionDir.initial x✝¹ x✝ = x✝¹ ++ x✝
• Minimalist.placeYield Minimalist.ConventionDir.final x✝¹ x✝ = x✝ ++ x✝¹

The linearization state

structure Minimalist.LinearizationState (side : ConventionDir) : Type

The value of the head function in its two descriptions: the projecting head with its residual stack, enriched with the yield; 0 off Dom(h). The side parameter is phantom in the carrier — the multiplication reads it.

• toOption : Option ((LIToken × List Cat) × List LIToken)

def Minimalist.instDecidableEqLinearizationState.decEq {side✝ : ConventionDir} (x✝ x✝¹ : LinearizationState side✝) : Decidable (x✝ = x✝¹)

Equations

• Minimalist.instDecidableEqLinearizationState.decEq { toOption := a } { toOption := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Minimalist.instDecidableEqLinearizationState {side✝ : ConventionDir} : DecidableEq (LinearizationState side✝)

Equations

• Minimalist.instDecidableEqLinearizationState = Minimalist.instDecidableEqLinearizationState.decEq

def Minimalist.LinearizationState.of {side : ConventionDir} (tok : LIToken) (stack : List Cat) (yld : List LIToken) : LinearizationState side

A defined state: projecting head tok, residual stack stack, yield yld.

Equations

• Minimalist.LinearizationState.of tok stack yld = { toOption := some ((tok, stack), yld) }

@[implicit_reducible]

instance Minimalist.LinearizationState.instMulZeroClass {side : ConventionDir} : MulZeroClass (LinearizationState side)

Merge-local externalization: the selCombine decision places the projecting daughter's yield on the convention side; 0 is absorbing.

Equations

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

theorem Minimalist.LinearizationState.some_mul_some {side : ConventionDir} (s₁ s₂ : LIToken × List Cat) (y₁ y₂ : List LIToken) : { toOption := some (s₁, y₁) } * { toOption := some (s₂, y₂) } = { toOption := Option.map (fun (p : Bool × LIToken × List Cat) => (p.2, placeYield side (bif p.1 then y₁ else y₂) (bif p.1 then y₂ else y₁))) (selCombine { toOption := some s₁ } { toOption := some s₂ }) }

* on defined states: the canonical accessor.

@[implicit_reducible]

instance Minimalist.LinearizationState.instCommMagma {side : ConventionDir} : CommMagma (LinearizationState side)

Equations

• Minimalist.LinearizationState.instCommMagma = { toMul := Minimalist.LinearizationState.instMulZeroClass.toMul, mul_comm := ⋯ }

def Minimalist.LinearizationState.sel {side : ConventionDir} : LinearizationState side →ₙ* SelectionState

The projection to the selection state: forgetting the order description.

Equations

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

@[simp]

theorem Minimalist.LinearizationState.sel_of {side : ConventionDir} (tok : LIToken) (stack : List Cat) (yld : List LIToken) : sel (of tok stack yld) = SelectionState.of tok stack

@[simp]

theorem Minimalist.LinearizationState.sel_zero {side : ConventionDir} : sel 0 = 0

def Minimalist.LinearizationState.yield {side : ConventionDir} (x : LinearizationState side) : Option (List LIToken)

The yield component: the ordered leaf sequence, none off Dom(h).

Equations

• x.yield = Option.map (fun (x : (Minimalist.LIToken × List Minimalist.Cat) × List Minimalist.LIToken) => x.2) x.toOption

@[simp]

theorem Minimalist.LinearizationState.yield_of {side : ConventionDir} (tok : LIToken) (stack : List Cat) (yld : List LIToken) : (of tok stack yld).yield = some yld

@[simp]

theorem Minimalist.LinearizationState.yield_zero {side : ConventionDir} : yield 0 = none

Externalization on SyntacticObject

def Minimalist.SyntacticObject.linearizationState (side : ConventionDir) (s : SyntacticObject) : LinearizationState side

The head function's value on a syntactic object: the liftFun of pronounced lexical leaves and the silent, saturated trace.

Equations

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

@[simp]

theorem Minimalist.SyntacticObject.linearizationState_lexLeaf (side : ConventionDir) (tok : LIToken) : linearizationState side (lexLeaf tok) = LinearizationState.of tok tok.item.outerSel [tok]

@[simp]

theorem Minimalist.SyntacticObject.linearizationState_traceLeaf (side : ConventionDir) : linearizationState side traceLeaf = LinearizationState.of (mkTraceToken 0) [] []

@[simp]

theorem Minimalist.SyntacticObject.linearizationState_node (side : ConventionDir) (l r : SyntacticObject) : linearizationState side (l.node r) = linearizationState side l * linearizationState side r

noncomputable def Minimalist.SyntacticObject.headHom (side : ConventionDir) : SyntacticObject →ₙ* LinearizationState side

The head function as a morphism of magmas ([MCB25] §1.13's algebraic frame): Merge multiplies constituents, h multiplies states.

Equations

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

@[simp]

theorem Minimalist.SyntacticObject.headHom_apply (side : ConventionDir) (s : SyntacticObject) : (headHom side) s = linearizationState side s

theorem Minimalist.SyntacticObject.sel_comp_headHom (side : ConventionDir) : LinearizationState.sel.comp (headHom side) = selCheckHom

Fusion: the selection component of the head function's value is the selection check — two morphisms agreeing on the leaves (hom_ext).

def Minimalist.SyntacticObject.linearize (side : ConventionDir) (s : SyntacticObject) : Option (List LIToken)

The surface token order under head-side convention side ([MCB25] §1.12.1): the yield readout of the linearization state. Not a morphism — placing a yield needs the head.

Equations

• Minimalist.SyntacticObject.linearize side s = (Minimalist.SyntacticObject.linearizationState side s).yield

def Minimalist.SyntacticObject.phonYield (side : ConventionDir) (s : SyntacticObject) : Option (List String)

The pronounced surface forms: the yield with unpronounced tokens dropped.

Equations

• Minimalist.SyntacticObject.phonYield side s = Option.map (fun (x : List Minimalist.LIToken) => List.filterMap Minimalist.LIToken.phonForm? x) (Minimalist.SyntacticObject.linearize side s)

@[simp]

theorem Minimalist.SyntacticObject.linearize_lexLeaf (side : ConventionDir) (tok : LIToken) : linearize side (lexLeaf tok) = some [tok]

@[simp]

theorem Minimalist.SyntacticObject.linearize_traceLeaf (side : ConventionDir) : linearize side traceLeaf = some []