Feature-checking slots

A feature-checking slot records the state of one feature dimension on a lexical item. Under Agree a dimension is in one of three states: absent, when the item lacks it; unvalued, a probe, present but valueless (Chomsky's unvalued feature, which searches for a goal); and valued v. A determinate slot of Core/Order/Flat.lean has two states, bottom or a value, so a checking slot is a flat slot with a new bottom below it: WithBot (Flat α), as EReal is WithBot (WithTop ℝ). Its subsumption order is therefore absent < unvalued < valued v with distinct values incomparable, the per-slot order the bundle subsumption order is built from.

Following Marcolli, Chomsky and Berwick, the free-Merge core keeps the features of a syntactic object atomic, and the valued/unvalued apparatus belongs to the Agree layer, so slots are kept general here, polymorphic in the value type, and decoupled from the SyntacticObject carrier.

Main definitions

• Minimalist.FeatureSlot — WithBot (Flat α), with the patterns absent, unvalued, valued and the eliminator FeatureSlot.rec'
• Minimalist.FeatureSlot.valueWith — valuation of an unvalued slot

References

• [Cho00]
• [MCB25]

@[reducible, inline]

abbrev Minimalist.FeatureSlot (α : Type u_1) : Type u_1

A feature-checking slot for value type α is absent, unvalued (a probe), or valued v: a flat slot with a new bottom below it.

Equations

• Minimalist.FeatureSlot α = WithBot (Flat α)

@[reducible, match_pattern, inline]

abbrev Minimalist.FeatureSlot.absent {α : Type u_1} : FeatureSlot α

An item lacking the dimension has the absent slot.

Equations

• Minimalist.FeatureSlot.absent = none

@[reducible, match_pattern, inline]

abbrev Minimalist.FeatureSlot.unvalued {α : Type u_1} : FeatureSlot α

A probe has the unvalued slot, present but valueless.

Equations

• Minimalist.FeatureSlot.unvalued = ↑⊥

@[reducible, match_pattern, inline]

abbrev Minimalist.FeatureSlot.valued {α : Type u_1} (v : α) : FeatureSlot α

The valued v slot carries the value v.

Equations

• Minimalist.FeatureSlot.valued v = ↑↑v

def Minimalist.FeatureSlot.rec' {α : Type u_1} {motive : FeatureSlot α → Sort u_2} (absent : motive absent) (unvalued : motive unvalued) (valued : (v : α) → motive (valued v)) (s : FeatureSlot α) : motive s

A slot is absent, unvalued, or valued.

Equations

• Minimalist.FeatureSlot.rec' absent unvalued valued none = absent
• Minimalist.FeatureSlot.rec' absent unvalued valued (some none) = unvalued
• Minimalist.FeatureSlot.rec' absent unvalued valued (some (some v)) = valued v

@[simp]

theorem Minimalist.FeatureSlot.bot_eq_absent {α : Type u_1} : ⊥ = absent

@[simp]

theorem Minimalist.FeatureSlot.unvalued_ne_absent {α : Type u_1} : unvalued ≠ absent

@[simp]

theorem Minimalist.FeatureSlot.valued_ne_absent {α : Type u_1} (v : α) : valued v ≠ absent

@[simp]

theorem Minimalist.FeatureSlot.valued_ne_unvalued {α : Type u_1} (v : α) : valued v ≠ unvalued

@[simp]

theorem Minimalist.FeatureSlot.valued_inj {α : Type u_1} {v w : α} : valued v = valued w ↔ v = w

def Minimalist.FeatureSlot.isSpecified {α : Type u_1} : FeatureSlot α → Bool

The slot specifies a present feature, that is, it is not absent.

Equations

• Minimalist.FeatureSlot.isSpecified none = false
• x✝.isSpecified = true

def Minimalist.FeatureSlot.isUnvalued {α : Type u_1} : FeatureSlot α → Bool

The slot is a probe (present but unvalued).

Equations

• Minimalist.FeatureSlot.isUnvalued (some none) = true
• x✝.isUnvalued = false

def Minimalist.FeatureSlot.isValued {α : Type u_1} : FeatureSlot α → Bool

The slot carries a value.

Equations

• Minimalist.FeatureSlot.isValued (some (some val)) = true
• x✝.isValued = false

def Minimalist.FeatureSlot.value? {α : Type u_1} : FeatureSlot α → Option α

The value of a slot, when it is valued.

Equations

• Minimalist.FeatureSlot.value? (some (some val)) = some val
• x✝.value? = none

def Minimalist.FeatureSlot.valueWith {α : Type u_1} (v : α) : FeatureSlot α → FeatureSlot α

Valuing a slot with v fills it when it is unvalued and leaves an absent or valued slot as it is.

Equations

• Minimalist.FeatureSlot.valueWith v (some none) = Minimalist.FeatureSlot.valued v
• Minimalist.FeatureSlot.valueWith v x✝ = x✝

@[simp]

theorem Minimalist.FeatureSlot.valueWith_absent {α : Type u_1} (v : α) : valueWith v absent = absent

@[simp]

theorem Minimalist.FeatureSlot.valueWith_unvalued {α : Type u_1} (v : α) : valueWith v unvalued = valued v

@[simp]

theorem Minimalist.FeatureSlot.valueWith_valued {α : Type u_1} (v w : α) : valueWith v (valued w) = valued w

theorem Minimalist.FeatureSlot.valueWith_of_ne_unvalued {α : Type u_1} (v : α) {s : FeatureSlot α} (h : s ≠ unvalued) : valueWith v s = s

theorem Minimalist.FeatureSlot.le_valueWith {α : Type u_1} (v : α) (s : FeatureSlot α) : s ≤ valueWith v s

Valuation is inflationary in the subsumption order.

@[simp]

theorem Minimalist.FeatureSlot.isSpecified_iff_ne_bot {α : Type u_1} {s : FeatureSlot α} : s.isSpecified = true ↔ s ≠ ⊥