Control: Basic Definitions

The framework-neutral vocabulary of control. A dependency is a relation SetRel Pos Pos over argument positions, read antecedent ~[r] dependent, with a valuation val : Pos → Ref assigning referents — [Sti07]'s mechanism-neutral definition of control as referential inclusion, "open as to how the control reading is obtained". Reading types follow [Lan00a]: exhaustive (IsExhaustive), partial (IsPartial), and split (IsSplit); control shift varies the antecedent across readings of one construction, so it is not a property of a single dependency. Mechanism names what a dependency shares ([Bre82]'s functional vs. anaphoric cut), and IsSaturating is the bi-unique, exhaustive profile of saturation (predication, structure sharing). Grammatical dependencies share [Kos87]'s configurational-matrix format ([NvdK02]), whose clauses are mathlib vocabulary: refinement r ⊆ s, Relator.LeftUnique, dependent ⊆ r.cod. Lemmas are in Syntax/Control/Basic.lean.

Main definitions

• Control.IsExhaustive, Control.IsPartial, Control.IsSplit
• Control.Mechanism
• Control.IsSaturating

def Control.IsExhaustive {Pos : Type u_1} {Ref : Type u_2} (val : Pos → Ref) (ante : SetRel Pos Pos) : Prop

Exhaustive control ([Lan00a]): the dependency shares the valuation exhaustively — related positions are co-valued, i.e. the dependency refines the kernel of the valuation.

Equations

• Control.IsExhaustive val ante = (ante ⊆ {(a, b) : Pos × Pos | val a = val b})

def Control.IsPartial {Pos : Type u_1} {Ref : Type u_2} [Preorder Ref] (val : Pos → Ref) (d : SetRel Pos Pos) : Prop

A partial reading ([Lan00a]): some dependent's referent strictly extends its controller's.

Equations

• Control.IsPartial val d = ∃ (a : Pos), ∃ (b : Pos), (a, b) ∈ d ∧ val a < val b

@[reducible, inline]

abbrev Control.IsSplit {Pos : Type u_1} (d : SetRel Pos Pos) : Prop

Split control: some dependent has two distinct controllers — the dependency is not left-unique.

Equations

• Control.IsSplit d = ¬Relator.LeftUnique fun (x1 x2 : Pos) => (x1, x2) ∈ d

inductive Control.Mechanism : Type

What a control dependency shares — the framework-neutral cut behind the movement vs. base-generation and functional vs. anaphoric ([Bre82]) oppositions.

• occupant : Mechanism

  Token identity: the occupant assignment itself is shared (movement chains; LFG functional control).

• referent : Mechanism

  Referential co-valuation only (LFG anaphoric control; predication).

• composite : Mechanism

  A binding leg composed over a predication leg ([Lan24]).

• free : Mechanism

  No grammatical dependency (non-obligatory control).

@[instance_reducible]

instance Control.instDecidableEqMechanism : DecidableEq Mechanism

Equations

• Control.instDecidableEqMechanism x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Control.instReprMechanism.repr : Mechanism → ℕ → Std.Format

Equations

• Control.instReprMechanism.repr Control.Mechanism.occupant prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Control.Mechanism.occupant")).group prec✝
• Control.instReprMechanism.repr Control.Mechanism.referent prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Control.Mechanism.referent")).group prec✝
• Control.instReprMechanism.repr Control.Mechanism.composite prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Control.Mechanism.composite")).group prec✝
• Control.instReprMechanism.repr Control.Mechanism.free prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Control.Mechanism.free")).group prec✝

@[instance_reducible]

instance Control.instReprMechanism : Repr Mechanism

Equations

• Control.instReprMechanism = { reprPrec := Control.instReprMechanism.repr }

structure Control.IsSaturating {Pos : Type u_1} {Ref : Type u_2} (val : Pos → Ref) (d : SetRel Pos Pos) : Prop

The profile of a dependency enforced by saturation (predication, structure sharing): each dependent has a unique controller, each controller saturates a single slot, and the referent is shared exhaustively.

• biUnique : Relator.BiUnique fun (x1 x2 : Pos) => (x1, x2) ∈ d
• exhaustive : IsExhaustive val d