Agree: closest goals, horizons, and valuation

This file defines the structural conditions of Agree over syntactic objects and its valuation step over feature bundles. A closest goal for a probe is a node of the probe's c-command domain that satisfies the probe's relativization and that no other such node asymmetrically c-commands, which is the Minimal Link Condition of [Cho95b] with mutually c-commanding candidates equidistant. A target lies behind a horizon for a probe when a leaf of the horizon category lies in the probe's domain and c-commands the target, so that the probe's search terminates before reaching it ([Kei19]). Valuation copies a goal's value into an unvalued probe slot and is inflationary in the subsumption order on bundles, so Agree only adds information.

The closest-goal predicate is the tree-native form of the list search Probe.search. A probe's search over an enumeration of its domain sorted by c-command finds one of its closest visible goals (isClosestGoalIn_of_search_eq_some).

Main definitions

• Minimalist.SyntacticObject.isClosestGoalIn: a goal in the probe's domain that no other candidate asymmetrically c-commands.
• Minimalist.SyntacticObject.behindHorizonIn: a target c-commanded by a horizon-category leaf in the probe's domain.
• Minimalist.FeatureBundle.valueAt, Minimalist.FeatureBundle.applyAgree: valuation of an unvalued slot, and the probe's bundle valued from a goal's.

References

• [Cho95b], [Cho00]
• [Kei19]
• [AP25]

Closest goals

def Minimalist.SyntacticObject.isClosestGoalIn (root probe goal : SyntacticObject) (pred : SyntacticObject → Prop) : Prop

A closest pred-goal for probe in root is a node of probe's c-command domain satisfying pred that no other pred-node of the domain asymmetrically c-commands. Mutually c-commanding candidates are equidistant and do not block each other.

Equations

• root.isClosestGoalIn probe goal pred = (goal ∈ root.cCommandDomain probe ∧ pred goal ∧ ∀ x ∈ root.cCommandDomain probe, pred x → ¬root.AsymmCCommands x goal)

@[instance_reducible]

instance Minimalist.SyntacticObject.instDecidableIsClosestGoalInOfDecidablePred {pred : SyntacticObject → Prop} [DecidablePred pred] (root probe goal : SyntacticObject) : Decidable (root.isClosestGoalIn probe goal pred)

Equations

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

theorem Minimalist.SyntacticObject.isClosestGoalIn_of_search_eq_some {root probe goal : SyntacticObject} {p : Probe SyntacticObject} {dom : List SyntacticObject} (hdom : ↑dom = root.cCommandDomain probe) (hord : List.Pairwise (fun (x y : SyntacticObject) => ¬root.AsymmCCommands y x) dom) (h : p.search dom = some goal) : root.isClosestGoalIn probe goal fun (x : SyntacticObject) => p.sat x = true

A probe's search over an enumeration of its domain sorted by c-command finds one of its closest visible goals.

theorem Minimalist.SyntacticObject.isClosestGoalIn_iff_forall_not_sister {root probe goal : SyntacticObject} {pred : SyntacticObject → Prop} : root.isClosestGoalIn probe goal pred ↔ goal ∈ root.cCommandDomain probe ∧ pred goal ∧ ∀ x ∈ root.cCommandDomain probe, pred x → ¬root.Sisters x goal → ¬root.AsymmCCommands x goal

Sisters are equidistant. A closest goal need only be free of asymmetric c-command by the pred-nodes of the domain that are not its sisters, since a sister never asymmetrically c-commands it.

Horizons

def Minimalist.SyntacticObject.behindHorizonIn (root probe target : SyntacticObject) (c : Cat) : Prop

A target lies behind a horizon of category c for probe in root when a c leaf of probe's c-command domain c-commands it, so that probe's search terminates before reaching it ([Kei19]). With N a horizon for the wh-probe on C, the D head of [DP D [PossP Psr N]] stays visible while the possessor, c-commanded by N, does not ([AP25]).

Equations

• root.behindHorizonIn probe target c = ∃ n ∈ root.cCommandDomain probe, Minimalist.SyntacticObject.isLeafOf c n ∧ root.CCommands n target

@[instance_reducible]

instance Minimalist.SyntacticObject.instDecidableBehindHorizonIn (root probe target : SyntacticObject) (c : Cat) : Decidable (root.behindHorizonIn probe target c)

Equations

• root.instDecidableBehindHorizonIn probe target c = Multiset.decidableExistsMultiset

Valuation

def Minimalist.FeatureBundle.valueAt (b : FeatureBundle) (t : FeatureType) (v : t.ValueOf) : FeatureBundle

The bundle b with dimension t valued by v when its slot is unvalued; a valued or absent slot is left as it is.

Equations

• b.valueAt t v = Function.update b t (Minimalist.FeatureSlot.valueWith v (b t))

@[simp]

theorem Minimalist.FeatureBundle.valueAt_apply_self (t : FeatureType) (b : FeatureBundle) (v : t.ValueOf) : b.valueAt t v t = FeatureSlot.valueWith v (b t)

theorem Minimalist.FeatureBundle.le_valueAt (t : FeatureType) (b : FeatureBundle) (v : t.ValueOf) : b ≤ b.valueAt t v

Valuation is inflationary in the subsumption order, so Agree only adds information.

def Minimalist.FeatureBundle.applyAgree (probe goal : FeatureBundle) (t : FeatureType) : Option FeatureBundle

The probe's bundle valued from the goal's value at dimension t, or none when the goal has no value to transmit.

Equations

• probe.applyAgree goal t = Option.map (probe.valueAt t) (goal.getValuedFeature t)

@[simp]

theorem Minimalist.FeatureBundle.applyAgree_bot (probe : FeatureBundle) (t : FeatureType) : probe.applyAgree ⊥ t = none

theorem Minimalist.FeatureBundle.applyAgree_eq_none_iff (probe goal : FeatureBundle) (t : FeatureType) : probe.applyAgree goal t = none ↔ ¬goal.hasValuedFeature t = true

theorem Minimalist.FeatureBundle.le_of_applyAgree_eq_some (probe goal : FeatureBundle) (t : FeatureType) {probe' : FeatureBundle} (h : probe.applyAgree goal t = some probe') : probe ≤ probe'

A probe valued by Agree only gains information.