Docs / Syntax / Minimalist / Probe / Agree

The Agree operation

import Linglib.Syntax.Minimalist.Probe.Agree · namespace Minimalist.Probe

In Deal's interaction and satisfaction theory, Agree inspects the goals in the probe's domain one at a time. A goal that interacts with the probe has its interacting features copied to the probe and is flagged as interacting; a goal that satisfies the probe is flagged as its satisfier and ends the search; and a goal bearing a feature marked for dynamic interaction changes the interaction condition for the goals after it. Probe.Dynamic.agree is this operation for a probe that depends on a state, Probe.agree its case for a fixed probe, and Probe.Spec.agree its case for feature specifications, Deal's algorithm (30).

For a fixed probe, a search that meets no interacting goal leaves the state unchanged, so Agree fails without penalty as Preminger argues; the single goal of Probe.goal is the case in which every interacting goal satisfies the probe; and Multiple Agree is the case of an insatiable probe.

This is the one Agree of the library. A theory of Agree supplies a probe, which fixes what the search finds, and a copying operation, which fixes what Agree does to the state: valuation of feature bundles (Minimalist.FeatureState.value), the value of a case (Minimalist.agree_eq_search), or the features a probe accumulates (Probe.Spec.agree). When the state is the list of goals itself, Agree replaces each entry it interacts with (Probe.agreeList). When copying joins the state with what each goal contributes, the order of the goals does not matter: Agree joins the initial state with the contributions of the goals it flags.

Main definitions

Minimalist.Probe.Result: the state Agree leaves, the goals flagged as interacting, and the satisfier.
Minimalist.Probe.Dynamic, Minimalist.Probe.Dynamic.agree: a probe depending on a state, and its Agree operation.
Minimalist.Probe.agree: Agree for a fixed probe and a copying operation.
Minimalist.Probe.inspected: the goals up to and including the first satisfier.
Minimalist.Probe.agreeList: Agree over the entries of a list that is itself the state.
Minimalist.Probe.Spec: interaction and satisfaction conditions, each a finite set of feature bundles presenting the upper set of bundles containing one of them.
Minimalist.Probe.Spec.ofFeatures: the conditions met by bearing any one of some features.
Minimalist.Probe.Spec.ofGeometry, Minimalist.Probe.Spec.relativized: [INT:f, SAT:g] over a feature geometry, interaction copying f and the features it dominates.
Minimalist.Probe.Spec.agree: Agree over goals exposing feature sets, with dynamic interaction.

Main results

Minimalist.Probe.Dynamic.agree_satisfier: when satisfaction ignores the state, the satisfier is the first goal that satisfies the probe.
Minimalist.Probe.agree_interacted, Minimalist.Probe.agree_state: a fixed probe flags the interacting inspected goals and copies from them in order.
Minimalist.Probe.agree_interacted_eq_goal, Minimalist.Probe.insatiable_agree_interacted: single-goal Agree and Multiple Agree as special cases.
Minimalist.Probe.Spec.agree_empty: without dynamic interaction a specification Agrees as the probe it denotes.
Minimalist.Probe.Spec.sup_toProbe_int, Minimalist.Probe.Spec.sup_toProbe_sat: the join of two specifications is a disjunctive probe.
Minimalist.Probe.Spec.ofGeometry_toProbe_int_iff: over a privative geometry, interacting with [INT:f] is bearing f.
Minimalist.Probe.Spec.subset_Ici_of_mem_dynamicUpdate: dynamic interaction narrows the interaction condition to the features a dynamic feature dominates.
Minimalist.Probe.Spec.foldl_dynamicUpdate, Minimalist.Probe.Spec.mem_agree_interacted_iff: the interaction condition a goal meets is the one the last goal before it bearing a dynamic feature sets, so the goals Agree flags are fixed by their position in the search.

Implementation notes

Movement, the M subfeatures of lines 5–6 and 9–10 of (30), is not modelled; Probe.attract gives movement a search of its own instead. Line 13 installs the closure of one feature marked for dynamic interaction; when a goal bears several, Spec.dynamicUpdate installs the features all of them dominate, which on a chain of features is the closure of the most specific one.

References

Deal 2025a, Current models of Agree formalized
Deal 2024, Interaction, Satisfaction, and the PCC formalized
Hiraiwa 2001, Multiple Agree and the Defective Intervention Constraint in Japanese
Preminger 2014, Agreement and Its Failures formalized

Declarations

The result of Agree over a goal sequence, the state after copying from every interacting goal, the goals flagged as interacting, in search order, and the goal flagged as the satisfier, if any.

