Head Functions for Minimalist Syntactic Objects (MCB §1.12-§1.13) #

@cite{marcolli-chomsky-berwick-2025}

What MCB say #

Per @cite{marcolli-chomsky-berwick-2025} §1.12 (book pp. 105-108), Externalization is modelled as a section σ_L : 𝔗_{SO_0} → 𝔗^{pl}_{SO_0} of the projection Π : 𝔗^{pl}_{SO_0} → 𝔗_{SO_0} from planar to nonplanar binary rooted trees. The section satisfies Π ∘ σ_L = id and is:

NOT a morphism of magmas (Lemma 1.13.1: no morphism of magmas exists from the commutative SO to the noncommutative SO^{nc}).
Noncanonical — depends on the language L.

A head function (Def 1.13.6) is a partial map h defined on a subdomain Dom(h) ⊂ 𝔗_{SO_0} that assigns to each T ∈ Dom(h) a function h_T : V^o(T) → L(T) from non-leaf vertices of T to leaves, satisfying coherence: T_v ⊆ T_w ∧ h_T(w) ∈ L(T_v) ⊆ L(T_w) ⟹ h_T(w) = h_T(v) (Def 1.13.3).

Per Lemma 1.13.5, head functions on T are in bijection with planar embeddings of T — under either the harmonic head-initial convention (head daughter to the LEFT) or the harmonic head-final convention (head daughter to the RIGHT). The choice between conventions inverts the bijection.

Encoding #

HeadFunction is a FreeCommMagma.Section (the σ_L part) plus head-side convention (initial vs final per Lemma 1.13.5) plus partial domain (Def 1.13.6):

structure HeadFunction where
  section_  : FreeCommMagma.Section (LIToken ⊕ Nat)
  headSide  : ConventionDir
  Dom       : SyntacticObject → Prop
  decDom    : DecidablePred Dom

The substrate primitive is headAtVertex h T v (MCB Def 1.13.3): the head leaf at vertex v of T. The root special case head h T is derived as headAtVertex h T T.

Per Lemma 1.13.5, the head leaf at vertex v is:

under .initial: leftmost-leaf of h.section_.σ v
under .final: rightmost-leaf of h.section_.σ v

Key definitions #

ConventionDir — harmonic head-side (.initial/.final)
HeadFunction — bundle of section + side + domain
headAtVertex h T v — MCB Def 1.13.3 head function at vertex (substrate primitive)
head h T — root special case (MCB notation h(T))
outerCat h so, outerSel h so — head's category/selectional stack
linearize h so, phonYield h so, terminalNodes h so, leafTokens h so — planar yields
IsRaisingClauseI, IsRaisingClauseII, IsRaising — Def 1.15.1 raising condition

Out of scope (queued for §1.14+) #

Complemented head function (Def 1.14.2): extends h(v) to (h(v), Z_v) with the head's complement subtree. Will be a sibling structure ComplementedHeadFunction extends HeadFunction with complement : V^o T → Option SO.
Maximal-projection paths γ_ℓ (Lemma 1.14.1): requires headAtVertex (now landed) to define paths of constant-head vertices.
Phase Theory restrictions on Dom(h) (MCB §1.14).
Π_L language filter (eq 1.12.4): second projection separate from σ_L. Will be a sibling structure LanguageFilter if/when needed; not merged into Dom.
Mixed-direction headSide: empirically real (German VP head-final + CP head-initial) but MCB don't address. Future refinement: headSide : Cat → ConventionDir. Current global encoding suffices for §1.13-§1.16.
Lemma 1.13.7 three Chomsky [23] §4 properties: equivalent characterizations of head functions via per-vertex projection-marking. Optional sibling constructor fromProjectionMarking.
Module-side lifting (§1.12.3, §1.12.5): Section.σ lifts to V(𝔗_{SO_0}) → V(𝔗^{pl}_{SO_0}) linear map via Quot.lift. Add when needed.
headAtVertex_coherent proof: requires well-founded induction on planar descent; statement is correct here, proof is queued.

Head Functions for Minimalist Syntactic Objects (MCB §1.12-§1.13) #

What MCB say #

Encoding #

Key definitions #

Out of scope (queued for §1.14+) #

Convention direction (MCB Lemma 1.13.5) #