Docs / Syntax / Minimalist / Probe / Movement

Movement probes

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

Source

A head may carry conditions on movement as well as on agreement, each an interaction and a satisfaction specification, a relativized EPP. A movement probe attracts the goal it agrees with to its specifier, and since Merge is binary it attracts at most one: a probe that agrees with two goals attracts neither, the Ban on Multiple Move. On a linearized syntactic object a probe on a head searches the positions the head c-commands, and the goal it attracts is the mover of an Internal Merge step.

Main definitions

Main results

Implementation notes

Movement is a search of its own, with its own conditions. The movement subfeatures of the algorithm Probe.Spec.agree implements, which move goals of the agreement search, are not modelled.

References

Declarations

L56–57

The goal a movement probe attracts, the one goal it agrees with. Binary Merge cannot move two goals at once (Coon & Keine 2021), and a probe that agrees with several attracts none, the Ban on Multiple Move of Hammerly & Mathieu 2026.

def Probe.attractL59–63
{α : Type u_1} {β : Type u_2} [Preorder β] [Fintype α] [DecidableEq α] (p : Probe α) (s : Set α) [DecidablePred fun (x : α) => x ∈ s] (key : α → β) [DecidableRel fun (x1 x2 : β) => x1 < x2] :
Option α

Used by Probe.attract_eq_some_iff, Probe.attract_eq_none_of_ne, LinearizedSyntacticObject.attractStep?, LinearizedSyntacticObject.attractStep?_eq_some_iff

theorem Probe.attract_eq_some_iffL67–81
{α : Type u_1} {β : Type u_2} [Preorder β] [Fintype α] [DecidableEq α] {p : Probe α} {s : Set α} [DecidablePred fun (x : α) => x ∈ s] {key : α → β} [DecidableRel fun (x1 x2 : β) => x1 < x2] {a : α} :
p.attract s key = some a ↔ p.AgreesWith s key a ∧ ∀ (b : α), p.AgreesWith s key b → b = a

Built from

The Ban on Multiple Move: a probe agreeing with two goals attracts neither.

theorem Probe.attract_eq_none_of_neL83–88
{α : Type u_1} {β : Type u_2} [Preorder β] [Fintype α] [DecidableEq α] {p : Probe α} {s : Set α} [DecidablePred fun (x : α) => x ∈ s] {key : α → β} [DecidableRel fun (x1 x2 : β) => x1 < x2] {a b : α} (ha : p.AgreesWith s key a) (hb : p.AgreesWith s key b) (hab : a ≠ b) :
p.attract s key = none

Built from

The Internal Merge a movement probe searching the positions s of t triggers, those its head c-commands or a part of them: the term at the goal it attracts re-merges.

def LinearizedSyntacticObject.attractStep?L96–100
{β : Type u_1} [Preorder β] [DecidableRel fun (x1 x2 : β) => x1 < x2] (t : LinearizedSyntacticObject) (p : Probe (↑t).Positions) (s : Set (↑t).Positions) [DecidablePred fun (x : (↑t).Positions) => x ∈ s] (key : (↑t).Positions → β) :
Option Step

Built from

Used by LinearizedSyntacticObject.attractStep?_eq_some_iff

theorem LinearizedSyntacticObject.attractStep?_eq_some_iffL102–106
{β : Type u_1} [Preorder β] [DecidableRel fun (x1 x2 : β) => x1 < x2] {t : LinearizedSyntacticObject} {p : Probe (↑t).Positions} {s : Set (↑t).Positions} [DecidablePred fun (x : (↑t).Positions) => x ∈ s] {key : (↑t).Positions → β} {step : Step} :
t.attractStep? p s key = some step ↔ ∃ (q : (↑t).Positions), p.attract s key = some q ∧ step = Step.im (t.termAt q)

Built from ,