structure Result L96–105

(α : Type u_4) (σ : Type u_5) :

Type (max u_4 u_5)

state : σ
The state after copying from every interacting goal.
interacted : List α
The goals flagged as interacting, in search order.
satisfier : Option α
The goal flagged as satisfying the probe, if the search was satisfied.

Used by Dynamic.agree, agree, Spec.agree

Used in Deal2024

A probe that depends on a state, as a probe under dynamic interaction depends on what it has met.

@[reducible, inline] abbrev Dynamic L109–111

(σ : Type u_4) (α : Type u_5) :

Type (max u_4 u_5)

Dynamic σ α = (σ → Minimalist.Probe α)

Used by Dynamic.agree, Dynamic.agree_nil, Dynamic.agree_cons, Dynamic.agree_satisfier

Agree for a probe that depends on a state. Each goal in turn is flagged and copied from if it interacts with the probe of the current state, ends the search if it satisfies it, and otherwise moves the state by update before the next goal.

def Dynamic.agree L117–128

{α : Type u_1} {σ : Type u_2} (P : Dynamic σ α) (copy update : α → σ → σ) :

σ → List α → Result α σ

The definition is too large to print here; read it in the source.

Built from ,

Used by Dynamic.agree_nil, Dynamic.agree_cons, Dynamic.agree_satisfier, agree

L132

L134–140

When satisfaction does not depend on the state, the satisfier is the first goal that satisfies the probe.

theorem Dynamic.agree_satisfier L142–150

{α : Type u_1} {σ : Type u_2} {P : Dynamic σ α} {copy update : α → σ → σ} {s : σ} {goals : List α} {q : Probe α} (h : ∀ (s : σ), (P s).sat = q.sat) :

(P.agree copy update s goals).satisfier = q.search goals

Built from ,

Agree for a fixed probe over an ordered goal sequence, copying from every interacting goal up to the first satisfier.

def agree L154–157

{α : Type u_1} {σ : Type u_2} (p : Probe α) (copy : α → σ → σ) :

σ → List α → Result α σ

p.agree copy = Dynamic.agree (fun (x : σ) => p) copy fun (x : α) (s : σ) => s

Built from ,

Used by agree_nil, agree_cons, agree_satisfier, agree_interacted, agree_state, le_agree_state, agree_state_eq_of_forall_not_int, agree_interacted_eq_goal, agree_state_eq_elim, relativized_agree_interacted, insatiable_agree_interacted, agree_sup_state, agreeList, Spec.agree_empty

Used in Syntax/Minimalist/Feature/Valuation, Syntax/Minimalist/Probe/Minimal, Amato2025

The goals a probe inspects, those before the first satisfying goal together with it.

def inspected L159–161

{α : Type u_1} (p : Probe α) (goals : List α) :

List α

p.inspected goals = List.takeWhile (fun (x : α) => decide ¬p.sat x) goals ++ (p.search goals).toList

Used by agree_interacted, mem_of_mem_inspected, inspected_filter_int_eq_goal, agree_sup_state, Spec.copied_agree_empty

Used in Syntax/Minimalist/Probe/Minimal

L165

L167–172

L174–176

The goals flagged as interacting are the inspected goals that interact.

@[simp] theorem agree_interacted L178–186

{α : Type u_1} {σ : Type u_2} {p : Probe α} {copy : α → σ → σ} {s : σ} {goals : List α} :

(p.agree copy s goals).interacted = List.filter (fun (x : α) => decide (p.int x)) (p.inspected goals)

Built from ,

The state is the fold of copy over the goals flagged as interacting.

theorem agree_state L188–196

{α : Type u_1} {σ : Type u_2} {p : Probe α} {copy : α → σ → σ} {s : σ} {goals : List α} :

(p.agree copy s goals).state = List.foldl (fun (s : σ) (a : α) => copy a s) s (p.agree copy s goals).interacted

Built from

When every interacting goal satisfies the probe, the only goal flagged as interacting is the goal of the probe.

theorem agree_interacted_eq_goal L232–236

{α : Type u_1} {σ : Type u_2} {p : Probe α} {copy : α → σ → σ} {s : σ} {goals : List α} (h : ∀ (a : α), p.int a → p.sat a) :

(p.agree copy s goals).interacted = (p.goal goals).toList

Built from

L238–244

L246–248

An insatiable probe flags every interacting goal, Multiple Agree (Hiraiwa 2001).

theorem insatiable_agree_interacted L250–255

{α : Type u_1} {σ : Type u_2} {copy : α → σ → σ} {s : σ} {goals : List α} (f : α → Prop) [DecidablePred f] :

