Docs / Syntax / Minimalist / Feature / Valuation

Valuation

import Linglib.Syntax.Minimalist.Feature.Valuation · namespace Minimalist

This file defines valuation of feature bundles, the part of Agree that copies the value of a goal into a probe (Chomsky 2000), from the valuation of a single slot (FeatureSlot.valueWith). An absent slot is unchanged, since an item that lacks a dimension is not a probe for it.

Valuing a bundle at a dimension it bears is unification with the bundle that bears only the value. At an agreement dimension, valuation followed by FeatureBundle.agreement is unification of agreement bundles. Agree with a goal that has no value at the dimension leaves the probe unchanged, so Agree can fail without causing a crash (Preminger 2014). The goal a probe agrees with is found by search (Minimalist.LinearizedSyntacticObject.goals).

The items of a derivation carry their bundles in a FeatureState, and Agree over it is the one Agree of Probe/Agree.lean, Probe.agree, with the probe of an item at a dimension and valuation as its copying. Valuation values the probe and the goal each with the value of the other at the dimension, so a valued probe, such as a case assigner, values an unvalued goal. A goal matches a probe when it bears the dimension, since matching is identity of the dimension and not of the value (Chomsky 2000). The probe of an item at a dimension is satisfied by the goals that match it and interacts with those that are also active. A matching goal that is not active therefore halts the search without valuing: Chomsky's defective intervention is satisfaction without interaction in the sense of Deal 2025a. Valuation only adds features, so a run of Agree extends the state, and a slot valued before Agree keeps its value.

Main definitions

Minimalist.FeatureBundle.valueAt: a bundle valued with v at a dimension.
Minimalist.FeatureBundle.valueFrom: a bundle valued from another at a dimension.
Minimalist.FeatureState: the feature bundles of the items of a derivation.
Minimalist.FeatureState.Matches: a goal matches a probe at a dimension.
Minimalist.FeatureState.probe: the probe of an item at a dimension.
Minimalist.FeatureState.value: two items valued from each other at a dimension, the copying of Agree.

Implementation notes

The leaves of a SyntacticObject are lexical-item tokens, and the tree records nothing else: in Marcolli et al. 2025 the leaves are drawn from a set of lexical items and syntactic features, and Merge attaches no label to an internal vertex. A lexical item carries the bundle it has in the lexicon (LexicalItem.features). Agree changes the features of the items it relates, producing what Chomsky 2000 calls modified lexical items. The bundles of a derivation are therefore kept outside the tree: a FeatureState assigns a bundle to each item, and valuation changes that assignment, not the tree.

References

Chomsky 2000, Minimalist Inquiries: The Framework
Marcolli et al. 2025, Mathematical Structure of Syntactic Merge: An Algebraic Model for Generative Linguistics formalized
Deal 2025a, Current models of Agree formalized
Preminger 2014, Agreement and Its Failures formalized
Amato 2025, Apparent minimality violations solved by Nested Agree formalized

Declarations

The bundle b valued with v at t, or ⊤ if b is valued otherwise at t.

def FeatureBundle.valueAt L70–72

(b : FeatureBundle) (t : FeatureType) (v : t.Value) :

WithTop FeatureBundle

b.valueAt t v = WithTop.map (Function.update b t) (FeatureSlot.valueWith v (b t))

Used by FeatureBundle.le_of_valueAt_eq_coe, FeatureBundle.valueAt_eq_unify, FeatureBundle.map_agreement_valueAt, FeatureBundle.valueFrom

Used in BejarRezac2003

L76–78

theorem FeatureBundle.valueAt_eq_unify L80–82

{t : FeatureType} {b : FeatureBundle} {v : t.Value} (hb : b t ≠ FeatureSlot.absent) :

b.valueAt t v = PartialUnify.unify b (single t v)

Built from

theorem FeatureBundle.map_agreement_valueAt L84–94

