Feature Infrastructure for Minimalist Agree

@cite{adger-2003} @cite{chomsky-2000} @cite{chomsky-2001} @cite{alok-2020} @cite{alok-bhalla-2026} @cite{lobeck-1995} @cite{panagiotidis-2015} @cite{pollock-1989}

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; see ObligatoryOperations.lean).

Design Decision: PersonLevel replaces Nat

PhiFeature.person uses Core.Prominence.PersonLevel (.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:

• Core.Prominence.PersonLevel — framework-agnostic person hierarchy
• PersonGeometry.DecomposedPerson — @cite{preminger-2014}'s [±participant, ±author] decomposition, now mapping from PersonLevel
• DifferentialIndexing.IndexingPersonLevel — @cite{just-2024}'s SAP/3rd binary split, bridged to PersonLevel

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 Minimalism.PhiFeature : Type

Phi-features (agreement features).

• person : Core.Prominence.PersonLevel → PhiFeature
• number : Number → PhiFeature
• gender : Nat → PhiFeature

def Minimalism.instReprPhiFeature.repr : PhiFeature → Nat → Std.Format

Equations

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

instance Minimalism.instReprPhiFeature : Repr PhiFeature

Equations

• Minimalism.instReprPhiFeature = { reprPrec := Minimalism.instReprPhiFeature.repr }

instance Minimalism.instDecidableEqPhiFeature : DecidableEq PhiFeature

Equations

• Minimalism.instDecidableEqPhiFeature = Minimalism.instDecidableEqPhiFeature.decEq

def Minimalism.instDecidableEqPhiFeature.decEq (x✝ x✝¹ : PhiFeature) : Decidable (x✝ = x✝¹)

Equations

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

inductive Minimalism.CaseVal : Type

Case values used in the Agree system.

This is the Minimalism-internal case type, covering the 8 values needed for Agree-based case assignment. For the full cross-linguistic inventory, see Core.Case.

• nom : CaseVal
• acc : CaseVal
• dat : CaseVal
• gen : CaseVal
• obl : CaseVal
• abl : CaseVal
• erg : CaseVal
• abs : CaseVal

def Minimalism.instReprCaseVal.repr : CaseVal → Nat → Std.Format

Equations

• Minimalism.instReprCaseVal.repr Minimalism.CaseVal.nom prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalism.CaseVal.nom")).group prec✝
• Minimalism.instReprCaseVal.repr Minimalism.CaseVal.acc prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalism.CaseVal.acc")).group prec✝
• Minimalism.instReprCaseVal.repr Minimalism.CaseVal.dat prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalism.CaseVal.dat")).group prec✝
• Minimalism.instReprCaseVal.repr Minimalism.CaseVal.gen prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalism.CaseVal.gen")).group prec✝
• Minimalism.instReprCaseVal.repr Minimalism.CaseVal.obl prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalism.CaseVal.obl")).group prec✝
• Minimalism.instReprCaseVal.repr Minimalism.CaseVal.abl prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalism.CaseVal.abl")).group prec✝
• Minimalism.instReprCaseVal.repr Minimalism.CaseVal.erg prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalism.CaseVal.erg")).group prec✝
• Minimalism.instReprCaseVal.repr Minimalism.CaseVal.abs prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalism.CaseVal.abs")).group prec✝

instance Minimalism.instReprCaseVal : Repr CaseVal

Equations

• Minimalism.instReprCaseVal = { reprPrec := Minimalism.instReprCaseVal.repr }

instance Minimalism.instDecidableEqCaseVal : DecidableEq CaseVal

Equations

• Minimalism.instDecidableEqCaseVal x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Minimalism.CaseVal.toCase : CaseVal → Core.Case

Convert a Minimalist CaseVal to the theory-neutral Core.Case.

obl (oblique) is a Minimalism-internal category, not a specific case in @cite{blake-1994}'s typology. We map it to dat as the highest-ranked peripheral case — this is an approximation, since "oblique" in Minimalism is a cover term for non-core cases, most commonly dative-like.

Equations

• Minimalism.CaseVal.nom.toCase = Core.Case.nom
• Minimalism.CaseVal.acc.toCase = Core.Case.acc
• Minimalism.CaseVal.dat.toCase = Core.Case.dat
• Minimalism.CaseVal.gen.toCase = Core.Case.gen
• Minimalism.CaseVal.obl.toCase = Core.Case.dat
• Minimalism.CaseVal.abl.toCase = Core.Case.abl
• Minimalism.CaseVal.erg.toCase = Core.Case.erg
• Minimalism.CaseVal.abs.toCase = Core.Case.abs

inductive Minimalism.HonLevel : Type

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

instance Minimalism.instReprHonLevel : Repr HonLevel

Equations

• Minimalism.instReprHonLevel = { reprPrec := Minimalism.instReprHonLevel.repr }

def Minimalism.instReprHonLevel.repr : HonLevel → Nat → Std.Format

Equations

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

instance Minimalism.instDecidableEqHonLevel : DecidableEq HonLevel

Equations

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

inductive Minimalism.FeatureVal : Type

Feature values that can be checked via Agree

• phi : PhiFeature → FeatureVal
• case : CaseVal → 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

def Minimalism.instReprFeatureVal.repr : FeatureVal → Nat → Std.Format

Equations

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

instance Minimalism.instReprFeatureVal : Repr FeatureVal

Equations

• Minimalism.instReprFeatureVal = { reprPrec := Minimalism.instReprFeatureVal.repr }

def Minimalism.instDecidableEqFeatureVal.decEq (x✝ x✝¹ : FeatureVal) : Decidable (x✝ = x✝¹)

Equations

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

instance Minimalism.instDecidableEqFeatureVal : DecidableEq FeatureVal

Equations

• Minimalism.instDecidableEqFeatureVal = Minimalism.instDecidableEqFeatureVal.decEq

def Minimalism.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

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

inductive Minimalism.GramFeature : Type

A grammatical feature: either valued or unvalued

• Valued (interpretable): contributes to meaning, can be a goal
• Unvalued (uninterpretable): must be checked, acts as probe

• valued : FeatureVal → GramFeature
• unvalued : FeatureVal → GramFeature

def Minimalism.instReprGramFeature.repr : GramFeature → Nat → Std.Format

Equations

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

instance Minimalism.instReprGramFeature : Repr GramFeature

Equations

• Minimalism.instReprGramFeature = { reprPrec := Minimalism.instReprGramFeature.repr }

def Minimalism.instDecidableEqGramFeature.decEq (x✝ x✝¹ : GramFeature) : Decidable (x✝ = x✝¹)

Equations

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

instance Minimalism.instDecidableEqGramFeature : DecidableEq GramFeature

Equations

• Minimalism.instDecidableEqGramFeature = Minimalism.instDecidableEqGramFeature.decEq

def Minimalism.GramFeature.isValued : GramFeature → Bool

Is this feature valued?

Equations

• (Minimalism.GramFeature.valued a).isValued = true
• (Minimalism.GramFeature.unvalued a).isValued = false

def Minimalism.GramFeature.isUnvalued : GramFeature → Bool

Is this feature unvalued (a potential probe)?

Equations

• (Minimalism.GramFeature.valued a).isUnvalued = false
• (Minimalism.GramFeature.unvalued a).isUnvalued = true

def Minimalism.GramFeature.featureType : GramFeature → FeatureVal

Get the feature type (ignoring valued/unvalued distinction)

Equations

• (Minimalism.GramFeature.valued a).featureType = a
• (Minimalism.GramFeature.unvalued a).featureType = a

def Minimalism.featuresMatch (f1 f2 : GramFeature) : Bool

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

Equations

• Minimalism.featuresMatch f1 f2 = f1.featureType.sameType f2.featureType

@[reducible, inline]

abbrev Minimalism.FeatureBundle : Type

A feature bundle: list of grammatical features

Equations

• Minimalism.FeatureBundle = List Minimalism.GramFeature

def Minimalism.hasUnvaluedFeature (fb : FeatureBundle) (ftype : FeatureVal) : Bool

Does the bundle have an unvalued feature of a given type? Uses sameType so that e.g. [uPerson:] matches ftype [Person:].

Equations

• Minimalism.hasUnvaluedFeature fb ftype = List.any fb fun (f : Minimalism.GramFeature) => f.isUnvalued && f.featureType.sameType ftype

def Minimalism.hasValuedFeature (fb : FeatureBundle) (ftype : FeatureVal) : Bool

Does the bundle have a valued feature of a given type? Uses sameType so that e.g. [Person:3] matches ftype [Person:_].

Equations

• Minimalism.hasValuedFeature fb ftype = List.any fb fun (f : Minimalism.GramFeature) => f.isValued && f.featureType.sameType ftype

def Minimalism.getValuedFeature (fb : FeatureBundle) (ftype : FeatureVal) : Option GramFeature

Get the valued feature of a given type (if present). Uses sameType for type-level matching.

Equations

• Minimalism.getValuedFeature fb ftype = List.find? (fun (f : Minimalism.GramFeature) => f.isValued && f.featureType.sameType ftype) fb