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.cat?: the head token and its category, the head function of the phases (SyntacticObject.IsPhaseHead).
• 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.
• Head SelectionState: the head of a selection product is a factor's head, so selHead is endocentric (Minimalist.mem_head_or_mem_head_of_mem_head_map_mul).
• Minimalist.SelectionState.isSaturated_iff_not_isSaturated_of_mul_ne_zero, Minimalist.SelectionState.head_mul_of_not_isSaturated: Merge is triggered, one factor selecting and the other saturated, and the selecting factor projects.

Implementation notes

SelectionState is a one-field structure over Option (LexicalItem.Token × List Cat), so that the selection product can be an instance on it: the Option is implementation, and 0 is the public spelling of the exocentric failure, the off-domain value of a partial head function. There is no One, since two saturated states multiply to 0, and no associativity claim, so the structure is CommMagma + MulZeroClass only. The trace of a token is a lower copy of the phrase it heads, so it gets that phrase's value, saturated with the token's category (traceState), and a head that selected the moved phrase still selects its trace; the bare trace remembers no token and gets the saturated dummy .of .bareTrace []. selCheck reads only the token's category and sel. Two saturated sisters have no head, as in [MCB25]'s partial head functions: a specifier and its sister are labeled, if at all, by the labeling algorithm (SyntacticObject/Label.lean).

References

• [Adg03]
• [Cho95a]
• [MCB25]
• [CS16b]

The selection state

structure Minimalist.SelectionState : Type

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

• toOption : Option (LexicalItem.Token × 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 : LexicalItem.Token) (stack : List Cat) : SelectionState

A defined selection state has projecting head tok and 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 LexicalItem.Token

The projecting head token; none off the endocentric domain.

Equations

• x.head = Option.map (fun (x : Minimalist.LexicalItem.Token × 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.LexicalItem.Token × List Minimalist.Cat) => x.2) x.toOption

@[simp]

theorem Minimalist.SelectionState.head_of (tok : LexicalItem.Token) (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 × LexicalItem.Token × 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.cat = c then some (true, ha, rest) else none
• Minimalist.selCombine { toOption := some (ha, []) } { toOption := some (hb, c :: rest) } = if ha.item.cat = c then some (false, hb, rest) else none
• Minimalist.selCombine x✝¹ x✝ = none

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

The projecting daughter is reported as some true for the left and some false for the right.

Equations

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

theorem Minimalist.selCombine_comm (x y : SelectionState) : selCombine x y = Option.map (fun (p : Bool × LexicalItem.Token × 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 is 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 × LexicalItem.Token × List Cat) => x.2) (selCombine x y) }

* unfolds to the canonical accessor for the selection product.

@[instance_reducible]

instance Minimalist.instCommMagmaSelectionState : CommMagma SelectionState

Equations

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

@[simp]

theorem Minimalist.SelectionState.mul_self (x : SelectionState) : x * x = 0

A state never combines with itself, since of two equal sisters neither selects the other.

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

The projected head is the head of the sister on the reported side.

@[instance_reducible]

instance Minimalist.instHeadSelectionState : Head SelectionState

The head of a selection product is one of its factors' heads.

Equations

• Minimalist.instHeadSelectionState = { head := Minimalist.SelectionState.head, head_zero := Minimalist.instHeadSelectionState._proof_1, mem_head_or_mem_head_of_mem_head_mul := ⋯ }

theorem Minimalist.SelectionState.head_of_mul_of {a r : LexicalItem.Token} {y : SelectionState} (h : (of a [] * y).head = some r) : y.head = some r

A saturated state never projects, so the head of its product is the other factor's head.

Triggered Merge

def Minimalist.SelectionState.IsSaturated (x : SelectionState) : Prop

A selection state is saturated when its head selects nothing further.

Equations

• x.IsSaturated = (x.residual = some [])

@[instance_reducible]

instance Minimalist.instDecidablePredSelectionStateIsSaturated : DecidablePred SelectionState.IsSaturated

Equations

• Minimalist.instDecidablePredSelectionStateIsSaturated x = Minimalist.instDecidablePredSelectionStateIsSaturated._aux_1 x