((insatiable f).agree copy s goals).interacted = List.filter (fun (x : α) => decide (f x)) goals

Built from

When copying joins the state with what each goal contributes, Agree joins the initial state with the contributions of the goals it flags.

theorem agree_sup_state L257–266

{α : Type u_1} {σ : Type u_2} {p : Probe α} {s : σ} {goals : List α} [SemilatticeSup σ] [OrderBot σ] [DecidableEq α] (δ : α → σ) :

(p.agree (fun (a : α) (s : σ) => s ⊔ δ a) s goals).state = s ⊔ (List.filter (fun (x : α) => decide (p.int x)) (p.inspected goals)).toFinset.sup δ

Built from ,

Agree over a list of goals

Agree when the state is the list of goals itself: each interacting entry is replaced with f of it.

def agreeList L270–273

{α : Type u_1} (p : Probe α) (f : α → α) (l : List α) :

List α

p.agreeList f l = ((comap Prod.fst p).agree (fun (e : α × ℕ) (t : List α) => t.set e.2 (f e.1)) l l.zipIdx).state

Built from

Used by agreeList_nil, agreeList_cons

Used in BejarRezac2003

L286

L288–293

Feature specifications

A probe specification over a feature type, [INT:int, SAT:sat] in Deal 2025a's notation. Each condition lists bundles of features, and a goal meets it when it bears every feature of one of them, so that a condition presents the upper set of the bundles containing one of its own: [INT:Ā+D, SAT:D] is ⟨{{Ā, D}}, {{D}}⟩, and a condition listing several bundles is a disjunction.

structure Spec L297–307

(F : Type u_4) :

Type u_4

int : Finset (Finset F)
The bundles whose bearers the probe interacts with.
sat : Finset (Finset F)
The bundles whose bearers halt the probe's search.

Used by Spec.equivProd, Spec.instPartialOrder, Spec.le_def, Spec.instOrderBot, Spec.instLatticeOfDecidableEq, Spec.sup_int, Spec.sup_sat, Spec.ofFeatures, Spec.intFeatures, Spec.satFeatures, Spec.toProbe, Spec.toProbe_int, Spec.toProbe_sat, Spec.sup_toProbe_int, Spec.sup_toProbe_sat, Spec.ofGeometry, Spec.relativized, Spec.agree, Spec.agree_satisfier, Spec.agree_empty, Spec.copied_agree_empty, Spec.mem_agree_interacted_iff

Used in Syntax/Minimalist/Probe/Minimal, BrananErlewine2024, Deal2025a, HammerlyMathieu2026

The specification whose bundles are single features, interacting with a goal that bears a feature of int and satisfied by one that bears a feature of sat.

def Spec.ofFeatures L339–341

{F : Type u_3} (int sat : Finset F) :

Spec F

Spec.ofFeatures int sat = { int := Finset.powersetCard 1 int, sat := Finset.powersetCard 1 sat }

Built from

Used by Spec.ofFeatures_toProbe_int, Spec.ofFeatures_toProbe_sat, Spec.ofFeatures_intFeatures, Spec.ofFeatures_satFeatures, Spec.ofGeometry

Used in Deal2025a

The join interacts with a goal iff either specification does.

theorem Spec.sup_toProbe_int L378–381

