Agree (Minimalist Feature Checking)

Formalization of Agree following [Cho00] and [Adg03].

The Agree Operation

Agree is the mechanism by which features are checked/valued:

1. A probe (head with unvalued feature) searches its c-command domain
2. It finds the closest goal (element with matching valued feature)
3. The probe's feature is valued by copying from the goal
4. Both features are then checked (and may delete at PF/LF)

Architecture

This file contains the Agree operation and its structural conditions (locality, activity, phase-boundedness, defective intervention). For the feature types (PhiFeature, FeatureVal, etc.), see Features.lean. For the failure model (what happens when Agree fails — a Probe.outcome of unvalued, tolerated per [Pre14] Ch. 5), see Probe/Basic.lean. For the Case Filter, see CaseFilter.lean.

Satisfaction Conditions

Standard Agree assumes a probe is satisfied by finding a matching valued feature. [Dea24] and [Kei19] argue for richer conditions:

• Feature match: the standard case
• Head encounter: probe is satisfied by encountering a head of a particular category (e.g., Infl's probe stopped by transitive Voice)
• Disjunctive: probe is satisfied by ANY of several conditions

This captures e.g. Mam's Infl probe, which has satisfaction condition [SAT: φ or Voice_TR] — it stops when it finds either matching φ-features OR transitive Voice, whichever comes first.

structure Minimalist.ExtendedLI : Type

Extended LI with grammatical features

This extends Harizanov's LI with Agree-relevant features. The original ⟨CAT, SEL⟩ handles selection; this adds φ, Case, etc.

• base : LexicalItem
• features : FeatureBundle

def Minimalist.instReprExtendedLI.repr : ExtendedLI → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Minimalist.instReprExtendedLI : Repr ExtendedLI

Equations

• Minimalist.instReprExtendedLI = { reprPrec := Minimalist.instReprExtendedLI.repr }

def Minimalist.ExtendedLI.fromSimple (cat : Cat) (sel : SelStack) (feats : FeatureBundle) : ExtendedLI

Create an extended LI from a simple LI

Equations

• Minimalist.ExtendedLI.fromSimple cat sel feats = { base := Minimalist.LexicalItem.simple cat sel, features := feats }

def Minimalist.ExtendedLI.isProbe (li : ExtendedLI) : Bool

Is this LI a probe (has unvalued features)?

Equations

• li.isProbe = Minimalist.FeatureType.all.any fun (t : Minimalist.FeatureType) => (li.features t).isUnvalued

def Minimalist.ExtendedLI.isGoalFor (li : ExtendedLI) (ftype : FeatureVal) : Bool

Is this LI a potential goal for a given feature type?

Equations

• li.isGoalFor ftype = Minimalist.hasValuedFeature li.features ftype

structure Minimalist.AgreeRelation : Type

A probe-goal pair for Agree

• probe : SyntacticObject
• goal : SyntacticObject
• feature : FeatureVal
• probeFeatures : FeatureBundle
• goalFeatures : FeatureBundle

def Minimalist.AgreeRelation.probeCommands (a : AgreeRelation) (root : SyntacticObject) : Prop

The probe c-commands the goal within a given tree

Equations

• a.probeCommands root = Minimalist.SO.cCommandsIn root a.probe a.goal

def Minimalist.AgreeRelation.goalHasFeature (a : AgreeRelation) : Bool

The goal has the relevant valued feature

Equations

• a.goalHasFeature = Minimalist.hasValuedFeature a.goalFeatures a.feature

def Minimalist.AgreeRelation.probeNeedsFeature (a : AgreeRelation) : Bool

The probe has the relevant unvalued feature

Equations

• a.probeNeedsFeature = Minimalist.hasUnvaluedFeature a.probeFeatures a.feature

def Minimalist.validAgree (a : AgreeRelation) (root : SyntacticObject) : Prop

Valid Agree: probe c-commands goal (in tree), probe has unvalued, goal has valued

Equations

• Minimalist.validAgree a root = (a.probeCommands root ∧ a.probeNeedsFeature = true ∧ a.goalHasFeature = true)

def Minimalist.closestGoalB (root probe goal : SyntacticObject) (pred : SyntacticObject → Bool) : Bool

Decidable tree presentation of Probe.search-locality (Probe.search_eq_some_iff_closest, pred playing Probe.vis): goal is pred-matching and c-commanded by probe, with no pred-matching node c-commanded by probe c-commanding goal.

Equations

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

@[implicit_reducible]

instance Minimalist.instDecidableIsHorizonLeafFor (horizonCat : Cat) (n : SyntacticObject) : Decidable (Minimalist.isHorizonLeafFor✝ horizonCat n)

Equations

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

def Minimalist.behindHorizonB (root probe target : SyntacticObject) (horizonCat : Cat) : Bool

Is target behind a horizon of category horizonCat relative to probe in tree root?

A leaf head n of category horizonCat creates a horizon: its c-command domain is opaque to the probe. target is behind the horizon iff there exists a leaf n with category horizonCat such that:

1. probe c-commands n (n is in probe's search domain)
2. n c-commands target (target is in n's opaque domain)

This captures [Kei19]'s horizon mechanism: the probe cannot see past a head of the horizon category. Elements that are c-commanded by the horizon head are invisible to the probe.

Example: N° is a horizon for wh-probes ([AP25]). In [DP D° [PossP Psr N°]], N° c-commands Psr (they are sisters), so wh-probes on C° cannot reach Psr. But D° is a sister of PossP, NOT c-commanded by N°, so the whole DP remains visible for pied-piping.

Equations

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

def Minimalist.applyAgree (probeFeats goalFeats : FeatureBundle) (ftype : FeatureVal) : Option FeatureBundle

Apply Agree: value the probe's feature from the goal. Matching is by dimension (ftype.dimension), so a probe with [uPerson:_] is valued by a goal with [Person:3rd] — the placeholder value is irrelevant. If the goal has a valued feature at the dimension and the probe's slot there is unvalued, the probe's slot is set to that value.

Equations

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

structure Minimalist.TAgree : Type

T-Agree: T probes for φ-features on subject DP

T has [uφ], subject DP has [φ] → T gets valued φ. The .third value on person probes is a conventional placeholder — sameType ignores the specific Person value, matching any .person _ against any .person _.

• tHead : SyntacticObject
• subject : SyntacticObject
• tFeatures : FeatureBundle
• subjFeatures : FeatureBundle
• t_has_uphi : hasUnvaluedFeature self.tFeatures (FeatureVal.phi (PhiFeature.person Person.third)) = true ∨ hasUnvaluedFeature self.tFeatures (FeatureVal.phi (PhiFeature.number Number.singular)) = true
• subj_has_phi : hasValuedFeature self.subjFeatures (FeatureVal.phi (PhiFeature.person Person.third)) = true ∨ hasValuedFeature self.subjFeatures (FeatureVal.phi (PhiFeature.number Number.singular)) = true

structure Minimalist.CAgree : Type

C-Agree: C probes for [Q] feature

C has [uQ], interrogative element has [+Q] → question is licensed

• cHead : SyntacticObject
• qElement : SyntacticObject
• cFeatures : FeatureBundle
• qFeatures : FeatureBundle
• c_has_uq : hasUnvaluedFeature self.cFeatures (FeatureVal.q false) = true
• q_has_q : hasValuedFeature self.qFeatures (FeatureVal.q true) = true

def Minimalist.hasEPP (fb : FeatureBundle) : Bool

EPP triggers movement to specifier

When a head has [EPP], Agree is not enough - the goal must MOVE to the specifier position of the agreeing head.

Equations

• Minimalist.hasEPP fb = match fb Minimalist.FeatureType.epp with | Features.FeatureSlot.valued b => b | Features.FeatureSlot.unvalued => true | Features.FeatureSlot.absent => false

def Minimalist.tToCTriggered (cFeats : FeatureBundle) : Bool

T-to-C movement is triggered by [uQ] + [EPP] on C

In matrix questions:

• C has [uQ, EPP]
• T has [+Q] (in some analyses) or movement satisfies EPP
• T moves to C (head movement)

Equations

• Minimalist.tToCTriggered cFeats = (Minimalist.hasUnvaluedFeature cFeats (Minimalist.FeatureVal.q false) && Minimalist.hasEPP cFeats)

def Minimalist.matrixCFeatures : FeatureBundle

Matrix C features: [uQ, EPP]

Equations

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

def Minimalist.embeddedCFeatures : FeatureBundle

Embedded C features: [uQ] only (satisfied by wh-movement)

Equations

• Minimalist.embeddedCFeatures = Minimalist.FeatureBundle.ofGramFeatures [Minimalist.GramFeature.unvalued (Minimalist.FeatureVal.q false)]

theorem Minimalist.matrix_triggers_t_to_c : tToCTriggered matrixCFeatures = true

Matrix C triggers T-to-C

theorem Minimalist.embedded_no_t_to_c : tToCTriggered embeddedCFeatures = false

Embedded C does not trigger T-to-C

def Minimalist.isActive (fb : FeatureBundle) : Bool

Is a feature bundle active? (has at least one unvalued feature)

An element is active iff it has at least one unvalued feature. Typically, DPs are active when they have unvalued Case.

Equations

• Minimalist.isActive fb = Minimalist.FeatureType.all.any fun (t : Minimalist.FeatureType) => (fb t).isUnvalued

def Minimalist.needsCase (fb : FeatureBundle) : Bool

An element needs Case (has unvalued Case feature)

Equations

• Minimalist.needsCase fb = (fb Minimalist.FeatureType.case).isUnvalued

def Minimalist.hasCase (fb : FeatureBundle) : Bool

An element has valued Case

Equations

• Minimalist.hasCase fb = (fb Minimalist.FeatureType.case).isValued

theorem Minimalist.activity_via_case (fb : FeatureBundle) (h : ∀ (t : FeatureType), t ≠ FeatureType.case → fb t = Features.FeatureSlot.absent) : isActive fb = true ↔ needsCase fb = true

Activity is typically determined by Case: A DP is active iff it lacks Case

When a feature bundle contains only Case features, the bundle is active (has unvalued features) iff it needs Case (has unvalued Case).

structure Minimalist.ActiveGoal : Type

A goal that satisfies the Activity Condition

• goal : SyntacticObject
• goalFeatures : FeatureBundle
• isActive : Minimalist.isActive self.goalFeatures = true

def Minimalist.mkActiveGoal (goal : SyntacticObject) (feats : FeatureBundle) : Option ActiveGoal

Create an ActiveGoal if the features are indeed active

Equations

• Minimalist.mkActiveGoal goal feats = if h : Minimalist.isActive feats = true then some { goal := goal, goalFeatures := feats, isActive := h } else none

def Minimalist.validAgreeWithActivity (a : AgreeRelation) (root : SyntacticObject) : Prop

Valid Agree with Activity Condition

Agree requires:

1. Probe c-commands goal (within tree)
2. Probe has unvalued feature
3. Goal has matching valued feature
4. Goal is ACTIVE (has some unvalued feature)

Equations

• Minimalist.validAgreeWithActivity a root = (Minimalist.validAgree a root ∧ Minimalist.isActive a.goalFeatures = true)

def Minimalist.validAgreeWithPIC (strength : PICStrength) (phases : List Phase) (rel : AgreeRelation) (root : SyntacticObject) : Prop

Valid Agree with Phase Impenetrability Condition.

Agree is blocked if the goal is frozen in a phase interior (Phase.Impenetrable, MCB eq 1.14.3). The strength parameter is load-bearing: strong/weak apply the PIC block, while linearizationBound ([SCD26]) drops it (locality is then enforced by Cyclic Linearization, not phasehood).

Equations

• Minimalist.validAgreeWithPIC Minimalist.PICStrength.linearizationBound phases rel root = (Minimalist.validAgree rel root ∧ True)
• Minimalist.validAgreeWithPIC Minimalist.PICStrength.strong phases rel root = (Minimalist.validAgree rel root ∧ ¬∃ ph ∈ phases, ph.Impenetrable rel.goal)
• Minimalist.validAgreeWithPIC Minimalist.PICStrength.weak phases rel root = (Minimalist.validAgree rel root ∧ ¬∃ ph ∈ phases, ph.Impenetrable rel.goal)

def Minimalist.fullAgree (strength : PICStrength) (phases : List Phase) (rel : AgreeRelation) (root : SyntacticObject) : Prop

PIC-bounded Agree with Activity Condition.

The full Agree constraint: probe c-commands goal, feature matching holds, goal is active, AND no intervening phase boundary blocks the relation. See validAgreeWithPIC for the role of strength.

Equations

• Minimalist.fullAgree Minimalist.PICStrength.linearizationBound phases rel root = (Minimalist.validAgreeWithActivity rel root ∧ True)
• Minimalist.fullAgree Minimalist.PICStrength.strong phases rel root = (Minimalist.validAgreeWithActivity rel root ∧ ¬∃ ph ∈ phases, ph.Impenetrable rel.goal)
• Minimalist.fullAgree Minimalist.PICStrength.weak phases rel root = (Minimalist.validAgreeWithActivity rel root ∧ ¬∃ ph ∈ phases, ph.Impenetrable rel.goal)

def Minimalist.finAgreeFeatures (isFinite : Bool) : FeatureBundle

Fin-Agree: Fin probes for [±finite] on its complement (TP).

Equations

• Minimalist.finAgreeFeatures isFinite = Minimalist.FeatureBundle.ofGramFeatures [Minimalist.GramFeature.unvalued (Minimalist.FeatureVal.finite isFinite)]

def Minimalist.forceFinAgreeFeatures (isFactive : Bool) : FeatureBundle

Force-Fin-Agree: Force/C probes for clause-type features on Fin.

Equations

• Minimalist.forceFinAgreeFeatures isFactive = Minimalist.FeatureBundle.ofGramFeatures [Minimalist.GramFeature.unvalued (Minimalist.FeatureVal.factive isFactive)]

def Minimalist.negAgreeFeatures : FeatureBundle

Neg-Agree: Neg probes for [±neg], licensing sentential negation.

Equations

• Minimalist.negAgreeFeatures = Minimalist.FeatureBundle.ofGramFeatures [Minimalist.GramFeature.unvalued (Minimalist.FeatureVal.neg true)]

def Minimalist.relAgreeFeatures : FeatureBundle

Rel-Agree: Rel probes for [±rel], licensing relative clause formation.

Equations

• Minimalist.relAgreeFeatures = Minimalist.FeatureBundle.ofGramFeatures [Minimalist.GramFeature.unvalued (Minimalist.FeatureVal.rel true)]

theorem Minimalist.finite_features_match : featuresMatch (GramFeature.unvalued (FeatureVal.finite true)) (GramFeature.valued (FeatureVal.finite true)) = true

Clause-typing features match correctly.

theorem Minimalist.factive_features_match : featuresMatch (GramFeature.unvalued (FeatureVal.factive true)) (GramFeature.valued (FeatureVal.factive false)) = true

theorem Minimalist.neg_features_match : featuresMatch (GramFeature.unvalued (FeatureVal.neg true)) (GramFeature.valued (FeatureVal.neg true)) = true

theorem Minimalist.rel_features_match : featuresMatch (GramFeature.unvalued (FeatureVal.rel true)) (GramFeature.valued (FeatureVal.rel false)) = true

def Minimalist.phiProbe (ftype : FeatureVal) : Probe FeatureBundle

The φ-probe: relativized search ([BR03]/[Pre14]) for a goal bearing a valued ftype feature.

Equations

• Minimalist.phiProbe ftype = Minimalist.Probe.ofVis fun (gf : Minimalist.FeatureBundle) => (Minimalist.getValuedFeature gf ftype).isSome

theorem Minimalist.applyAgree_is_phi_transmit (probeFeats : FeatureBundle) (ftype : FeatureVal) {goals : List FeatureBundle} {gf : FeatureBundle} (h : (phiProbe ftype).search goals = some gf) : (phiProbe ftype).transmit (fun (g pf : FeatureBundle) => (applyAgree pf g ftype).getD pf) probeFeats goals = (applyAgree probeFeats gf ftype).getD probeFeats

applyAgree is the φ goal→probe transmission. A φ-Agree is Probe.transmit of the φ-probe with the valuation applyAgree: search the goal sequence for a ftype-bearing goal, then value the probe's features from it. This recognizes the standalone applyAgree as the transmission step of the unified Agree operation (Probe/Transmission.lean), rather than a parallel mechanism. (The probe→goal direction — dependent case — and a full clause's worth of valuations are folds of transmits: the composition axis, not a single transmit.)