{d : Agreement.Dimension} {v : d.Value} {b : FeatureBundle} (hb : b (FeatureType.agr d) ≠ FeatureSlot.absent) :

WithTop.map agreement (b.valueAt (FeatureType.agr d) v) = PartialUnify.unify b.agreement (Agreement.Bundle.set d v ⊥)

Built from

The bundle probe valued from goal at t: valued with the value of goal at t, or unchanged if goal has no value there.

def FeatureBundle.valueFrom L98–103

(probe goal : FeatureBundle) (t : FeatureType) :

WithTop FeatureBundle

probe.valueFrom goal t = match goal t with | some (some v) => probe.valueAt t v | x => ↑probe

Built from

Used by FeatureBundle.valueFrom_bot, FeatureBundle.valueFrom_of_forall_ne_valued, FeatureBundle.le_of_valueFrom_eq_coe, FeatureBundle.le_untopD_valueFrom, FeatureState.value

Used in ElkinsTorrenceBrown2026

Agree between items

The feature bundles of the items of a derivation.

@[reducible, inline] abbrev FeatureState L132–133

(H : Type u_1) :

Type u_1

FeatureState H = (H → FeatureBundle)

Used by FeatureState.Matches, FeatureState.instDecidablePredMatches, FeatureState.probe, FeatureState.value, FeatureState.le_value, FeatureState.le_agree_state, FeatureState.apply_eq_valued_of_le

Used in Amato2025

The goal g matches the probe α at t. An unvalued probe matches a goal that bears t, whether valued or not. A valued probe, such as a case assigner, matches a goal that bears t unvalued (Amato 2025).

def FeatureState.Matches L139–146

{H : Type u_1} (s : FeatureState H) (α : H) (t : FeatureType) (g : H) :

Prop

s.Matches α t g = match s α t with | some none => s g t ≠ FeatureSlot.absent | some (some val) => s g t = FeatureSlot.unvalued | none => False

Built from

Used by FeatureState.instDecidablePredMatches, FeatureState.probe

Used in Amato2025

L148–149

The probe of α at t, satisfied by the goals that match it and interacting with the matching goals that are also active.

def FeatureState.probe L151–154

{H : Type u_1} (s : FeatureState H) (α : H) (t : FeatureType) (active : H → Prop) [DecidablePred active] :

Probe H

s.probe α t active = { int := fun (g : H) => s.Matches α t g ∧ active g, sat := s.Matches α t, decInt := fun (a : H) => instDecidableAnd, decSat := s.instDecidablePredMatches α t }

Built from , ,

Used by FeatureState.le_agree_state

The valuation of α and g at t, the copying of Agree between them: each is valued with the value of the other at t, and a bundle whose value differs from the other's is unchanged.

def FeatureState.value L160–164

{H : Type u_1} (s : FeatureState H) (α : H) (t : FeatureType) [DecidableEq H] (g : H) :

FeatureState H

s.value α t g = Function.update (Function.update s α (WithTop.untopD (s α) ((s α).valueFrom (s g) t))) g (WithTop.untopD (s g) ((s g).valueFrom (s α) t))

Built from ,

Used by FeatureState.le_value, FeatureState.le_agree_state

Used in Amato2025

L166–172

theorem FeatureState.le_agree_state L174–176

{H : Type u_1} (s : FeatureState H) (α : H) (t : FeatureType) [DecidableEq H] (active : H → Prop) [DecidablePred active] (goals : List H) :

s ≤ ((s.probe α t active).agree (fun (g : H) (s : FeatureState H) => s.value α t g) s goals).state

Built from , ,

theorem FeatureState.apply_eq_valued_of_le L182–184

{H : Type u_1} {s s' : FeatureState H} (h : s ≤ s') {x : H} {u : FeatureType} {v : u.Value} (hv : s x u = FeatureSlot.valued v) :

s' x u = FeatureSlot.valued v

Built from