Syntactic Objects: the SO₀ alphabet

[Cho13] [MCB25]

The lexical alphabet of the Minimalist Program: categorial features, lexical items, and the LIToken leaves over which syntactic objects are built. The SyntacticObject carrier itself — the MCB-faithful nonplanar SO type — lives in SyntacticObject.lean (which imports this file for the alphabet), so this Defs module is carrier-agnostic.

Per [MCB25] Def 1.1.1 (book p. 22), SO₀ consists of lexical items and syntactic features. Linglib encodes a leaf as an LIToken (an instantiated LexicalItem); the carrier's leaf alphabet is LIToken ⊕ Unit (lexical leaf inl tok vs the bare trace/structural vertex inr ()).

• Cat, SelStack, SimpleLI, LexicalItem, LIToken
• ConventionDir — harmonic head-side parameter (Lemma 1.13.5)
• uposToCat — UD POS → Minimalist Cat bridge
• mkTraceToken, LIToken.phonForm — carrier-free token helpers

inductive Minimalist.Cat : Type

Categorial features (Definition 10).

Enumerates the head categories of the Minimalist Program clausal spine and nominal extended projection: cartographic left periphery, inflectional spine, v/Voice/Appl event-structure layer, nominal categorizer-and-quantity sequence, and adpositional Place/Path articulation.

• V : Cat
• N : Cat
• A : Cat
• P : Cat
• D : Cat
• T : Cat
• C : Cat
• v : Cat
• n : Cat
• a : Cat
• Place : Cat
• Path : Cat
• Num : Cat
• Q : Cat
• Voice : Cat
• Appl : Cat
• Foc : Cat
• Top : Cat
• Fin : Cat
• SA : Cat
• Say : Cat
• Force : Cat
• Neg : Cat
• Mod : Cat
• Rel : Cat
• Pol : Cat
• Asp : Cat
• Evid : Cat
• Nmlz : Cat
• K : Cat

@[implicit_reducible]

instance Minimalist.instReprCat : Repr Cat

Equations

• Minimalist.instReprCat = { reprPrec := Minimalist.instReprCat.repr }

def Minimalist.instReprCat.repr : Cat → ℕ → Std.Format

Equations

• Minimalist.instReprCat.repr Minimalist.Cat.V prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalist.Cat.V")).group prec✝
• Minimalist.instReprCat.repr Minimalist.Cat.N prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalist.Cat.N")).group prec✝
• Minimalist.instReprCat.repr Minimalist.Cat.A prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalist.Cat.A")).group prec✝
• Minimalist.instReprCat.repr Minimalist.Cat.P prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalist.Cat.P")).group prec✝
• Minimalist.instReprCat.repr Minimalist.Cat.D prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalist.Cat.D")).group prec✝
• Minimalist.instReprCat.repr Minimalist.Cat.T prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalist.Cat.T")).group prec✝
• Minimalist.instReprCat.repr Minimalist.Cat.C prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalist.Cat.C")).group prec✝
• Minimalist.instReprCat.repr Minimalist.Cat.v prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalist.Cat.v")).group prec✝
• Minimalist.instReprCat.repr Minimalist.Cat.n prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalist.Cat.n")).group prec✝
• Minimalist.instReprCat.repr Minimalist.Cat.a prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalist.Cat.a")).group prec✝
• Minimalist.instReprCat.repr Minimalist.Cat.Place prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalist.Cat.Place")).group prec✝
• Minimalist.instReprCat.repr Minimalist.Cat.Path prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalist.Cat.Path")).group prec✝
• Minimalist.instReprCat.repr Minimalist.Cat.Num prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalist.Cat.Num")).group prec✝
• Minimalist.instReprCat.repr Minimalist.Cat.Q prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalist.Cat.Q")).group prec✝
• Minimalist.instReprCat.repr Minimalist.Cat.Voice prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalist.Cat.Voice")).group prec✝
• Minimalist.instReprCat.repr Minimalist.Cat.Appl prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalist.Cat.Appl")).group prec✝
• Minimalist.instReprCat.repr Minimalist.Cat.Foc prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalist.Cat.Foc")).group prec✝
• Minimalist.instReprCat.repr Minimalist.Cat.Top prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalist.Cat.Top")).group prec✝
• Minimalist.instReprCat.repr Minimalist.Cat.Fin prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalist.Cat.Fin")).group prec✝
• Minimalist.instReprCat.repr Minimalist.Cat.SA prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalist.Cat.SA")).group prec✝
• Minimalist.instReprCat.repr Minimalist.Cat.Say prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalist.Cat.Say")).group prec✝
• Minimalist.instReprCat.repr Minimalist.Cat.Force prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalist.Cat.Force")).group prec✝
• Minimalist.instReprCat.repr Minimalist.Cat.Neg prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalist.Cat.Neg")).group prec✝
• Minimalist.instReprCat.repr Minimalist.Cat.Mod prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalist.Cat.Mod")).group prec✝
• Minimalist.instReprCat.repr Minimalist.Cat.Rel prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalist.Cat.Rel")).group prec✝
• Minimalist.instReprCat.repr Minimalist.Cat.Pol prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalist.Cat.Pol")).group prec✝
• Minimalist.instReprCat.repr Minimalist.Cat.Asp prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalist.Cat.Asp")).group prec✝
• Minimalist.instReprCat.repr Minimalist.Cat.Evid prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalist.Cat.Evid")).group prec✝
• Minimalist.instReprCat.repr Minimalist.Cat.Nmlz prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalist.Cat.Nmlz")).group prec✝
• Minimalist.instReprCat.repr Minimalist.Cat.K prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalist.Cat.K")).group prec✝

