Lexical items

The leaves of syntactic objects are drawn from SO₀, the lexical items and syntactic features. A lexical item is a category with its selectional stack, its phonological form and its [wh] and [E] features, and a token of it is the item with the index that tells its tokens apart. The carrier built over tokens is SyntacticObject/Basic.lean.

Main definitions

• Minimalist.LexicalItem, Minimalist.LexicalItem.Token

References

• [MCB25], §1.1 (Definition 1.1.1)
• [Mer01]

structure Minimalist.LexicalItem : Type

A lexical item is a category with its selectional stack, a phonological form, empty for a silent item, and the [wh] and [E] features.

• cat : Cat

  The category.

• sel : SelStack

  The selectional stack, consumed left to right.

• phonForm : String

  The phonological form, empty for a silent item.

• wh : Bool

  The [wh] feature, read by wh-movement and the multiple-wh-fronting parameter.

• ellipsis : Bool

  The [E] feature, which leaves the head's complement unpronounced ([Mer01]).

@[instance_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.

@[instance_reducible]

instance Minimalist.instDecidableEqLexicalItem : DecidableEq LexicalItem

Equations

• Minimalist.instDecidableEqLexicalItem = Minimalist.instDecidableEqLexicalItem.decEq

def Minimalist.instDecidableEqLexicalItem.decEq (x✝ x✝¹ : LexicalItem) : Decidable (x✝ = x✝¹)

Equations

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

def Minimalist.LexicalItem.of (cat : Cat) (sel : SelStack) (phonForm : String := "") (wh ellipsis : Bool := false) : LexicalItem

The lexical item of a category and selectional stack, silent and without [wh] or [E] unless the optional arguments say otherwise.

Equations

• Minimalist.LexicalItem.of cat sel phonForm wh ellipsis = { cat := cat, sel := sel, phonForm := phonForm, wh := wh, ellipsis := ellipsis }

def Minimalist.LexicalItem.phonForm? (li : LexicalItem) : Option String

The phonological form of a pronounced item, none for a silent one.

Equations

• li.phonForm? = if li.phonForm.isEmpty = true then none else some li.phonForm

structure Minimalist.LexicalItem.Token : Type

A token of a lexical item. Syntactic objects are compared as values, so two occurrences of one item, the two thes of a transitive clause, are different leaves only through their tokens; the index tells apart the tokens of one item, and tokens of different items differ anyway.

• item : LexicalItem

  The lexical item.

• id : ℕ

  The index among the tokens of item.

@[instance_reducible]

instance Minimalist.LexicalItem.instReprToken : Repr Token

Equations

• Minimalist.LexicalItem.instReprToken = { reprPrec := Minimalist.LexicalItem.instReprToken.repr }

def Minimalist.LexicalItem.instReprToken.repr : Token → ℕ → Std.Format

Equations

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

def Minimalist.LexicalItem.instDecidableEqToken.decEq (x✝ x✝¹ : Token) : Decidable (x✝ = x✝¹)

Equations

• Minimalist.LexicalItem.instDecidableEqToken.decEq { item := a, id := a_1 } { item := b, id := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance Minimalist.LexicalItem.instDecidableEqToken : DecidableEq Token

Equations

• Minimalist.LexicalItem.instDecidableEqToken = Minimalist.LexicalItem.instDecidableEqToken.decEq

def Minimalist.LexicalItem.Token.bareTrace : Token

The placeholder head of a bare trace, which remembers no token. Selection reads it as a saturated silent noun, and its index lies above those lexical tokens use, so it equals none of them.

Equations

• Minimalist.LexicalItem.Token.bareTrace = { item := Minimalist.LexicalItem.of Minimalist.Cat.N [], id := 10000 }