inductive Minimalism.BarLevel : Type

Bar level in X-Bar theory

• zero: X (head, minimal projection)
• bar: X' (intermediate projection)
• max: XP (maximal projection, phrase)

• zero : BarLevel
• bar : BarLevel
• max : BarLevel

instance Minimalism.instReprBarLevel : Repr BarLevel

Equations

• Minimalism.instReprBarLevel = { reprPrec := Minimalism.instReprBarLevel.repr }

def Minimalism.instReprBarLevel.repr : BarLevel → ℕ → Std.Format

Equations

• Minimalism.instReprBarLevel.repr Minimalism.BarLevel.zero prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalism.BarLevel.zero")).group prec✝
• Minimalism.instReprBarLevel.repr Minimalism.BarLevel.bar prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalism.BarLevel.bar")).group prec✝
• Minimalism.instReprBarLevel.repr Minimalism.BarLevel.max prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalism.BarLevel.max")).group prec✝

instance Minimalism.instDecidableEqBarLevel : DecidableEq BarLevel

Equations

• Minimalism.instDecidableEqBarLevel x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Minimalism.instInhabitedBarLevel : Inhabited BarLevel

Equations

• Minimalism.instInhabitedBarLevel = { default := Minimalism.instInhabitedBarLevel.default }

def Minimalism.instInhabitedBarLevel.default : BarLevel

Equations

• Minimalism.instInhabitedBarLevel.default = Minimalism.BarLevel.zero

def Minimalism.BarLevel.toString : BarLevel → String

String representation for bar levels

Equations

• Minimalism.BarLevel.zero.toString = "X⁰"
• Minimalism.BarLevel.bar.toString = "X'"
• Minimalism.BarLevel.max.toString = "XP"

instance Minimalism.instToStringBarLevel : ToString BarLevel

Equations

• Minimalism.instToStringBarLevel = { toString := Minimalism.BarLevel.toString }

structure Minimalism.XBarPhrase : Type

An X-Bar phrase with explicit Spec-Head-Complement structure

This captures the traditional X-Bar schema:

• head: The lexical head X
• complement: The sister of X (selected by X)
• specifier: The sister of X' (in Spec position)
• cat: The category of the phrase

• cat : Cat
• head : SyntacticObject
• complement : Option SyntacticObject
• specifier : Option SyntacticObject

instance Minimalism.instReprXBarPhrase : Repr XBarPhrase

Equations

• Minimalism.instReprXBarPhrase = { reprPrec := Minimalism.instReprXBarPhrase.repr }

def Minimalism.instReprXBarPhrase.repr : XBarPhrase → ℕ → Std.Format

Equations

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

def Minimalism.XBarPhrase.fromHead (h : SyntacticObject) : Option XBarPhrase

Create an X-Bar phrase from a head only (no complement or specifier)

Equations

• Minimalism.XBarPhrase.fromHead h = match h.getLIToken with | some tok => some { cat := tok.item.outerCat, head := h } | none => none

def Minimalism.XBarPhrase.addComplement (xp : XBarPhrase) (comp : SyntacticObject) : XBarPhrase

Add a complement to an X-Bar phrase (head + complement = X')

Equations

• xp.addComplement comp = { cat := xp.cat, head := xp.head, complement := some comp, specifier := xp.specifier }

def Minimalism.XBarPhrase.addSpecifier (xp : XBarPhrase) (spec : SyntacticObject) : XBarPhrase

Add a specifier to an X-Bar phrase (X' + specifier = XP)

Equations

• xp.addSpecifier spec = { cat := xp.cat, head := xp.head, complement := xp.complement, specifier := some spec }

def Minimalism.barLevelIn (so root : SyntacticObject) : BarLevel

Compute the bar level of a syntactic object relative to a root

• A leaf is minimal (zero)
• A node where the head projects further is intermediate (bar)
• A node where the head doesn't project further is maximal (max)

Equations

• One or more equations did not get rendered due to their size.
• Minimalism.barLevelIn (Minimalism.SyntacticObject.leaf a) root = if (Minimalism.SyntacticObject.leaf a).isLeaf = true then Minimalism.BarLevel.zero else Minimalism.BarLevel.zero

def Minimalism.barLevelSimple (so : SyntacticObject) : BarLevel

Alternative: determine bar level from structure alone

Equations

• One or more equations did not get rendered due to their size.
• Minimalism.barLevelSimple (Minimalism.SyntacticObject.leaf a) = Minimalism.BarLevel.zero

def Minimalism.getSpecifier (so : SyntacticObject) : Option SyntacticObject

Get the specifier of a node (the non-projecting daughter)

In {Spec, X'}, the specifier is the daughter that doesn't share the label with the parent.

Equations

• One or more equations did not get rendered due to their size.
• Minimalism.getSpecifier (Minimalism.SyntacticObject.leaf a) = none

def Minimalism.getComplement (so : SyntacticObject) : Option SyntacticObject

Get the complement of a node (the selected daughter)

In {X, Complement}, the complement is the daughter selected by the head.

Equations

• Minimalism.getComplement (Minimalism.SyntacticObject.leaf a) = none
• Minimalism.getComplement (a.node a_1) = if Minimalism.selectsB a a_1 = true then some a_1 else if Minimalism.selectsB a_1 a = true then some a else none

def Minimalism.getHead (so : SyntacticObject) : Option SyntacticObject

Get the head of a phrase (the projecting minimal element)

Equations

• One or more equations did not get rendered due to their size.
• Minimalism.getHead (Minimalism.SyntacticObject.leaf a) = some (Minimalism.SyntacticObject.leaf a)

def Minimalism.XBarPhrase.isWellFormed (xp : XBarPhrase) : Bool

An X-Bar phrase is well-formed if:

1. The head has the appropriate category
2. The complement (if present) is selected by the head
3. Structure is binary branching

Equations

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

def Minimalism.XBarPhrase.toSyntacticObject (xp : XBarPhrase) : SyntacticObject

Build a SyntacticObject from an XBarPhrase

Constructs the tree bottom-up:

1. Head alone = X
2. Head + Complement = X' (merge head with complement)
3. X' + Specifier = XP (merge specifier with X')

Equations

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

def Minimalism.analyzeAsXBar (so : SyntacticObject) : Option XBarPhrase

Analyze a SyntacticObject as an X-Bar phrase

Equations

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

theorem Minimalism.selection_gives_complement (h c : SyntacticObject) (hSel : selectsB h c = true) : getComplement (merge h c) = some c

Selection determines complement position

theorem Minimalism.heads_are_minimal (tok : LIToken) : barLevelSimple (SyntacticObject.leaf tok) = BarLevel.zero

Heads are minimal (zero bar level)

theorem Minimalism.spec_xbar_is_maximal (spec xbar : SyntacticObject) (hSpec : spec.isNode = true) : barLevelSimple (merge spec xbar) = BarLevel.max

Phrases built from specifier+X' are maximal

def Minimalism.exampleDP : XBarPhrase

Example: Building "the cat" as a DP

[D the] + [N cat] = [DP [D the] [N cat]] D selects N, so D projects

Equations

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

def Minimalism.exampleVP : XBarPhrase

Example: "John saw Mary" as a simple clause sketch

V selects D (object), so in [V saw] + [D Mary]: V projects, making VP

Equations

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