The labeling algorithm

The labeling algorithm of [Cho13] is minimal search for the head that tells the interfaces what kind of object a constituent is. A head merged with a phrase labels the result. Two phrases do not: minimal search finds two heads, and the object is labeled only if one of the phrases raises, its lower copy being invisible to the search, or if the two heads share an agreed feature. [MCB25] (Definition 1.15.2) state the algorithm over a partial head function: label by the head where it is defined, and where a term has raised, by the head of the object with the lower copy deleted. Here the head function is the selection head selHead and a lower copy is the trace of a token: it still satisfies the selection of whatever selected the phrase it copies (traceState), and is otherwise invisible. So the labeling state of a constituent is its selection state, or a lower copy (LabelState), and the label extends the selection head (label_eq_of_selHead): a lower copy beside a saturated phrase leaves the phrase to label their sum (label_merge_traceOf), and two saturated phrases leave it unlabeled (label_merge_eq_none), the configuration [Cho13] takes to force successive-cyclic movement.

[MCB25] also require the head function to be raising (Definition 1.15.1): the object Internal Merge forms is headed by the head of what it raised out of, so the landing site of a wh-phrase in the specifier of a C is headed by C. The raising head raisingHead reads this off the finished object: where two phrases merge and the head of one has a lower copy inside the other, the first has raised out of the second, which projects. It extends the label (raisingHead_eq_of_label).

Implementation notes

• The selection head and the label are not raising: they leave a landing site, two saturated phrases, without a head, as [Cho13]'s (21) requires of an intermediate landing site.
• The raising head reads Definition 1.15.1 on the finished object, a lower copy recording the token that heads the phrase it copies; the phases of SyntacticObject/Phase.lean are delimited by it.

Main definitions

• Minimalist.LabelState: a selection state or a lower copy, a commutative magma with zero.
• Minimalist.SyntacticObject.labelCheck, Minimalist.SyntacticObject.label: the labeling state and the label of a syntactic object.
• Minimalist.RaisingState, Minimalist.SyntacticObject.raisingHead: the raising state and the raising head of a syntactic object.

TODO

The labeling of two phrases by a feature their heads share, the interrogative feature of an indirect question or the φ-features of subject and predicate, which [Cho13] requires to be agreed rather than merely matched, needs Agree and is not formalized. The trace of a token is the lower copy of the phrase the token heads; a moved head, whose lower copy would still select, is not distinguished.

References

• [Cho13]
• [MCB25]

inductive Minimalist.LabelState : Type

A constituent's labeling state is its selection state, or a lower copy of the phrase a token heads, which satisfies selection as that phrase and is otherwise invisible to the labeling algorithm.

• sel (x : SelectionState) : LabelState

  The selection state of a constituent the labeling algorithm sees.

• copy (tok : LexicalItem.Token) : LabelState

  A lower copy of the phrase tok heads.

@[instance_reducible]

instance Minimalist.instDecidableEqLabelState : DecidableEq LabelState

Equations

• Minimalist.instDecidableEqLabelState = Minimalist.instDecidableEqLabelState.decEq

def Minimalist.instDecidableEqLabelState.decEq (x✝ x✝¹ : LabelState) : Decidable (x✝ = x✝¹)

Equations

