Selection-driven heads on the SyntacticObject carrier

This file defines the c-selection head of a syntactic object: whichever sister's head selects the saturated other projects — [Adg03]'s identification of the projecting item with the selecting item, instantiating the bare-phrase-structure projection ([Cho95a] §4) that [MCB25] §1.13.3 abstracts as head functions (Definition 1.13.6 / Lemma 1.13.7). Like the book's head functions it is partial: 0 at exocentric nodes.

Main declarations

• Minimalist.SelectionState: a constituent's selection state — the projecting head with its residual selectional stack; a CommMagma and MulZeroClass, with 0 the off-Dom(h) failure.
• Mul SelectionState and Minimalist.selSide: the carrier-free combinators — the selection product, and which daughter projects.
• Minimalist.selNode, Minimalist.selCheckPlanar, Minimalist.SyntacticObject.selCheck: the selection algebra (SyntacticObject.mergeAlgebra), its catamorphism, and the carrier lift.
• Minimalist.SyntacticObject.selHead, Minimalist.SyntacticObject.outerCatC: the head token and its outer category — the foundation the Phase API consumes (isPhaseHeadOf).
• Minimalist.SyntacticObject.selCheckHom: selCheck as a morphism of magmas SyntacticObject →ₙ* SelectionState, via SyntacticObject.lift.

Main results

• mul_comm (via CommMagma SelectionState) and Minimalist.selSide_comm: order-independence — the formal content of Merge's unordered output.
• Minimalist.SyntacticObject.selHead_node: endocentricity — a node's head is one of its daughters' heads.

Implementation notes

SelectionState is a one-field structure over Option (LIToken × List Cat): the Option is implementation, 0 is the public spelling of the exocentric failure — the absorbing element of [MCB25]'s renormalization reading of partial head functions (off-domain values as the "meaningless infinities" of computation, their §1.13.2 remark). No One (two saturated states multiply to 0 — exocentricity is a zero divisor) and no associativity claim, so the structure is CommMagma + MulZeroClass only. Index-free traces: a bare trace leaf gets the canonical saturated value .of (mkTraceToken 0) []; selCheck reads only the token's category and outerSel, both index-independent.

The selection state

structure Minimalist.SelectionState : Type

A constituent's selection state: the projecting head with its residual stack (.of tok [] = saturated), 0 off the endocentric domain.

• toOption : Option (LIToken × List Cat)

@[instance_reducible]

instance Minimalist.instDecidableEqSelectionState : DecidableEq SelectionState

Equations

• Minimalist.instDecidableEqSelectionState = Minimalist.instDecidableEqSelectionState.decEq

def Minimalist.instDecidableEqSelectionState.decEq (x✝ x✝¹ : SelectionState) : Decidable (x✝ = x✝¹)

Equations