{α : Type u_1} {F : Type u_3} [DecidableEq F] {sp : Spec F} {feats : α → Finset F} {sp' : Spec F} {a : α} :

((sp ⊔ sp').toProbe feats).int a ↔ (sp.toProbe feats).int a ∨ (sp'.toProbe feats).int a

Built from ,

The join is satisfied by a goal iff either specification is.

theorem Spec.sup_toProbe_sat L383–386

{α : Type u_1} {F : Type u_3} [DecidableEq F] {sp : Spec F} {feats : α → Finset F} {sp' : Spec F} {a : α} :

((sp ⊔ sp').toProbe feats).sat a ↔ (sp.toProbe feats).sat a ∨ (sp'.toProbe feats).sat a

Built from ,

The specification [INT:f, SAT:g] over a feature geometry, in which a feature is below the features it dominates: interaction with f copies f and every feature it dominates, (8a) of Deal 2024, and satisfaction is bearing g.

def Spec.ofGeometry L410–413

{F : Type u_3} [Preorder F] [LocallyFiniteOrderTop F] (f g : F) :

Spec F

Spec.ofGeometry f g = Spec.ofFeatures (Finset.Ici f) {g}

Built from ,

Used by Spec.relativized, Spec.ofGeometry_intFeatures, Spec.ofGeometry_toProbe_int_iff

The relativized probe [INT:f, SAT:f].

@[reducible, inline] abbrev Spec.relativized L415–416

{F : Type u_3} [Preorder F] [LocallyFiniteOrderTop F] (f : F) :

Spec F

Spec.relativized f = Spec.ofGeometry f f

Built from ,

Used in HammerlyMathieu2026

L420–422

When a goal bears every feature dominating one it bears, as in a privative geometry, it interacts with [INT:f] exactly when it bears f.

theorem Spec.ofGeometry_toProbe_int_iff L424–431

{α : Type u_1} {F : Type u_3} [DecidableEq F] {feats : α → Finset F} {a : α} [Preorder F] [LocallyFiniteOrderTop F] {f g : F} (hc : ∀ x ∈ feats a, ∀ y ≤ x, y ∈ feats a) :

((ofGeometry f g).toProbe feats).int a ↔ f ∈ feats a

Built from ,

L441–444

Agree (30) of Deal 2025a over goals exposing feature sets, dyn the features marked for dynamic interaction. The probe interacts by the current interaction condition, which starts as sp.int.

def Spec.agree L446–452

{α : Type u_1} {F : Type u_3} [DecidableEq F] (sp : Spec F) (feats : α → Finset F) [Preorder F] [LocallyFiniteOrderTop F] (dyn : Finset F) (goals : List α) :

Result α (State F)

The definition is too large to print here; read it in the source.

Built from , ,

Used by Spec.agree_satisfier, Spec.agree_empty, Spec.copied_agree_empty, Spec.mem_agree_interacted_iff

L454–458

Dynamic interaction narrows the interaction condition to the features that a dynamic feature of the goal dominates.

theorem Spec.subset_Ici_of_mem_dynamicUpdate L460–468

{α : Type u_1} {F : Type u_3} [DecidableEq F] (feats : α → Finset F) [Preorder F] [LocallyFiniteOrderTop F] (dyn : Finset F) {a : α} {x : F} (hx : x ∈ feats a ∩ dyn) {int : Finset (Finset F)} {m : Finset F} (hm : m ∈ dynamicUpdate feats dyn a int) :

m ⊆ Finset.Ici x

Built from

L470–472

Without dynamic interaction, a specification Agrees as the probe it denotes, copying the interaction-specified features of each interacting goal.

theorem Spec.agree_empty L474–487

{α : Type u_1} {F : Type u_3} [DecidableEq F] (sp : Spec F) (feats : α → Finset F) [Preorder F] [LocallyFiniteOrderTop F] (goals : List α) :

sp.agree feats ∅ goals = have r := (sp.toProbe feats).agree (fun (a : α) (c : Finset F) => c ∪ sp.intFeatures feats a) ∅ goals; { state := { copied := r.state, int := sp.int }, interacted := r.interacted, satisfier := r.satisfier }

Built from , , , ,

L489–497

L499–502

L504–506

After a sequence of goals the interaction condition is the one the last goal bearing a dynamic feature sets, and the initial condition if no goal bears one.

theorem Spec.foldl_dynamicUpdate L508–521

{α : Type u_1} {F : Type u_3} [DecidableEq F] (feats : α → Finset F) [Preorder F] [LocallyFiniteOrderTop F] (dyn : Finset F) (int : Finset (Finset F)) (l : List α) :

List.foldl (fun (i : Finset (Finset F)) (a : α) => dynamicUpdate feats dyn a i) int l = (List.filter (fun (a : α) => decide (feats a ∩ dyn).Nonempty) l).getLast?.elim int fun (b : α) => dynamicUpdate feats dyn b int

Built from

Agree with dynamic interaction flags a goal iff no goal before it satisfies the probe and it bears a feature of the interaction condition the goals before it leave, which foldl_dynamicUpdate reads off the last of them bearing a dynamic feature.

theorem Spec.mem_agree_interacted_iff L580–588

{α : Type u_1} {F : Type u_3} [DecidableEq F] (sp : Spec F) (feats : α → Finset F) [Preorder F] [LocallyFiniteOrderTop F] (dyn : Finset F) {a : α} (goals : List α) :

a ∈ (sp.agree feats dyn goals).interacted ↔ ∃ (l₁ : List α) (l₂ : List α), goals = l₁ ++ a :: l₂ ∧ (∀ b ∈ l₁, ¬(sp.toProbe feats).sat b) ∧ feats a ∈ upperClosure ↑(List.foldl (fun (i : Finset (Finset F)) (b : α) => dynamicUpdate feats dyn b i) sp.int l₁)

Built from , , ,