Docs / Syntax / Feature / Slot

Feature-checking slots

import Linglib.Syntax.Feature.Slot

This file defines the checking slot of one feature dimension on an item and its valuation. The slot is absent when the item lacks the dimension, unvalued when the item bears the dimension without a value, and valued v when it bears the value v. A probe bears an unvalued slot, and a nominal whose case has not been assigned bears an unvalued case slot.

A checking slot is a flat slot (Core/Order/Flat.lean) with a new bottom element, so its type is WithBot (Flat α). Its order is absent < unvalued < valued v, and distinct values are incomparable.

The map toFlat forgets whether the dimension is borne: it sends absent and unvalued to ⊥. It has a left adjoint ofFlat, which sends ⊥ to absent, and a right adjoint, the coercion, which sends ⊥ to unvalued. Both adjoints are sections of toFlat.

Valuing a slot with v unifies it with valued v. An unvalued slot becomes valued v, a slot valued v is unchanged, and a slot valued w ≠ v fails, which is ⊤. An absent slot is unchanged, since an item that lacks a dimension cannot be valued in it. On a borne slot, valuation is flat unification.

Main definitions

FeatureSlot: the checking slots with values in α.
FeatureSlot.toFlat: the value of a slot as a flat slot.
FeatureSlot.ofFlat: a flat slot as a checking slot.
FeatureSlot.gciOfFlat: ofFlat and toFlat form a Galois coinsertion.
FeatureSlot.giToFlat: toFlat and the coercion form a Galois insertion.
FeatureSlot.valueWith: a slot valued with v.

Implementation notes

FeatureSlot α unfolds to Option (Option α), so the literal none typechecks as a slot and denotes absent, not unvalued. Write the named slots.

References

Chomsky 2000, Minimalist Inquiries: The Framework

Declarations

A checking slot with values in α: absent, unvalued, or valued v.

@[reducible, inline] abbrev FeatureSlot L48–49

(α : Type u_1) :

Type u_1

FeatureSlot α = WithBot (Flat α)

Used by FeatureSlot.absent, FeatureSlot.unvalued, FeatureSlot.valued, FeatureSlot.rec', FeatureSlot.instDecidableEq, FeatureSlot.decidableEqAbsent, FeatureSlot.decidableEqUnvalued, FeatureSlot.valued_le_iff, FeatureSlot.value?, FeatureSlot.offer, FeatureSlot.map, FeatureSlot.map_eq_valued_iff, FeatureSlot.map_eq_unvalued_iff, FeatureSlot.value?_map, FeatureSlot.map_map, FeatureSlot.toFlat, FeatureSlot.ofFlat, FeatureSlot.valueWith, FeatureSlot.valueWith_of_ne_absent, FeatureSlot.valueWith_eq_top_iff, FeatureSlot.le_of_valueWith_eq_coe, FeatureSlot.map_toFlat_valueWith

Used in Syntax/Case/Assignment, Syntax/Case/Dependent, Syntax/Minimalist/Case/Assignment, Syntax/Minimalist/Case/SyntacticObject, Syntax/Minimalist/Feature/Basic and 11 more

The slot of an item that lacks the dimension.

@[reducible, match_pattern, inline] abbrev FeatureSlot.absent L55–56

{α : Type u_1} :

FeatureSlot.absent = none

Built from

Used by FeatureSlot.rec', FeatureSlot.bot_eq_absent, FeatureSlot.unvalued_ne_absent, FeatureSlot.valued_ne_absent, FeatureSlot.absent_ne_valued, FeatureSlot.absent_ne_unvalued, FeatureSlot.decidableEqAbsent, FeatureSlot.value?_absent, FeatureSlot.offer_ne_absent, FeatureSlot.map, FeatureSlot.map_absent, FeatureSlot.ofFlat, FeatureSlot.ofFlat_bot, FeatureSlot.toFlat_absent, FeatureSlot.valueWith, FeatureSlot.valueWith_of_ne_absent, FeatureSlot.valueWith_absent, FeatureSlot.map_toFlat_valueWith

Used in Syntax/Case/Assignment, Syntax/Minimalist/Feature/Valuation, BakerVinokurova2010

The slot of an item that bears the dimension without a value.

@[reducible, match_pattern, inline] abbrev FeatureSlot.unvalued L58–59

{α : Type u_1} :

FeatureSlot.unvalued = ↑⊥

Built from

Used by FeatureSlot.rec', FeatureSlot.unvalued_ne_absent, FeatureSlot.valued_ne_unvalued, FeatureSlot.absent_ne_unvalued, FeatureSlot.unvalued_ne_valued, FeatureSlot.decidableEqUnvalued, FeatureSlot.value?_unvalued, FeatureSlot.offer, FeatureSlot.offer_none, FeatureSlot.unvalued_le_valued, FeatureSlot.unvalued_le_offer, FeatureSlot.map, FeatureSlot.map_unvalued, FeatureSlot.map_eq_unvalued_iff, FeatureSlot.toFlat_unvalued, FeatureSlot.valueWith_unvalued