• Minimalist.instDecidableEqSelectionState.decEq { toOption := a } { toOption := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

def Minimalist.SelectionState.of (tok : LIToken) (stack : List Cat) : SelectionState

A defined selection state: projecting head tok with residual stack stack.

Equations

• Minimalist.SelectionState.of tok stack = { toOption := some (tok, stack) }

@[instance_reducible]

instance Minimalist.instZeroSelectionState : Zero SelectionState

Equations

• Minimalist.instZeroSelectionState = { zero := { toOption := none } }

def Minimalist.SelectionState.head (x : SelectionState) : Option LIToken

The projecting head token; none off the endocentric domain.

Equations

• x.head = Option.map (fun (x : Minimalist.LIToken × List Minimalist.Cat) => x.1) x.toOption

def Minimalist.SelectionState.residual (x : SelectionState) : Option (List Cat)

The residual selectional stack (some [] = saturated).

Equations

• x.residual = Option.map (fun (x : Minimalist.LIToken × List Minimalist.Cat) => x.2) x.toOption

@[simp]

theorem Minimalist.SelectionState.head_of (tok : LIToken) (stack : List Cat) : (of tok stack).head = some tok

@[simp]

theorem Minimalist.SelectionState.head_zero : head 0 = none

Carrier-free selection combinators

def Minimalist.selCombine : SelectionState → SelectionState → Option (Bool × LIToken × List Cat)

The selection decision at a binary node — (which sister projects, head, residual), none at exocentric nodes; * and selSide are its projections.

Equations

• Minimalist.selCombine { toOption := some (ha, c :: rest) } { toOption := some (hb, []) } = if hb.item.outerCat = c then some (true, ha, rest) else none
• Minimalist.selCombine { toOption := some (ha, []) } { toOption := some (hb, c :: rest) } = if ha.item.outerCat = c then some (false, hb, rest) else none
• Minimalist.selCombine x✝¹ x✝ = none

def Minimalist.selSide (x y : SelectionState) : Option Bool

Which daughter projects: some true = left, some false = right.

Equations

• Minimalist.selSide x y = Option.map (fun (x : Bool × Minimalist.LIToken × List Minimalist.Cat) => x.1) (Minimalist.selCombine x y)

theorem Minimalist.selCombine_comm (x y : SelectionState) : selCombine x y = Option.map (fun (p : Bool × LIToken × List Cat) => (!p.1, p.2)) (selCombine y x)

Swapping the sisters flips the side and keeps the head and residual.

theorem Minimalist.selSide_comm (x y : SelectionState) : selSide x y = Option.map not (selSide y x)

S₂-equivariance: swap acts on the sisters, Bool.not on the side — MCB's per-vertex edge-marking (Lemma 1.13.4).

@[instance_reducible]

instance Minimalist.instMulZeroClassSelectionState : MulZeroClass SelectionState

The selection product: the head-and-residual of the selCombine decision ([MCB25] §1.13); 0 is absorbing.

Equations

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

theorem Minimalist.SelectionState.mul_def (x y : SelectionState) : x * y = { toOption := Option.map (fun (x : Bool × LIToken × List Cat) => x.2) (selCombine x y) }

* unfolded: the canonical accessor for the selection product.

@[instance_reducible]

instance Minimalist.instCommMagmaSelectionState : CommMagma SelectionState

Equations

• Minimalist.instCommMagmaSelectionState = { toMul := Minimalist.instMulZeroClassSelectionState.toMul, mul_comm := Minimalist.instCommMagmaSelectionState._proof_1 }

theorem Minimalist.selCombine_eq_some {x y : SelectionState} {b : Bool} {hd : LIToken} {res : List Cat} (h : selCombine x y = some (b, hd, res)) : (bif b then x else y).head = some hd

Coherence: the projected head is the head of the sister on the reported side.

theorem Minimalist.SelectionState.head_mul {x y : SelectionState} {r : LIToken} (h : (x * y).head = some r) : x.head = some r ∨ y.head = some r

The head of x * y (when defined) is one of x/y's heads.

Selection check on the carriers

def Minimalist.selNode : SOLabel → List SelectionState → SelectionState

The selection algebra: the SyntacticObject.mergeAlgebra of token + outerSel leaves and the saturated, index-free trace.

Equations

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

theorem Minimalist.selNode_perm (a : SOLabel) {l₁ l₂ : List SelectionState} (h : l₁.Perm l₂) : selNode a l₁ = selNode a l₂

selNode is invariant under permutation of the daughter states.

def Minimalist.selCheckPlanar : RoseTree SOLabel → SelectionState

Selection check on a planar tree: the catamorphism of selNode.

Equations

• Minimalist.selCheckPlanar = RoseTree.fold Minimalist.selNode

theorem Minimalist.selCheckPlanar_node (a : SOLabel) (cs : List (RoseTree SOLabel)) : selCheckPlanar (RoseTree.node a cs) = selNode a (List.map selCheckPlanar cs)

Reduction of selCheckPlanar at a node: fold the algebra over the daughters.

theorem Minimalist.selCheckPlanar_perm {t s : RoseTree SOLabel} (h : t.Perm s) : selCheckPlanar t = selCheckPlanar s

selCheckPlanar is Perm-invariant, so it descends to the quotient.

def Minimalist.selCheckN : RoseTree.Nonplanar SOLabel → SelectionState

Selection check on the nonplanar carrier.

Equations

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

@[simp]

theorem Minimalist.selCheckN_mk (p : RoseTree SOLabel) : selCheckN (RoseTree.Nonplanar.mk p) = selCheckPlanar p

theorem Minimalist.selCheckN_node (a b : RoseTree.Nonplanar SOLabel) : selCheckN (RoseTree.Nonplanar.node (Sum.inr ()) {a, b}) = selCheckN a * selCheckN b

The selection-driven head on SyntacticObject

def Minimalist.SyntacticObject.selCheck (s : SyntacticObject) : SelectionState

Selection-driven head check: the selection instance of [MCB25]'s head functions; computable.

Equations

• s.selCheck = Minimalist.selCheckN ↑s

def Minimalist.SyntacticObject.selHead (s : SyntacticObject) : Option LIToken

The projecting head's lexical item, by c-selection.

Equations

• s.selHead = s.selCheck.head

def Minimalist.SyntacticObject.checkedSel (s : SyntacticObject) : Option (List Cat)

Residual pending selectional features (some [] = saturated).

Equations

• s.checkedSel = s.selCheck.residual

def Minimalist.SyntacticObject.outerCatC (s : SyntacticObject) : Option Cat

The projecting head's outer category (the phase-head selector); none at exocentric nodes.

Equations

• s.outerCatC = Option.map (fun (x : Minimalist.LIToken) => x.item.outerCat) s.selHead

@[simp]

theorem Minimalist.SyntacticObject.selCheck_lexLeaf (tok : LIToken) : (lexLeaf tok).selCheck = SelectionState.of tok tok.item.outerSel

@[simp]

theorem Minimalist.SyntacticObject.selCheck_traceLeaf : traceLeaf.selCheck = SelectionState.of (mkTraceToken 0) []

@[simp]

theorem Minimalist.SyntacticObject.selCheck_node (l r : SyntacticObject) : (l.node r).selCheck = l.selCheck * r.selCheck

noncomputable def Minimalist.SyntacticObject.selCheckHom : SyntacticObject →ₙ* SelectionState

selCheck as a morphism of magmas ([MCB25] §1.13's algebraic frame): the lift of the leaf data.

Equations

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

@[simp]

theorem Minimalist.SyntacticObject.selCheckHom_apply (s : SyntacticObject) : selCheckHom s = s.selCheck

@[simp]

theorem Minimalist.SyntacticObject.selHead_lexLeaf (tok : LIToken) : (lexLeaf tok).selHead = some tok

theorem Minimalist.SyntacticObject.selHead_node {l r : SyntacticObject} {h : LIToken} (hlr : (l.node r).selHead = some h) : l.selHead = some h ∨ r.selHead = some h

Endocentricity: a node's projecting head is one of its daughters' heads — bare-phrase-structure projection ([Cho95a] §4, abstracted as [MCB25] Definition 1.13.6 / Lemma 1.13.7).

@[simp]

theorem Minimalist.SyntacticObject.outerCatC_lexLeaf (tok : LIToken) : (lexLeaf tok).outerCatC = some tok.item.outerCat