theorem Minimalist.SelectionState.isSaturated_iff_not_isSaturated_of_mul_ne_zero {x y : SelectionState} (h : x * y ≠ 0) : x.IsSaturated ↔ ¬y.IsSaturated

[CS16b]'s triggered Merge (Definition 27): of the factors of a defined selection product exactly one is saturated, the other still selecting.

theorem Minimalist.SelectionState.head_mul_of_not_isSaturated {x y : SelectionState} (h : x * y ≠ 0) (hx : ¬x.IsSaturated) : (x * y).head = x.head

[CS16b], Theorem 13: the factor whose selection Merge checks projects.

Selection check on the carriers

def Minimalist.traceState : Option LexicalItem.Token → SelectionState

The selection state of a trace is a saturated copy of the phrase its token heads, and for the bare trace the saturated dummy.

Equations

• Minimalist.traceState (some tok) = Minimalist.SelectionState.of tok []
• Minimalist.traceState none = Minimalist.SelectionState.of Minimalist.LexicalItem.Token.bareTrace []

def Minimalist.selNode : SyntacticObject.Vertex → List SelectionState → SelectionState

The selection algebra is the SyntacticObject.mergeAlgebra of token + sel leaves and the traces' traceState.

Equations

• Minimalist.selNode = Minimalist.SyntacticObject.mergeAlgebra (fun (tok : Minimalist.LexicalItem.Token) => Minimalist.SelectionState.of tok tok.item.sel) Minimalist.traceState

theorem Minimalist.selNode_perm (a : SyntacticObject.Vertex) {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 SyntacticObject.Vertex → SelectionState

The selection check on a planar tree is the catamorphism of selNode.

Equations

• Minimalist.selCheckPlanar = RoseTree.fold Minimalist.selNode

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

At a node, selCheckPlanar folds the algebra over the daughters.

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

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

def Minimalist.selCheckN : UnorderedTree SyntacticObject.Vertex → SelectionState

Selection check on the nonplanar carrier.

Equations

• Minimalist.selCheckN = Minimalist.SyntacticObject.liftN (fun (tok : Minimalist.LexicalItem.Token) => Minimalist.SelectionState.of tok tok.item.sel) Minimalist.traceState

@[simp]

theorem Minimalist.selCheckN_mk (p : RoseTree SyntacticObject.Vertex) : selCheckN (UnorderedTree.mk p) = selCheckPlanar p

theorem Minimalist.selCheckN_node (a b : UnorderedTree SyntacticObject.Vertex) : selCheckN (UnorderedTree.node SyntacticObject.Vertex.bare {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 LexicalItem.Token

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.cat? (s : SyntacticObject) : Option Cat

The category of the projecting head, none at exocentric nodes.

Equations

• s.cat? = Option.map (fun (x : Minimalist.LexicalItem.Token) => x.item.cat) s.selHead

@[simp]

theorem Minimalist.SyntacticObject.selCheck_leaf (tok : LexicalItem.Token) : (↑tok).selCheck = SelectionState.of tok tok.item.sel

@[simp]

theorem Minimalist.SyntacticObject.selCheck_trace : trace.selCheck = SelectionState.of LexicalItem.Token.bareTrace []

@[simp]

theorem Minimalist.SyntacticObject.selCheck_traceOf (tok : LexicalItem.Token) : (traceOf tok).selCheck = SelectionState.of tok []

@[simp]

theorem Minimalist.SyntacticObject.selCheck_node (l r : SyntacticObject) : (l.merge 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

• Minimalist.SyntacticObject.selCheckHom = Minimalist.SyntacticObject.lift (fun (tok : Minimalist.LexicalItem.Token) => Minimalist.SelectionState.of tok tok.item.sel) Minimalist.traceState

@[simp]

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

@[simp]

theorem Minimalist.SyntacticObject.selHead_leaf (tok : LexicalItem.Token) : (↑tok).selHead = some tok

@[simp]

theorem Minimalist.SyntacticObject.selHead_merge_self (x : SyntacticObject) : (x.merge x).selHead = none

An object merged with itself has no head.

@[simp]

theorem Minimalist.SyntacticObject.cat?_leaf (tok : LexicalItem.Token) : (↑tok).cat? = some tok.item.cat