Used in Syntax/Case/Assignment, Syntax/Case/Dependent, Syntax/Minimalist/Case/Assignment, Syntax/Minimalist/Feature/Valuation, Syntax/Minimalist/Probe/Phi and 6 more

The slot of an item that bears the value v.

@[reducible, match_pattern, inline] abbrev FeatureSlot.valued L61–62

{α : Type u_1} (v : α) :

FeatureSlot.valued v = ↑↑v

Built from

Used by FeatureSlot.rec', FeatureSlot.valued_ne_absent, FeatureSlot.absent_ne_valued, FeatureSlot.valued_ne_unvalued, FeatureSlot.unvalued_ne_valued, FeatureSlot.valued_inj, FeatureSlot.valued_le_iff, FeatureSlot.value?_valued, FeatureSlot.offer, FeatureSlot.offer_some, FeatureSlot.offer_eq_valued_iff, FeatureSlot.unvalued_le_valued, FeatureSlot.map, FeatureSlot.map_valued, FeatureSlot.map_eq_valued_iff, FeatureSlot.ofFlat, FeatureSlot.ofFlat_coe, FeatureSlot.toFlat_valued, FeatureSlot.valueWith, FeatureSlot.valueWith_of_ne_absent, FeatureSlot.valueWith_unvalued, FeatureSlot.valueWith_valued, FeatureSlot.valueWith_eq_top_iff

Used in Syntax/Case/Assignment, Syntax/Case/Dependent, Syntax/Minimalist/Case/Assignment, Syntax/Minimalist/Feature/Basic, Syntax/Minimalist/Feature/Valuation and 8 more

The flat slot underneath

The value of a slot as a flat slot, ⊥ if the slot is absent or unvalued.

def FeatureSlot.toFlat L177–178

{α : Type u_1} :

FeatureSlot α → Flat α

FeatureSlot.toFlat = WithBot.unbotD ⊥

Built from

Used by FeatureSlot.toFlat_absent, FeatureSlot.toFlat_unvalued, FeatureSlot.toFlat_valued, FeatureSlot.toFlat_coe, FeatureSlot.toFlat_ofFlat, FeatureSlot.gc_ofFlat_toFlat, FeatureSlot.gciOfFlat, FeatureSlot.giToFlat, FeatureSlot.map_toFlat_valueWith

Used in Syntax/Minimalist/Feature/Basic, Syntax/Minimalist/Probe/Phi, Amato2025

A flat slot as a checking slot, absent where the flat slot is ⊥.

def FeatureSlot.ofFlat L180–181

{α : Type u_1} :

Flat α → FeatureSlot α

FeatureSlot.ofFlat x = Flat.recBotCoe FeatureSlot.absent FeatureSlot.valued x

Built from , ,

Used by FeatureSlot.ofFlat_bot, FeatureSlot.ofFlat_coe, FeatureSlot.toFlat_ofFlat, FeatureSlot.gc_ofFlat_toFlat, FeatureSlot.gciOfFlat

Used in Syntax/Minimalist/Feature/Basic

ofFlat and toFlat form a Galois coinsertion.

def FeatureSlot.gciOfFlat L207–209

{α : Type u_1} :

GaloisCoinsertion ofFlat toFlat

FeatureSlot.gciOfFlat = ⋯.toGaloisCoinsertion ⋯

Built from ,

toFlat and the coercion form a Galois insertion.

def FeatureSlot.giToFlat L211–213

{α : Type u_1} :

GaloisInsertion toFlat WithBot.some

FeatureSlot.giToFlat = WithBot.giUnbotDBot

Built from

Valuation

The slot s valued with v, or ⊤ if s is valued otherwise. An absent slot is unchanged.

def FeatureSlot.valueWith L221–224

{α : Type u_1} [DecidableEq α] (v : α) (s : FeatureSlot α) :

WithTop (FeatureSlot α)

FeatureSlot.valueWith v s = if s = FeatureSlot.absent then ↑s else PartialUnify.unify s (FeatureSlot.valued v)

Built from , ,

Used by FeatureSlot.valueWith_of_ne_absent, FeatureSlot.valueWith_absent, FeatureSlot.valueWith_unvalued, FeatureSlot.valueWith_valued, FeatureSlot.valueWith_eq_top_iff, FeatureSlot.le_of_valueWith_eq_coe, FeatureSlot.valueWith_mono, FeatureSlot.map_toFlat_valueWith

Used in Syntax/Minimalist/Feature/Valuation

theorem FeatureSlot.map_toFlat_valueWith L275–286

{α : Type u_1} [DecidableEq α] {v : α} {s : FeatureSlot α} (hs : s ≠ absent) :

WithTop.map toFlat (valueWith v s) = PartialUnify.unify s.toFlat ↑v

Built from , , ,