Docs / Syntax / Minimalist / Probe / Minimal

Relativized Minimality

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

Source

A probe finds the goals of its domain that satisfy it and that no satisfying goal is closer than. Closeness is read through a key into an ordered type, such as a goal's position in a list, its class of equidistant goals, or the nodes that dominate it, so finding is mathlib's MinimalFor and a theory of closeness is a choice of key. Agree inspects the goals that no satisfier is closer than and agrees with those of them that interact. Keyed by position, these are Probe.search and Probe.inspected.

Main definitions

Main results

References

Declarations

A probe finds a goal of s that satisfies it and that no satisfying goal of s is closer than, closeness read through key: Relativized Minimality (Rizzi 1990).

def FindsL62–64
{α : Type u_1} {β : Type u_2} [Preorder β] (p : Probe α) (s : Set α) (key : α → β) (a : α) :
Prop
  • p.Finds s key a = MinimalFor (fun (b : α) => b ∈ s ∧ p.sat b) key a

Used by finds_iff, Finds.inspects, Finds.sat, Finds.mem, Finds.le, exists_finds, Finds.of_subset, Finds.of_refines, agreesWith_iff_finds, agreesWith_relativized_iff, instDecidablePredFinds, Finds.of_bestMatch, finds_ancestors_iff, not_finds_ancestors_of_lt, search_eq_some_iff_finds

Used in Syntax/Minimalist/Probe/SyntacticObject, BrananErlewine2026, Storment2026, Zeijlstra2012

A probe inspects a goal of s that no satisfying goal of s is closer than.

def InspectsL66–67
{α : Type u_1} {β : Type u_2} [Preorder β] (p : Probe α) (s : Set α) (key : α → β) (a : α) :
Prop
  • p.Inspects s key a = (a ∈ s ∧ ∀ ⦃b : α⦄, b ∈ s → p.sat b → ¬key b < key a)

Used by AgreesWith, finds_iff, Finds.inspects, Inspects.mem, Inspects.of_subset, inspects_insatiable_iff, instDecidablePredInspects, instDecidablePredFinds, instDecidablePredAgreesWith, mem_inspected_iff_inspects

A probe agrees with a goal it inspects and interacts with (Deal 2025a).

def AgreesWithL69–70
{α : Type u_1} {β : Type u_2} [Preorder β] (p : Probe α) (s : Set α) (key : α → β) (a : α) :
Prop

Built from

Used by agreesWith_iff_finds, agreesWith_relativized_iff, agreesWith_insatiable_iff, instDecidablePredAgreesWith, Spec.copied, Spec.mem_copied_iff, mem_agree_interacted_iff

Used in Syntax/Minimalist/Probe/Movement, Storment2026

A probe finds the inspected goals that satisfy it.

theorem finds_iffL74–81
{α : Type u_1} {β : Type u_2} [Preorder β] {p : Probe α} {s : Set α} {key : α → β} {a : α} :
p.Finds s key a ↔ p.Inspects s key a ∧ p.sat a

Built from ,

L83
L85
L87
L89
L91–93

Under a well-founded key, a probe with a satisfier in its domain finds a goal.

theorem exists_findsL95–97
{α : Type u_1} {β : Type u_2} [Preorder β] {p : Probe α} {s : Set α} {key : α → β} [WellFoundedLT β] (h : ∃ a ∈ s, p.sat a) :
∃ (a : α), p.Finds s key a

Built from

A goal inspected in a domain is inspected in any part of it that contains the goal, as a horizon cuts the domain.

theorem Inspects.of_subsetL99–103
{α : Type u_1} {β : Type u_2} [Preorder β] {p : Probe α} {s : Set α} {key : α → β} {a : α} {t : Set α} (h : p.Inspects s key a) (hts : t ⊆ s) (ha : a ∈ t) :
p.Inspects t key a

Built from

L105–108

A goal found under a key that refines another is found under that one: a goal closer under the coarser key is closer under the finer.

