Documentation

Linglib.Syntax.Minimalist.Features

Feature Infrastructure for Minimalist Agree #

[Adg03] [Cho95] [Cho00] [Cho01] [Alo20] [AB26] [Lob95] [Pan15] [Pol89]

Phi-features, case values, and feature bundles — the shared infrastructure underlying all Agree-based operations. Extracted from Agree.lean to separate the feature types (what can be checked) from the Agree operation (how checking works) and the failure model (what happens when checking fails — a Probe.outcome of unvalued; see Probe/Basic.lean).

±Interpretable Features ([Cho95] Ch 4 §4.5) #

The ±Interpretable distinction is orthogonal to valued/unvalued:

+Interpretable: contributes to meaning, survives to LF. Categorial features ([N], [V], [D], [C]) and φ-features of nouns.
–Interpretable: must be checked and deleted before LF. Case features, φ-features of T/v, strong [nominal-] features.

Interpretability is determined by the combination of feature type and host category: person on N is +Interpretable, person on T is –Interpretable. isInterpretableOn encodes this mapping.

Design Decision: `Person` replaces `Nat` #

PhiFeature.person uses Person (.first |.second |.third) rather than a raw Nat. This eliminates the possibility of meaningless person values (e.g., person 47) and grounds the feature inventory in the same canonical type used across the library:

Person — framework-agnostic person hierarchy
Phi.Geometry.DecomposedPerson — [Pre14]'s [±participant, ±author] decomposition, now mapping from Person
DifferentialIndexing.IndexingPersonLevel — [Jus24]'s SAP/3rd binary split, bridged to Person

For unvalued (probe) features, the value is irrelevant — FeatureVal.sameType matches any .person _ against any .person _ and any .number _ against any .number _, ignoring specific values. Use .person .third and .number .sg as conventional placeholders for probes.

inductive Minimalist.PhiFeature :

Phi-features (agreement features).

person : Person → PhiFeature
number : Number → PhiFeature
gender : ℕ → PhiFeature

Instances For

def Minimalist.instReprPhiFeature.repr :

PhiFeature → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Minimalist.instReprPhiFeature :

Repr PhiFeature

Equations

Minimalist.instReprPhiFeature = { reprPrec := Minimalist.instReprPhiFeature.repr }

def Minimalist.instDecidableEqPhiFeature.decEq (x✝ x✝¹ : PhiFeature) :

Decidable (x✝ = x✝¹)

Equations

