Feature-checking slots

[Cho00] [MCB25]

A feature-checking slot records the state of one feature dimension on a lexical item. Unlike a plain determinate slot (Core/Order/Flat.lean's Flat, which is two-state — bottom or a value), a feature dimension under Agree is in one of three states:

• absent — the item lacks the dimension (the order bottom ⊥);
• unvalued — a probe: the dimension is present but valueless ([Cho00]'s unvalued/uninterpretable feature, which searches for a goal);
• valued v — the dimension is present with value v.

FeatureSlot is polymorphic in the value type α, so it is reusable across feature spaces (φ-features, case, categorial features, …) and carries no commitment to any particular inventory.

Why this is decoupled from the Merge carrier

Per [MCB25] (book p. 13), the valued/unvalued feature-checking apparatus is the Stabler-Minimalism layer: label-matching makes Merge partially defined, forcing "an algebraically more complex Hopf algebra and … a family of right-ideal coideals … which keep track of the feature checking problem." MCB's own free-Merge core (the SMT) keeps SO₀ features atomic — Merge is free, with no feature checking. So feature-checking slots are an Agree-layer structure, kept general here and decoupled from the SyntacticObject carrier rather than baked into it.

Subsumption order

absent (⊥) < unvalued < valued v, with distinct valued values forming an antichain: a probe is more specified than an absent dimension and less specified than a value, and two values are incomparable. This is the per-slot order that the bundle subsumption order (Features.BundleLike.Subsumes) is built from.

inductive Features.FeatureSlot (α : Type u_1) : Type u_1

A feature-checking slot for value type α: absent / unvalued (probe) / valued v. See the module docstring.

• absent {α : Type u_1} : FeatureSlot α
• unvalued {α : Type u_1} : FeatureSlot α
• valued {α : Type u_1} (v : α) : FeatureSlot α

@[implicit_reducible]

instance Features.instReprFeatureSlot {α✝ : Type u_1} [Repr α✝] : Repr (FeatureSlot α✝)

Equations

• Features.instReprFeatureSlot = { reprPrec := Features.instReprFeatureSlot.repr }

def Features.instReprFeatureSlot.repr {α✝ : Type u_1} [Repr α✝] : FeatureSlot α✝ → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Features.instDecidableEqFeatureSlot {α✝ : Type u_1} [DecidableEq α✝] : DecidableEq (FeatureSlot α✝)

Equations

• Features.instDecidableEqFeatureSlot = Features.instDecidableEqFeatureSlot.decEq

def Features.instDecidableEqFeatureSlot.decEq {α✝ : Type u_1} [DecidableEq α✝] (x✝ x✝¹ : FeatureSlot α✝) : Decidable (x✝ = x✝¹)

Equations

• Features.instDecidableEqFeatureSlot.decEq Features.FeatureSlot.absent Features.FeatureSlot.absent = isTrue ⋯
• Features.instDecidableEqFeatureSlot.decEq Features.FeatureSlot.absent Features.FeatureSlot.unvalued = isFalse ⋯
• Features.instDecidableEqFeatureSlot.decEq Features.FeatureSlot.absent (Features.FeatureSlot.valued v) = isFalse ⋯
• Features.instDecidableEqFeatureSlot.decEq Features.FeatureSlot.unvalued Features.FeatureSlot.absent = isFalse ⋯
• Features.instDecidableEqFeatureSlot.decEq Features.FeatureSlot.unvalued Features.FeatureSlot.unvalued = isTrue ⋯
• Features.instDecidableEqFeatureSlot.decEq Features.FeatureSlot.unvalued (Features.FeatureSlot.valued v) = isFalse ⋯
• Features.instDecidableEqFeatureSlot.decEq (Features.FeatureSlot.valued v) Features.FeatureSlot.absent = isFalse ⋯
• Features.instDecidableEqFeatureSlot.decEq (Features.FeatureSlot.valued v) Features.FeatureSlot.unvalued = isFalse ⋯
• Features.instDecidableEqFeatureSlot.decEq (Features.FeatureSlot.valued a) (Features.FeatureSlot.valued b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Features.FeatureSlot.instBot {α : Type u_1} : Bot (FeatureSlot α)

Equations

• Features.FeatureSlot.instBot = { bot := Features.FeatureSlot.absent }

@[simp]

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

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

The slot specifies a (present) feature: it is not absent.

Equations

• Features.FeatureSlot.absent.isSpecified = false
• x✝.isSpecified = true

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

The slot is a probe (present but unvalued).

Equations

• Features.FeatureSlot.unvalued.isUnvalued = true
• x✝.isUnvalued = false

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

The slot carries a value.

Equations

• (Features.FeatureSlot.valued v).isValued = true
• x✝.isValued = false

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

The value, when the slot is valued.

Equations

• (Features.FeatureSlot.valued v).value? = some v
• x✝.value? = none

inductive Features.FeatureSlot.LE {α : Type u_1} : FeatureSlot α → FeatureSlot α → Prop

Subsumption: absent ≤ unvalued ≤ valued v, with distinct values incomparable. The reflexive-transitive order on the three checking states.

• absent_le {α : Type u_1} (s : FeatureSlot α) : absent.LE s
• unvalued_le_unvalued {α : Type u_1} : unvalued.LE unvalued
• unvalued_le_valued {α : Type u_1} (v : α) : unvalued.LE (valued v)
• valued_le_valued {α : Type u_1} (v : α) : (valued v).LE (valued v)

@[implicit_reducible]

instance Features.FeatureSlot.instLE {α : Type u_1} : LE (FeatureSlot α)

Equations

• Features.FeatureSlot.instLE = { le := Features.FeatureSlot.LE }

theorem Features.FeatureSlot.le_def {α : Type u_1} {a b : FeatureSlot α} : a ≤ b ↔ a.LE b

theorem Features.FeatureSlot.le_refl {α : Type u_1} (a : FeatureSlot α) : a ≤ a

theorem Features.FeatureSlot.le_trans {α : Type u_1} {a b c : FeatureSlot α} (hab : a ≤ b) (hbc : b ≤ c) : a ≤ c

theorem Features.FeatureSlot.le_antisymm {α : Type u_1} {a b : FeatureSlot α} (hab : a ≤ b) (hba : b ≤ a) : a = b

@[implicit_reducible]

instance Features.FeatureSlot.instPartialOrder {α : Type u_1} : PartialOrder (FeatureSlot α)

Equations

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

@[implicit_reducible]

instance Features.FeatureSlot.instOrderBot {α : Type u_1} : OrderBot (FeatureSlot α)

Equations

• Features.FeatureSlot.instOrderBot = { toBot := Features.FeatureSlot.instBot, bot_le := ⋯ }

@[implicit_reducible]

instance Features.FeatureSlot.instDecidableLeOfDecidableEq {α : Type u_1} [DecidableEq α] (a b : FeatureSlot α) : Decidable (a ≤ b)

Equations

• Features.FeatureSlot.absent.instDecidableLeOfDecidableEq b = isTrue ⋯
• Features.FeatureSlot.unvalued.instDecidableLeOfDecidableEq Features.FeatureSlot.unvalued = isTrue ⋯
• Features.FeatureSlot.unvalued.instDecidableLeOfDecidableEq (Features.FeatureSlot.valued v) = isTrue ⋯
• Features.FeatureSlot.unvalued.instDecidableLeOfDecidableEq Features.FeatureSlot.absent = isFalse ⋯
• (Features.FeatureSlot.valued v).instDecidableLeOfDecidableEq (Features.FeatureSlot.valued w) = if h : v = w then isTrue ⋯ else isFalse ⋯
• (Features.FeatureSlot.valued v).instDecidableLeOfDecidableEq Features.FeatureSlot.absent = isFalse ⋯
• (Features.FeatureSlot.valued v).instDecidableLeOfDecidableEq Features.FeatureSlot.unvalued = isFalse ⋯

@[simp]

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