Clause Spine: Fine-Grained Clause Size

[ETB26] [Gri05b] [Wur14]

ComplementSize (ExtendedProjection/Basic.lean) classifies clausal complements by their highest functional head, which works well for tense-Agree transparency and CTP classification. But it can't distinguish VoiceP from ApplP, since both have fValue = 1. Languages like Mam need this distinction: =(y)a' appears when Voice⁰ is projected but not when only Appl⁰ is.

ClauseSpine records the full list of projected heads, enabling per-head projection queries.

structure Minimalist.ClauseSpine : Type

A clause spine: the ordered sequence of functional heads projected in a clause, from lowest (V) to highest (e.g., C). Unlike ComplementSize, which records only the highest head, ClauseSpine records every projected head, enabling per-head queries.

Example: a transitive clause with Voice projects [V, Appl, v, Voice], while an infinitival without Voice projects [V, Appl].

• projectedHeads : List Cat

  Projected heads, ordered bottom-up (V first, highest last). Non-empty: every clause projects at least a lexical head.

• nonempty : self.projectedHeads ≠ []

  The spine is non-empty

def Minimalist.instReprClauseSpine.repr : ClauseSpine → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Minimalist.instReprClauseSpine : Repr ClauseSpine

Equations

• Minimalist.instReprClauseSpine = { reprPrec := Minimalist.instReprClauseSpine.repr }

def Minimalist.ClauseSpine.projects (spine : ClauseSpine) (c : Cat) : Bool

Does this spine project a given functional head?

Equations

• spine.projects c = spine.projectedHeads.any fun (x : Minimalist.Cat) => x == c

def Minimalist.ClauseSpine.highestHead (spine : ClauseSpine) : Cat

The highest head in the spine (always exists by nonempty invariant).

Equations

• spine.highestHead = match spine.projectedHeads.getLast? with | some c => c | none => Minimalist.Cat.V

def Minimalist.ClauseSpine.lowestHead (spine : ClauseSpine) : Cat

The lowest (lexical) head in the spine.

Equations

• spine.lowestHead = match spine.projectedHeads.head? with | some c => c | none => Minimalist.Cat.V

def Minimalist.ClauseSpine.size (spine : ClauseSpine) : ℕ

Number of projected heads.

Equations

• spine.size = spine.projectedHeads.length

def Minimalist.ClauseSpine.extend (spine : ClauseSpine) (heads : List Cat) : ClauseSpine

Extend a spine upward with further projected heads — e.g. the nominal or adpositional superstructure over an embedded CP ([Dea26]'s shelled notional complements).

Equations

• spine.extend heads = { projectedHeads := spine.projectedHeads ++ heads, nonempty := ⋯ }

def Minimalist.ClauseSpine.above (spine : ClauseSpine) (c : Cat) : List Cat

The heads projected strictly above the last occurrence of c: above .C is the CP-external superstructure ([] for a bare CP).

Equations

• spine.above c = (List.takeWhile (fun (x : Minimalist.Cat) => x != c) spine.projectedHeads.reverse).reverse

def Minimalist.ClauseSpine.applP : ClauseSpine

ApplP-sized clause: [V, Appl]. Infinitival complement without Voice. In Mam, this is the size of infinitival complements where =(y)a' is impossible — Voice is not projected, so there is no host for [oblique].

Equations

• Minimalist.ClauseSpine.applP = { projectedHeads := [Minimalist.Cat.V, Minimalist.Cat.Appl], nonempty := Minimalist.ClauseSpine.applP._proof_1 }

def Minimalist.ClauseSpine.bareVP : ClauseSpine

Bare VP: [V]. Minimal clause — just the lexical verb. In Mam, this is the size of infinitival complements: the embedded clause is just VP, lacking Voice, Appl, v.

Equations

• Minimalist.ClauseSpine.bareVP = { projectedHeads := [Minimalist.Cat.V], nonempty := Minimalist.ClauseSpine.bareVP._proof_1 }

def Minimalist.ClauseSpine.vP : ClauseSpine

vP-sized clause: [V, v]. Light verb shell without Voice or Appl.

Equations

• Minimalist.ClauseSpine.vP = { projectedHeads := [Minimalist.Cat.V, Minimalist.Cat.v], nonempty := Minimalist.ClauseSpine.vP._proof_1 }

def Minimalist.ClauseSpine.voiceP : ClauseSpine

VoiceP-sized clause: [V, Appl, v, Voice]. Projects Voice head. In Mam, this is the size of "aspectless" complements — Voice is projected, so [oblique] can be hosted, and =(y)a' is obligatory on oblique extraction.

Equations

• Minimalist.ClauseSpine.voiceP = { projectedHeads := [Minimalist.Cat.V, Minimalist.Cat.Appl, Minimalist.Cat.v, Minimalist.Cat.Voice], nonempty := Minimalist.ClauseSpine.voiceP._proof_1 }

def Minimalist.ClauseSpine.tP : ClauseSpine

TP-sized clause: [V, Appl, v, Voice, T]. Full inflectional domain.

Equations

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

def Minimalist.ClauseSpine.cP : ClauseSpine

CP-sized clause: [V, Appl, v, Voice, T, C]. Full finite clause.

Equations

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

def Minimalist.ClauseSpine.nmlzP : ClauseSpine

NmlzP-sized clause: [V, Appl, v, Voice, T, Nmlz]. Hindi nominalized clause. [Kei20] ch. 2: NmlzP is a distinct clause type from CP — their transparency profiles are incomparable (NmlzP blocks Ā but not wh; CP blocks wh but not Ā in Hindi).

Equations

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

def Minimalist.ClauseSpine.forceP : ClauseSpine

ForceP-sized clause: [V, Appl, v, Voice, T, C, Force]. German V2 clause. [Kei20] ch. 4: V2 clauses in German are structurally larger than V-final (CP) clauses — they project ForceP above CP.

Equations

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

def Minimalist.ClauseSpine.fLevel (spine : ClauseSpine) : ℕ

The F-level of a clause spine: the fValue of its highest projected head. This bridges ClauseSpine (concrete head list) to ExtendedProjection's F-value hierarchy, enabling [Kei19]'s transparency calculations.

Example: ClauseSpine.cP.fLevel = 6 (C is F6), ClauseSpine.tP.fLevel = 2 (T is F2).

Equations

• spine.fLevel = Minimalist.fValue spine.highestHead