Minimalist.instDecidableEqPhiFeature.decEq (Minimalist.PhiFeature.person a) (Minimalist.PhiFeature.person b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
Minimalist.instDecidableEqPhiFeature.decEq (Minimalist.PhiFeature.person a) (Minimalist.PhiFeature.number a_1) = isFalse ⋯
Minimalist.instDecidableEqPhiFeature.decEq (Minimalist.PhiFeature.person a) (Minimalist.PhiFeature.gender a_1) = isFalse ⋯
Minimalist.instDecidableEqPhiFeature.decEq (Minimalist.PhiFeature.number a) (Minimalist.PhiFeature.person a_1) = isFalse ⋯
Minimalist.instDecidableEqPhiFeature.decEq (Minimalist.PhiFeature.number a) (Minimalist.PhiFeature.number b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
Minimalist.instDecidableEqPhiFeature.decEq (Minimalist.PhiFeature.number a) (Minimalist.PhiFeature.gender a_1) = isFalse ⋯
Minimalist.instDecidableEqPhiFeature.decEq (Minimalist.PhiFeature.gender a) (Minimalist.PhiFeature.person a_1) = isFalse ⋯
Minimalist.instDecidableEqPhiFeature.decEq (Minimalist.PhiFeature.gender a) (Minimalist.PhiFeature.number a_1) = isFalse ⋯
Minimalist.instDecidableEqPhiFeature.decEq (Minimalist.PhiFeature.gender a) (Minimalist.PhiFeature.gender b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

Instances For

@[implicit_reducible]

instance Minimalist.instDecidableEqPhiFeature :

DecidableEq PhiFeature

Equations

Minimalist.instDecidableEqPhiFeature = Minimalist.instDecidableEqPhiFeature.decEq

inductive Minimalist.HonLevel :

Honorific level: social ordering between speaker and referent. Relational, not absolute. ⟦iHON⟧ = λx. S_i ≺ x, where ≺ encodes social hierarchy.

nh : HonLevel
h : HonLevel
hh : HonLevel

Instances For

@[implicit_reducible]

instance Minimalist.instReprHonLevel :

Equations

Minimalist.instReprHonLevel = { reprPrec := Minimalist.instReprHonLevel.repr }

def Minimalist.instReprHonLevel.repr :

HonLevel → ℕ → Std.Format

Equations

Minimalist.instReprHonLevel.repr Minimalist.HonLevel.nh prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalist.HonLevel.nh")).group prec✝
Minimalist.instReprHonLevel.repr Minimalist.HonLevel.h prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalist.HonLevel.h")).group prec✝
Minimalist.instReprHonLevel.repr Minimalist.HonLevel.hh prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalist.HonLevel.hh")).group prec✝

Instances For

@[implicit_reducible]

instance Minimalist.instDecidableEqHonLevel :

DecidableEq HonLevel

Equations

Minimalist.instDecidableEqHonLevel x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive Minimalist.FeatureVal :

Feature values that can be checked via Agree

phi : PhiFeature → FeatureVal
case : Case → FeatureVal
wh : Bool → FeatureVal
q : Bool → FeatureVal
epp : Bool → FeatureVal
tense : Bool → FeatureVal
hon : HonLevel → FeatureVal
finite : Bool → FeatureVal
factive : Bool → FeatureVal
neg : Bool → FeatureVal
rel : Bool → FeatureVal
oblique : Bool → FeatureVal
ellipsis : Bool → FeatureVal
catN : Bool → FeatureVal
catV : Bool → FeatureVal
foc : Bool → FeatureVal
pol : Bool → FeatureVal
pov : Bool → FeatureVal
atomic : Bool → FeatureVal
minimal : Bool → FeatureVal
participant : Bool → FeatureVal
author : Bool → FeatureVal

Instances For

@[implicit_reducible]

instance Minimalist.instReprFeatureVal :

Repr FeatureVal

Equations

Minimalist.instReprFeatureVal = { reprPrec := Minimalist.instReprFeatureVal.repr }

def Minimalist.instReprFeatureVal.repr :

FeatureVal → ℕ → Std.Format

Equations

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

Instances For

def Minimalist.instDecidableEqFeatureVal.decEq (x✝ x✝¹ : FeatureVal) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

@[implicit_reducible]

instance Minimalist.instDecidableEqFeatureVal :

DecidableEq FeatureVal

Equations

Minimalist.instDecidableEqFeatureVal = Minimalist.instDecidableEqFeatureVal.decEq

def Minimalist.FeatureVal.sameType :

FeatureVal → FeatureVal → Bool

Do two feature values have the same type, ignoring specific values?

This is the correct matching predicate for Agree: a probe with [uPerson] should match any goal with [Person:x], regardless of the specific person value x. In contrast, DecidableEq (==) compares both type and value, which is wrong for Agree matching where the probe carries a placeholder value.

Equations

(Minimalist.FeatureVal.phi (Minimalist.PhiFeature.person a)).sameType (Minimalist.FeatureVal.phi (Minimalist.PhiFeature.person a_1)) = true
(Minimalist.FeatureVal.phi (Minimalist.PhiFeature.number a)).sameType (Minimalist.FeatureVal.phi (Minimalist.PhiFeature.number a_1)) = true
(Minimalist.FeatureVal.phi (Minimalist.PhiFeature.gender a)).sameType (Minimalist.FeatureVal.phi (Minimalist.PhiFeature.gender a_1)) = true
(Minimalist.FeatureVal.phi p1).sameType (Minimalist.FeatureVal.phi p2) = false
(Minimalist.FeatureVal.case a).sameType (Minimalist.FeatureVal.case a_1) = true
(Minimalist.FeatureVal.wh a).sameType (Minimalist.FeatureVal.wh a_1) = true
(Minimalist.FeatureVal.q a).sameType (Minimalist.FeatureVal.q a_1) = true
(Minimalist.FeatureVal.epp a).sameType (Minimalist.FeatureVal.epp a_1) = true
(Minimalist.FeatureVal.tense a).sameType (Minimalist.FeatureVal.tense a_1) = true
(Minimalist.FeatureVal.hon a).sameType (Minimalist.FeatureVal.hon a_1) = true
(Minimalist.FeatureVal.finite a).sameType (Minimalist.FeatureVal.finite a_1) = true
(Minimalist.FeatureVal.factive a).sameType (Minimalist.FeatureVal.factive a_1) = true
(Minimalist.FeatureVal.neg a).sameType (Minimalist.FeatureVal.neg a_1) = true
(Minimalist.FeatureVal.rel a).sameType (Minimalist.FeatureVal.rel a_1) = true
(Minimalist.FeatureVal.oblique a).sameType (Minimalist.FeatureVal.oblique a_1) = true
(Minimalist.FeatureVal.ellipsis a).sameType (Minimalist.FeatureVal.ellipsis a_1) = true
(Minimalist.FeatureVal.catN a).sameType (Minimalist.FeatureVal.catN a_1) = true
(Minimalist.FeatureVal.catV a).sameType (Minimalist.FeatureVal.catV a_1) = true
(Minimalist.FeatureVal.foc a).sameType (Minimalist.FeatureVal.foc a_1) = true
(Minimalist.FeatureVal.pol a).sameType (Minimalist.FeatureVal.pol a_1) = true
(Minimalist.FeatureVal.pov a).sameType (Minimalist.FeatureVal.pov a_1) = true
(Minimalist.FeatureVal.atomic a).sameType (Minimalist.FeatureVal.atomic a_1) = true
(Minimalist.FeatureVal.minimal a).sameType (Minimalist.FeatureVal.minimal a_1) = true
(Minimalist.FeatureVal.participant a).sameType (Minimalist.FeatureVal.participant a_1) = true
(Minimalist.FeatureVal.author a).sameType (Minimalist.FeatureVal.author a_1) = true
x✝¹.sameType x✝ = false

Instances For

inductive Minimalist.GramFeature :

A grammatical feature: either valued or unvalued.

Valued vs unvalued is about whether the feature carries a specific value (person:3) or just a type placeholder (person:_). This is orthogonal to ±Interpretable (see Interpretability below):

	+Interpretable	–Interpretable
Valued	φ of N (person:3)	—
Unvalued	—	φ of T/v, Case of N

Unvalued features act as probes; valued features can be goals. But interpretability determines whether a feature must be checked and deleted before LF — a separate question from whether it currently carries a value.

valued : FeatureVal → GramFeature
unvalued : FeatureVal → GramFeature

Instances For

def Minimalist.instReprGramFeature.repr :

GramFeature → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Minimalist.instReprGramFeature :

Repr GramFeature

Equations

Minimalist.instReprGramFeature = { reprPrec := Minimalist.instReprGramFeature.repr }

@[implicit_reducible]

instance Minimalist.instDecidableEqGramFeature :

DecidableEq GramFeature

Equations

Minimalist.instDecidableEqGramFeature = Minimalist.instDecidableEqGramFeature.decEq

def Minimalist.instDecidableEqGramFeature.decEq (x✝ x✝¹ : GramFeature) :

Decidable (x✝ = x✝¹)

Equations

Minimalist.instDecidableEqGramFeature.decEq (Minimalist.GramFeature.valued a) (Minimalist.GramFeature.valued b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
Minimalist.instDecidableEqGramFeature.decEq (Minimalist.GramFeature.valued a) (Minimalist.GramFeature.unvalued a_1) = isFalse ⋯
Minimalist.instDecidableEqGramFeature.decEq (Minimalist.GramFeature.unvalued a) (Minimalist.GramFeature.valued a_1) = isFalse ⋯
Minimalist.instDecidableEqGramFeature.decEq (Minimalist.GramFeature.unvalued a) (Minimalist.GramFeature.unvalued b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

Instances For

def Minimalist.GramFeature.isValued :

GramFeature → Bool

Is this feature valued?

Equations

(Minimalist.GramFeature.valued a).isValued = true
(Minimalist.GramFeature.unvalued a).isValued = false

Instances For

def Minimalist.GramFeature.isUnvalued :

GramFeature → Bool

Is this feature unvalued (a potential probe)?

Equations

(Minimalist.GramFeature.valued a).isUnvalued = false
(Minimalist.GramFeature.unvalued a).isUnvalued = true

Instances For

def Minimalist.GramFeature.featureType :

GramFeature → FeatureVal

Get the feature type (ignoring valued/unvalued distinction)

Equations

(Minimalist.GramFeature.valued a).featureType = a
(Minimalist.GramFeature.unvalued a).featureType = a

Instances For

def Minimalist.featuresMatch (f1 f2 : GramFeature) :

Bool

Do two features match in type? (for Agree) Delegates to FeatureVal.sameType, ignoring specific values.

Equations

Minimalist.featuresMatch f1 f2 = f1.featureType.sameType f2.featureType

Instances For

A feature bundle is a total assignment from feature dimensions to three-state checking slots (Features.FeatureSlot): one slot per dimension, absent / unvalued (probe) / valued v. This replaces the earlier list representation (List GramFeature), which admitted junk — duplicate dimensions, conflicting values — and was not extensional, so it could not be a LawfulBundleLike (the Features/Basic.lean Todo).

This is the Agree-layer structure; per [MCB25] (book p. 13) the free-Merge core keeps SO₀ features atomic, so the slot apparatus is decoupled from the SyntacticObject carrier and lives in Features/Slot.lean.

GramFeature survives as a literal-builder DSL: ofGramFeatures folds a list of valued/unvalued features into the assignment, the list head winning on duplicate dimensions.

inductive Minimalist.FeatureType :

The feature dimensions checked via Agree — the equivalence classes of FeatureVal.sameType. φ-features split into their three sub-dimensions (person, number, gender) so each is a slot in its own right.

person : FeatureType
number : FeatureType
gender : FeatureType
case : FeatureType
wh : FeatureType
q : FeatureType
epp : FeatureType
tense : FeatureType
hon : FeatureType
finite : FeatureType
factive : FeatureType
neg : FeatureType
rel : FeatureType
oblique : FeatureType
ellipsis : FeatureType
catN : FeatureType
catV : FeatureType
foc : FeatureType
pol : FeatureType
pov : FeatureType
atomic : FeatureType
minimal : FeatureType
participant : FeatureType
author : FeatureType

Instances For

@[implicit_reducible]

instance Minimalist.instReprFeatureType :

Repr FeatureType

Equations

Minimalist.instReprFeatureType = { reprPrec := Minimalist.instReprFeatureType.repr }

def Minimalist.instReprFeatureType.repr :

FeatureType → ℕ → Std.Format

Equations

One or more equations did not get rendered due to their size.
Minimalist.instReprFeatureType.repr Minimalist.FeatureType.q prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalist.FeatureType.q")).group prec✝

Instances For

@[implicit_reducible]

instance Minimalist.instDecidableEqFeatureType :

DecidableEq FeatureType

Equations

Minimalist.instDecidableEqFeatureType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Minimalist.instFintypeFeatureType :

Fintype FeatureType

Equations

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

def Minimalist.FeatureType.all :

List FeatureType

All feature dimensions, for computable enumeration (Finset.univ.toList is noncomputable).

Equations

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

Instances For

def Minimalist.FeatureVal.dimension :

FeatureVal → FeatureType

The dimension a feature value belongs to. Two values share a dimension iff FeatureVal.sameType holds.

Equations

Instances For

@[reducible]

def Minimalist.FeatureType.ValueOf :

FeatureType → Type

The value space of a dimension: the canonical type a slot at that dimension carries (person ↦ Person, number ↦ Number, gender ↦ Nat, case ↦ Case, hon ↦ HonLevel, every binary dimension ↦ Bool).

Equations

Minimalist.FeatureType.person.ValueOf = Person
Minimalist.FeatureType.number.ValueOf = Number
Minimalist.FeatureType.gender.ValueOf = ℕ
Minimalist.FeatureType.case.ValueOf = Case
Minimalist.FeatureType.hon.ValueOf = Minimalist.HonLevel
Minimalist.FeatureType.wh.ValueOf = Bool
Minimalist.FeatureType.q.ValueOf = Bool
Minimalist.FeatureType.epp.ValueOf = Bool
Minimalist.FeatureType.tense.ValueOf = Bool
Minimalist.FeatureType.finite.ValueOf = Bool
Minimalist.FeatureType.factive.ValueOf = Bool
Minimalist.FeatureType.neg.ValueOf = Bool
Minimalist.FeatureType.rel.ValueOf = Bool
Minimalist.FeatureType.oblique.ValueOf = Bool
Minimalist.FeatureType.ellipsis.ValueOf = Bool
Minimalist.FeatureType.catN.ValueOf = Bool
Minimalist.FeatureType.catV.ValueOf = Bool
Minimalist.FeatureType.foc.ValueOf = Bool
Minimalist.FeatureType.pol.ValueOf = Bool
Minimalist.FeatureType.pov.ValueOf = Bool
Minimalist.FeatureType.atomic.ValueOf = Bool
Minimalist.FeatureType.minimal.ValueOf = Bool
Minimalist.FeatureType.participant.ValueOf = Bool
Minimalist.FeatureType.author.ValueOf = Bool

Instances For

@[implicit_reducible]

instance Minimalist.instDecidableEqValueOf (t : FeatureType) :

DecidableEq t.ValueOf

Equations

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

@[implicit_reducible]

instance Minimalist.instReprValueOf (t : FeatureType) :

Repr t.ValueOf

Equations

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

def Minimalist.FeatureVal.value (fv : FeatureVal) :

fv.dimension.ValueOf

The value carried by a feature value, in its dimension's value space.

Equations

(Minimalist.FeatureVal.phi (Minimalist.PhiFeature.person a)).value = a
(Minimalist.FeatureVal.phi (Minimalist.PhiFeature.number a)).value = a
(Minimalist.FeatureVal.phi (Minimalist.PhiFeature.gender a)).value = a
(Minimalist.FeatureVal.case a).value = a
(Minimalist.FeatureVal.wh a).value = a
(Minimalist.FeatureVal.q a).value = a
(Minimalist.FeatureVal.epp a).value = a
(Minimalist.FeatureVal.tense a).value = a
(Minimalist.FeatureVal.hon a).value = a
(Minimalist.FeatureVal.finite a).value = a
(Minimalist.FeatureVal.factive a).value = a
(Minimalist.FeatureVal.neg a).value = a
(Minimalist.FeatureVal.rel a).value = a
(Minimalist.FeatureVal.oblique a).value = a
(Minimalist.FeatureVal.ellipsis a).value = a
(Minimalist.FeatureVal.catN a).value = a
(Minimalist.FeatureVal.catV a).value = a
(Minimalist.FeatureVal.foc a).value = a
(Minimalist.FeatureVal.pol a).value = a
(Minimalist.FeatureVal.pov a).value = a
(Minimalist.FeatureVal.atomic a).value = a
(Minimalist.FeatureVal.minimal a).value = a
(Minimalist.FeatureVal.participant a).value = a
(Minimalist.FeatureVal.author a).value = a

Instances For

@[reducible, inline]

abbrev Minimalist.FeatureBundle :

A feature bundle as a total assignment: each dimension maps to a three-state checking slot. The canonical extensional carrier — replacing List GramFeature — that is LawfulBundleLike.

Equations

Minimalist.FeatureBundle = ((t : Minimalist.FeatureType) → Features.FeatureSlot t.ValueOf)

Instances For

@[implicit_reducible]

instance Minimalist.FeatureBundle.instBundleLikeFeatureTypeFeatureSlotValueOf :

BundleLike FeatureBundle FeatureType fun (t : FeatureType) => Features.FeatureSlot t.ValueOf

Equations

Minimalist.FeatureBundle.instBundleLikeFeatureTypeFeatureSlotValueOf = { val := fun (b : Minimalist.FeatureBundle) => b }

instance Minimalist.FeatureBundle.instLawfulBundleLikeFeatureTypeFeatureSlotValueOf :

LawfulBundleLike FeatureBundle

def Minimalist.FeatureBundle.hasValuedFeature (a : FeatureBundle) (t : FeatureType) :

Bool

The bundle has a valued feature of the given dimension.

Equations

a.hasValuedFeature t = (a t).isValued

Instances For

def Minimalist.FeatureBundle.hasUnvaluedFeature (a : FeatureBundle) (t : FeatureType) :

Bool

The bundle has an unvalued (probe) feature of the given dimension.

Equations

a.hasUnvaluedFeature t = (a t).isUnvalued

Instances For

def Minimalist.FeatureBundle.getValuedFeature (a : FeatureBundle) (t : FeatureType) :

Option t.ValueOf

The value at the given dimension, when valued.

Equations

a.getValuedFeature t = (a t).value?

Instances For

def Minimalist.FeatureBundle.single (t : FeatureType) (v : t.ValueOf) :

The assignment specifying exactly one valued dimension, all others absent.

Equations

Minimalist.FeatureBundle.single t v = Function.update ⊥ t (Features.FeatureSlot.valued v)

Instances For

@[simp]

theorem Minimalist.FeatureBundle.single_self (t : FeatureType) (v : t.ValueOf) :

single t v t = Features.FeatureSlot.valued v

@[implicit_reducible]

instance Minimalist.FeatureBundle.instInhabited :

Inhabited FeatureBundle

The everywhere-absent bundle is the default.

Equations

Minimalist.FeatureBundle.instInhabited = { default := ⊥ }

@[implicit_reducible]

instance Minimalist.FeatureBundle.instDecidableEq :

DecidableEq FeatureBundle

Equations

Minimalist.FeatureBundle.instDecidableEq a b = Fintype.decidablePiFintype a b

@[implicit_reducible]

instance Minimalist.FeatureBundle.instRepr :

Repr FeatureBundle

Render a bundle by its specified (non-absent) dimensions. The function carrier has no structural Repr, so containing structures that deriving Repr rely on this.

Equations

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

def Minimalist.GramFeature.toSlot (gf : GramFeature) :

Features.FeatureSlot gf.featureType.dimension.ValueOf

The checking slot a single grammatical feature contributes at its own dimension: valued v ↦ valued v.value, unvalued _ ↦ unvalued.

Equations

Instances For

def Minimalist.FeatureBundle.ofGramFeatures (l : List GramFeature) :

Bridge from the legacy list representation: fold each feature into its dimension's slot, the list head taking precedence on duplicate dimensions (matching getValuedFeature/find? first-match semantics).

Equations

Minimalist.FeatureBundle.ofGramFeatures l = List.foldr (fun (gf : Minimalist.GramFeature) (a : Minimalist.FeatureBundle) => Function.update a gf.featureType.dimension gf.toSlot) ⊥ l

Instances For

def Minimalist.FeatureType.toFeatureVal (t : FeatureType) :

t.ValueOf → FeatureVal

Reconstruct a FeatureVal at dimension t from a value.

Equations

Instances For

def Minimalist.FeatureType.placeholderValue (t : FeatureType) :

A conventional placeholder value per dimension (for unvalued-feature reconstruction, where the value is semantically irrelevant).

Equations

Minimalist.FeatureType.person.placeholderValue = Person.third
Minimalist.FeatureType.number.placeholderValue = Number.singular
Minimalist.FeatureType.gender.placeholderValue = 0
Minimalist.FeatureType.case.placeholderValue = Case.nom
Minimalist.FeatureType.hon.placeholderValue = Minimalist.HonLevel.nh
Minimalist.FeatureType.wh.placeholderValue = false
Minimalist.FeatureType.q.placeholderValue = false
Minimalist.FeatureType.epp.placeholderValue = false
Minimalist.FeatureType.tense.placeholderValue = false
Minimalist.FeatureType.finite.placeholderValue = false
Minimalist.FeatureType.factive.placeholderValue = false
Minimalist.FeatureType.neg.placeholderValue = false
Minimalist.FeatureType.rel.placeholderValue = false
Minimalist.FeatureType.oblique.placeholderValue = false
Minimalist.FeatureType.ellipsis.placeholderValue = false
Minimalist.FeatureType.catN.placeholderValue = false
Minimalist.FeatureType.catV.placeholderValue = false
Minimalist.FeatureType.foc.placeholderValue = false
Minimalist.FeatureType.pol.placeholderValue = false
Minimalist.FeatureType.pov.placeholderValue = false
Minimalist.FeatureType.atomic.placeholderValue = false
Minimalist.FeatureType.minimal.placeholderValue = false
Minimalist.FeatureType.participant.placeholderValue = false
Minimalist.FeatureType.author.placeholderValue = false

Instances For

def Minimalist.FeatureBundle.toGramFeatures (fb : FeatureBundle) :

List GramFeature

Bridge back to the legacy list representation: one GramFeature per specified dimension. The placeholder value on unvalued features is semantically inert (ofGramFeatures discards it via toSlot), so ofGramFeatures ∘ toGramFeatures round-trips.

Equations

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

Instances For

`FeatureVal`-keyed query wrappers #

Convenience over the FeatureType-keyed methods: pass a sample FeatureVal (its carried value is ignored, only the dimension matters — the old sameType semantics). These keep probe-spec call sites that pass a placeholder feature (.phi (.person .third)) unchanged.

def Minimalist.hasValuedFeature (fb : FeatureBundle) (fv : FeatureVal) :

Bool

The bundle has a valued feature of fv's dimension.

Equations

Minimalist.hasValuedFeature fb fv = fb.hasValuedFeature fv.dimension

Instances For

def Minimalist.hasUnvaluedFeature (fb : FeatureBundle) (fv : FeatureVal) :

Bool

The bundle has an unvalued (probe) feature of fv's dimension.

Equations

Minimalist.hasUnvaluedFeature fb fv = fb.hasUnvaluedFeature fv.dimension

Instances For

def Minimalist.getValuedFeature (fb : FeatureBundle) (fv : FeatureVal) :

Option fv.dimension.ValueOf

The value at fv's dimension, when valued.

Equations

Minimalist.getValuedFeature fb fv = fb.getValuedFeature fv.dimension

Instances For

inductive Minimalist.Interpretability :

Whether a feature is interpretable (contributes to LF) or uninterpretable (must be checked and deleted before LF).

This is the central distinction of [Cho95] Ch 4 §4.5. It is orthogonal to valued/unvalued: a feature can be interpretable but unvalued (rare), or uninterpretable but valued (never, in the standard theory). The typical pairings are:

+Interpretable, valued: φ-features on nouns, categorial features
–Interpretable, unvalued: φ-features on T/v, Case on nouns

AgreeSOT.lean uses Interpretability directly for tense features. GenderResolution.lean's AnnotatedFeature.interp uses Interpretability directly; CoordinateResolution.lean, AdamsonAnagnostopoulou2025.lean, and Carstens2026.lean all use it via open _root_.Minimalist.

interpretable : Interpretability
uninterpretable : Interpretability

Instances For

def Minimalist.instReprInterpretability.repr :

Interpretability → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Minimalist.instReprInterpretability :

Repr Interpretability

Equations

Minimalist.instReprInterpretability = { reprPrec := Minimalist.instReprInterpretability.repr }

@[implicit_reducible]

instance Minimalist.instDecidableEqInterpretability :

DecidableEq Interpretability

Equations

Minimalist.instDecidableEqInterpretability x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Minimalist.FeatureVal.inherentInterpretability :

FeatureVal → Option Interpretability

Whether a feature is inherently interpretable regardless of host.

Some features are always interpretable (categorial, honorific, factive) or always uninterpretable (Case, EPP, ellipsis). For features whose interpretability depends on host category (phi, wh, tense), see isInterpretableOn in Checking.lean.

Equations

Instances For

theorem Minimalist.case_always_uninterpretable (c : Case) :

(FeatureVal.case c).inherentInterpretability = some Interpretability.uninterpretable

Case is always uninterpretable.

theorem Minimalist.catN_always_interpretable (b : Bool) :

(FeatureVal.catN b).inherentInterpretability = some Interpretability.interpretable

Categorial [N] is always interpretable.