• Minimalist.instDecidableEqLabelState.decEq (Minimalist.LabelState.sel a) (Minimalist.LabelState.sel b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Minimalist.instDecidableEqLabelState.decEq (Minimalist.LabelState.sel x_2) (Minimalist.LabelState.copy tok) = isFalse ⋯
• Minimalist.instDecidableEqLabelState.decEq (Minimalist.LabelState.copy tok) (Minimalist.LabelState.sel x_2) = isFalse ⋯
• Minimalist.instDecidableEqLabelState.decEq (Minimalist.LabelState.copy a) (Minimalist.LabelState.copy b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Minimalist.LabelState.instZero : Zero LabelState

Equations

• Minimalist.LabelState.instZero = { zero := Minimalist.LabelState.sel 0 }

@[instance_reducible]

instance Minimalist.LabelState.instMul : Mul LabelState

A lower copy satisfies the selection of a sister selecting the phrase it copies and is otherwise invisible; two lower copies leave nothing to see.

Equations

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

@[simp]

theorem Minimalist.LabelState.sel_mul_sel (x y : SelectionState) : sel x * sel y = sel (x * y)

theorem Minimalist.LabelState.copy_mul_sel (a : LexicalItem.Token) (y : SelectionState) : copy a * sel y = if SelectionState.of a [] * y = 0 then sel y else sel (SelectionState.of a [] * y)

theorem Minimalist.LabelState.sel_mul_copy (x : SelectionState) (a : LexicalItem.Token) : sel x * copy a = if x * SelectionState.of a [] = 0 then sel x else sel (x * SelectionState.of a [])

@[instance_reducible]

instance Minimalist.LabelState.instCommMagma : CommMagma LabelState

Equations

• Minimalist.LabelState.instCommMagma = { toMul := Minimalist.LabelState.instMul, mul_comm := Minimalist.LabelState.instCommMagma._proof_1 }

@[instance_reducible]

instance Minimalist.LabelState.instMulZeroClass : MulZeroClass LabelState

Equations

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

def Minimalist.LabelState.label : LabelState → Option LexicalItem.Token

The label a labeling state provides is the head of a visible constituent, and none for a lower copy.

Equations

• (Minimalist.LabelState.sel x_1).label = x_1.head
• (Minimalist.LabelState.copy tok).label = none

@[simp]

theorem Minimalist.LabelState.mul_self (l : LabelState) : l * l = 0

A labeling state never combines with itself.

@[instance_reducible]

instance Minimalist.LabelState.instHead : Head LabelState

The label of a labeling product is a factor's label.

Equations

• Minimalist.LabelState.instHead = { head := Minimalist.LabelState.label, head_zero := Minimalist.LabelState.instHead._proof_2, mem_head_or_mem_head_of_mem_head_mul := ⋯ }

def Minimalist.labelTraceState : Option LexicalItem.Token → LabelState

A trace's labeling state is the lower copy of the phrase its token heads; the bare trace, which remembers no token and belongs to no chain, keeps its selection state.

Equations

• Minimalist.labelTraceState (some tok) = Minimalist.LabelState.copy tok
• Minimalist.labelTraceState none = Minimalist.LabelState.sel (Minimalist.traceState none)

def Minimalist.SyntacticObject.labelCheck (s : SyntacticObject) : LabelState

The labeling state of a syntactic object.

Equations

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

def Minimalist.SyntacticObject.label (s : SyntacticObject) : Option LexicalItem.Token

The label of a syntactic object, none where the labeling algorithm finds none.

Equations

• s.label = s.labelCheck.label

@[simp]

theorem Minimalist.SyntacticObject.labelCheck_leaf (tok : LexicalItem.Token) : (↑tok).labelCheck = LabelState.sel (SelectionState.of tok tok.item.sel)

@[simp]

theorem Minimalist.SyntacticObject.labelCheck_traceOf (tok : LexicalItem.Token) : (traceOf tok).labelCheck = LabelState.copy tok

@[simp]

theorem Minimalist.SyntacticObject.labelCheck_trace : trace.labelCheck = LabelState.sel (traceState none)

@[simp]

theorem Minimalist.SyntacticObject.labelCheck_merge (l r : SyntacticObject) : (l.merge r).labelCheck = l.labelCheck * r.labelCheck

theorem Minimalist.SyntacticObject.labelCheck_eq_sel_or (s : SyntacticObject) (h : s.selCheck ≠ 0) : s.labelCheck = LabelState.sel s.selCheck ∨ ∃ (tok : LexicalItem.Token), s = traceOf tok

Where the selection head is defined, the labeling algorithm sees the selection state, unless the object is itself a lower copy.

theorem Minimalist.SyntacticObject.label_eq_of_selHead (s : SyntacticObject) {h : LexicalItem.Token} (hs : s.selHead = some h) (hc : ∀ (tok : LexicalItem.Token), s ≠ traceOf tok) : s.label = some h

The label extends the selection head: where [MCB25]'s head function is defined, it labels.

theorem Minimalist.SyntacticObject.label_merge_traceOf (a : LexicalItem.Token) {r : SyntacticObject} {h : LexicalItem.Token} (hr : r.labelCheck = LabelState.sel (SelectionState.of h [])) : ((traceOf a).merge r).label = some h

A lower copy beside a saturated phrase is invisible, so the phrase labels their sum.

theorem Minimalist.SyntacticObject.label_merge_eq_none {l r : SyntacticObject} {a b : LexicalItem.Token} (hl : l.labelCheck = LabelState.sel (SelectionState.of a [])) (hr : r.labelCheck = LabelState.sel (SelectionState.of b [])) : (l.merge r).label = none

Two saturated phrases leave their sum unlabeled.

The raising head

structure Minimalist.RaisingState : Type

The raising state of a constituent pairs its labeling state with the tokens whose lower copies it contains.

• label : LabelState

  The labeling state.

• copies : Multiset LexicalItem.Token

  The tokens heading the phrases of which the constituent contains a lower copy.

@[instance_reducible]

instance Minimalist.instDecidableEqRaisingState : DecidableEq RaisingState

Equations

• Minimalist.instDecidableEqRaisingState = Minimalist.instDecidableEqRaisingState.decEq

def Minimalist.instDecidableEqRaisingState.decEq (x✝ x✝¹ : RaisingState) : Decidable (x✝ = x✝¹)

Equations

• Minimalist.instDecidableEqRaisingState.decEq { label := a, copies := a_1 } { label := b, copies := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance Minimalist.RaisingState.instZero : Zero RaisingState

Equations

• Minimalist.RaisingState.instZero = { zero := { label := 0, copies := 0 } }

def Minimalist.RaisingState.raise (x y : RaisingState) : LabelState

Under raising, two merged constituents take the labeling product where it is defined, and otherwise the labeling state of the one containing a lower copy of the other's head, since the other raised out of it and it projects.

Equations

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

@[instance_reducible]

instance Minimalist.RaisingState.instMul : Mul RaisingState

Equations

• Minimalist.RaisingState.instMul = { mul := fun (x y : Minimalist.RaisingState) => { label := x.raise y, copies := x.copies + y.copies } }

theorem Minimalist.RaisingState.mul_def (x y : RaisingState) : x * y = { label := x.raise y, copies := x.copies + y.copies }

theorem Minimalist.RaisingState.raise_comm (x y : RaisingState) : x.raise y = y.raise x

@[instance_reducible]

instance Minimalist.RaisingState.instCommMagma : CommMagma RaisingState

Equations

• Minimalist.RaisingState.instCommMagma = { toMul := Minimalist.RaisingState.instMul, mul_comm := ⋯ }

@[instance_reducible]

instance Minimalist.RaisingState.instHead : Head RaisingState

The raising head of a product is a factor's raising head.

Equations

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

def Minimalist.raisingTraceState : Option LexicalItem.Token → RaisingState

A trace's raising state is the lower copy of the phrase its token heads, with the token recorded among the copies; the bare trace remembers no token.

Equations

• Minimalist.raisingTraceState (some tok) = { label := Minimalist.LabelState.copy tok, copies := {tok} }
• Minimalist.raisingTraceState none = { label := Minimalist.LabelState.sel (Minimalist.traceState none), copies := 0 }

def Minimalist.SyntacticObject.raisingCheck (s : SyntacticObject) : RaisingState

The raising state of a syntactic object.

Equations

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

def Minimalist.SyntacticObject.raisingHead (s : SyntacticObject) : Option LexicalItem.Token

The raising head of a syntactic object, [MCB25]'s raising head function: the label where there is one, and at a landing site the head of the phrase moved out of.

Equations

• s.raisingHead = s.raisingCheck.label.label

@[simp]

theorem Minimalist.SyntacticObject.raisingCheck_merge (l r : SyntacticObject) : (l.merge r).raisingCheck = l.raisingCheck * r.raisingCheck

theorem Minimalist.SyntacticObject.raisingCheck_label_eq_or (s : SyntacticObject) : s.raisingCheck.label = s.labelCheck ∨ s.labelCheck = 0

The raising state refines the labeling state.

theorem Minimalist.SyntacticObject.raisingHead_eq_of_label (s : SyntacticObject) {a : LexicalItem.Token} (hs : s.label = some a) : s.raisingHead = some a

The raising head extends the label.

noncomputable def Minimalist.SyntacticObject.raisingCheckHom : SyntacticObject →ₙ* RaisingState

raisingCheck as a morphism of magmas.

Equations

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

theorem Minimalist.SyntacticObject.raisingHead_merge {l r : SyntacticObject} {h : LexicalItem.Token} (hlr : (l.merge r).raisingHead = some h) : l.raisingHead = some h ∨ r.raisingHead = some h

The raising head of a merge is a daughter's raising head ([MCB25] Lemma 1.13.7).

@[simp]

theorem Minimalist.SyntacticObject.raisingHead_merge_self (x : SyntacticObject) : (x.merge x).raisingHead = none

An object merged with itself has no raising head.