theorem Finds.of_refinesL110–114
{α : Type u_1} {β : Type u_2} [Preorder β] {p : Probe α} {s : Set α} {key : α → β} {a : α} {γ : Type u_3} [Preorder γ] {key' : α → γ} (hk : ∀ ⦃a b : α⦄, key a < key b → key' a < key' b) (h : p.Finds s key' a) :
p.Finds s key a

Built from

When every interacting goal satisfies the probe, it agrees with the goals it finds that interact.

theorem agreesWith_iff_findsL116–121
{α : Type u_1} {β : Type u_2} [Preorder β] {p : Probe α} {s : Set α} {key : α → β} {a : α} (hp : ∀ (a : α), p.int a → p.sat a) :
p.AgreesWith s key a ↔ p.Finds s key a ∧ p.int a

Built from ,

L128–130
L132–134

Finite domains

L142–143
L145
L147

Feature specifications: Best Match and copying

L162–165

The features Agree copies, the interaction features of the goals the probe agrees with.

def Spec.copiedL167–170
{α : Type u_1} {β : Type u_2} [Preorder β] {F : Type u_3} [DecidableEq F] (sp : Spec F) (feats : α → Finset F) [Fintype α] (s : Set α) [DecidablePred fun (x : α) => x ∈ s] (key : α → β) [DecidableRel fun (x1 x2 : β) => x1 < x2] :
Finset F

Built from

Used by Spec.mem_copied_iff

L174–178

A goal found under Best Match is found under the closeness it refines.

theorem Finds.of_bestMatchL182–186
{α : Type u_1} {β : Type u_2} [Preorder β] {s : Set α} {key : α → β} {a : α} {F : Type u_3} [DecidableEq F] {sp : Spec F} {feats : α → Finset F} (h : (sp.toProbe feats).Finds s (sp.bestMatch feats key) a) :
(sp.toProbe feats).Finds s key a

Built from ,

Closeness in phrase structure

Among satisfiers none of which dominates another, a probe finds those that no satisfier asymmetrically commands, the Minimal Link Condition.

theorem finds_ancestors_iffL197–202
{α : Type u_3} [PartialOrder α] {P : Set α} {p : Probe α} {s : Set α} {a : α} (hs : IsAntichain (fun (x1 x2 : α) => x1 ≤ x2) {b : α | b ∈ s ∧ p.sat b}) :
p.Finds s (PhraseStructure.ancestors P) a ↔ (a ∈ s ∧ p.sat a) ∧ ∀ ⦃b : α⦄, b ∈ s → p.sat b → ¬((b, a) ∈ PhraseStructure.commandRelation P ∧ (a, b) ∉ PhraseStructure.commandRelation P)

Built from

A probe does not find a goal that a satisfier dominates through a generator: the container is found before what it contains, as the A-over-A principle requires.

theorem not_finds_ancestors_of_ltL204–208
{α : Type u_3} [PartialOrder α] {P : Set α} {p : Probe α} {s : Set α} {a b x : α} (hb : b ∈ s) (hsb : p.sat b) (hbx : b ≤ x) (hxa : x < a) (hx : x ∈ P) :
¬p.Finds s (PhraseStructure.ancestors P) a

Built from

The list search, keyed by position

The list search is Relativized Minimality keyed by position.

theorem search_eq_some_iff_findsL268–270
{α : Type u_1} {p : Probe α} {a : α} [DecidableEq α] {l : List α} :
p.search l = some a ↔ p.Finds {b : α | b ∈ l} (fun (a : α) => List.idxOf a l) a

Built from

The list Agree flags the goals the probe agrees with, keyed by position.

theorem mem_agree_interacted_iffL272–275
{α : Type u_1} {p : Probe α} {a : α} [DecidableEq α] {l : List α} {σ : Type u_3} {copy : α → σ → σ} {st : σ} :
a ∈ (p.agree copy st l).interacted ↔ p.AgreesWith {b : α | b ∈ l} (fun (a : α) => List.idxOf a l) a

Built from