@[implicit_reducible]

instance Minimalist.instDecidableEqCat : DecidableEq Cat

Equations

• Minimalist.instDecidableEqCat x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Minimalist.instInhabitedCat : Inhabited Cat

Equations

• Minimalist.instInhabitedCat = { default := Minimalist.instInhabitedCat.default }

@[reducible, inline]

abbrev Minimalist.SelStack : Type

Selectional stack consumed left-to-right

Equations

• Minimalist.SelStack = List Minimalist.Cat

structure Minimalist.SimpleLI : Type

A simple LI is a ⟨CAT, SEL⟩ pair (Definition 10), optionally with a phonological form for linearization.

• cat : Cat
• sel : SelStack
• phonForm : String

@[implicit_reducible]

instance Minimalist.instReprSimpleLI : Repr SimpleLI

Equations

• Minimalist.instReprSimpleLI = { reprPrec := Minimalist.instReprSimpleLI.repr }

def Minimalist.instReprSimpleLI.repr : SimpleLI → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Minimalist.instDecidableEqSimpleLI : DecidableEq SimpleLI

Equations

• Minimalist.instDecidableEqSimpleLI = Minimalist.instDecidableEqSimpleLI.decEq

def Minimalist.instDecidableEqSimpleLI.decEq (x✝ x✝¹ : SimpleLI) : Decidable (x✝ = x✝¹)

Equations

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

structure Minimalist.LexicalItem : Type

Lexical item (simple or complex from head movement, Definition 88)

• features : List SimpleLI
• nonempty : self.features ≠ []

@[implicit_reducible]

instance Minimalist.instReprLexicalItem : Repr LexicalItem

Equations

• Minimalist.instReprLexicalItem = { reprPrec := Minimalist.instReprLexicalItem.repr }

def Minimalist.instReprLexicalItem.repr : LexicalItem → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Minimalist.instDecidableEqLexicalItem : DecidableEq LexicalItem

Equations

• Minimalist.instDecidableEqLexicalItem a b = if h : a.features = b.features then isTrue ⋯ else isFalse ⋯

def Minimalist.LexicalItem.simple (cat : Cat) (sel : SelStack) (phonForm : String := "") : LexicalItem

Create a simple (non-complex) LI

Equations

• Minimalist.LexicalItem.simple cat sel phonForm = { features := [{ cat := cat, sel := sel, phonForm := phonForm }], nonempty := ⋯ }

def Minimalist.LexicalItem.outerCat (li : LexicalItem) : Cat

Get the outer (projecting) category of an LI

Equations

• li.outerCat = match li.features with | [] => Minimalist.Cat.V | s :: tail => s.cat

def Minimalist.LexicalItem.outerSel (li : LexicalItem) : SelStack

Get the outer selectional requirements

Equations

• li.outerSel = match li.features with | [] => [] | s :: tail => s.sel

def Minimalist.LexicalItem.isComplex (li : LexicalItem) : Bool

Is this LI complex (result of head-to-head movement)?

Equations

• li.isComplex = decide (li.features.length > 1)

def Minimalist.LexicalItem.combine (target mover : LexicalItem) : LexicalItem

Combine two LIs for head-to-head movement (target reprojects)

Equations

• target.combine mover = { features := target.features ++ mover.features, nonempty := ⋯ }

structure Minimalist.LIToken : Type

LI token: specific instance of an LI in a derivation

• item : LexicalItem
• id : ℕ

def Minimalist.instReprLIToken.repr : LIToken → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Minimalist.instReprLIToken : Repr LIToken

Equations

• Minimalist.instReprLIToken = { reprPrec := Minimalist.instReprLIToken.repr }

@[implicit_reducible]

instance Minimalist.instDecidableEqLIToken : DecidableEq LIToken

Equations

• Minimalist.instDecidableEqLIToken a b = if hid : a.id = b.id then if hitem : a.item = b.item then isTrue ⋯ else isFalse ⋯ else isFalse ⋯

Head-side convention (MCB Lemma 1.13.5)

inductive Minimalist.ConventionDir : Type

The harmonic head-side convention ([MCB25] Lemma 1.13.5, book p. 127): head functions on a tree are in bijection with its planar embeddings, under one of two conventions:

• .initial (harmonic head-initial): the head daughter is to the LEFT of each binary node (English-like).
• .final (harmonic head-final): the head daughter is to the RIGHT (Japanese/Korean/Turkish).

A carrier-free parameter (it names a directionality, not a tree shape), so it lives in the alphabet layer alongside Cat. Consumed by the selection-induced externalization (SyntacticObject/Externalization.lean). Mixed-direction languages (German head-final VP + head-initial CP) need a headSide : Cat → ConventionDir refinement, out of scope for §1.13-§1.16.

• initial : ConventionDir
• final : ConventionDir

@[implicit_reducible]

instance Minimalist.instReprConventionDir : Repr ConventionDir

Equations

• Minimalist.instReprConventionDir = { reprPrec := Minimalist.instReprConventionDir.repr }

def Minimalist.instReprConventionDir.repr : ConventionDir → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Minimalist.instDecidableEqConventionDir : DecidableEq ConventionDir

Equations

• Minimalist.instDecidableEqConventionDir x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Minimalist.instInhabitedConventionDir : Inhabited ConventionDir

Equations

• Minimalist.instInhabitedConventionDir = { default := Minimalist.instInhabitedConventionDir.default }

def Minimalist.uposToCat : UD.UPOS → Cat

Map UD UPOS tags to Minimalist categories.

This bridges the theory-neutral UD POS tags used in Core/Basic.lean and Fragments/ to the Minimalist Cat system.

Equations

• Minimalist.uposToCat UD.UPOS.VERB = Minimalist.Cat.V
• Minimalist.uposToCat UD.UPOS.AUX = Minimalist.Cat.T
• Minimalist.uposToCat UD.UPOS.NOUN = Minimalist.Cat.N
• Minimalist.uposToCat UD.UPOS.PROPN = Minimalist.Cat.N
• Minimalist.uposToCat UD.UPOS.ADJ = Minimalist.Cat.A
• Minimalist.uposToCat UD.UPOS.ADP = Minimalist.Cat.P
• Minimalist.uposToCat UD.UPOS.DET = Minimalist.Cat.D
• Minimalist.uposToCat UD.UPOS.SCONJ = Minimalist.Cat.C
• Minimalist.uposToCat UD.UPOS.CCONJ = Minimalist.Cat.C
• Minimalist.uposToCat x✝ = Minimalist.Cat.N

def Minimalist.LIToken.phonForm (tok : LIToken) : String

Extract the phonological form from an LIToken.

Equations

• tok.phonForm = (Option.map (fun (x : Minimalist.SimpleLI) => x.phonForm) tok.item.features.head?).getD ""

def Minimalist.LIToken.selects (selector selected : LIToken) : Prop

LIToken-level c-selection: selector selects selected iff selector's outermost selectional feature equals selected's outer category. A pure LIToken relation; no SO structure involved.

Equations

• selector.selects selected = (List.head? selector.item.outerSel = some selected.item.outerCat)

@[implicit_reducible]

instance Minimalist.instDecidableSelects (lt1 lt2 : LIToken) : Decidable (lt1.selects lt2)

Equations

• Minimalist.instDecidableSelects lt1 lt2 = id inferInstance

def Minimalist.mkTraceToken (index : ℕ) : LIToken

Trace marker token: the canonical LIToken read off a bare trace vertex when a selection check needs an LIToken at that position. The index is recorded in the id field (sentinel ≥ 10000) but is not part of chain identity — MCB chain identity is workspace-level (Def 1.2.1), and the SO carrier's trace leaf is bare/index-free. Selection reads only the token's category (.N) and outerSel ([]), both index-independent.

Equations

• Minimalist.mkTraceToken index = { item := Minimalist.LexicalItem.simple Minimalist.Cat.N [], id := index + 10000 }