Complement frames — typed slots

A verb's complement frame as a list of typed Slots, factoring the flat ComplementType enum cells into their axes: syntactic category, case marking, CP-external shell ([Dea26]), clause form, [Noo07] coding, and embedded-subject requirement (genitive subjects of nominalized clauses, [Bon22]). The legacy enum survives as a round-trip view (ComplementType.toFrame / Frame.toComplementType).

Main declarations

• Slot.Shell, Slot.ShellInventory (+ isAttested, hasNominalShell, the named cells) — CP-external wrapping shells ([Dea26] Table 79)
• Slot, Slot.WellFormed — one complement position: category plus optional clausal axes
• Frame + Frame.np, Frame.finiteClause, … — a frame is a list of slots; the legacy enum cells as smart constructors

Implementation notes

Frame-conditioned readings (attitude, opacity, control) are not slot data — they live on Verb.Reading (Semantics/Verb/Defs.lean), keyed to the verb's frames. The [Noo07] selection relation between verb frames and clause-typers (Verb.realizes) lives in Syntax/Clause/Complementation.lean. This file never imports Semantics/.

CP-external wrapping shells

ComplementSize and ClauseSpine (Syntax/Minimalist/) record internal clause height; Slot.Shell records what wraps the CP externally. [Dea26] Table 79 cross-classifies the two axes.

inductive Slot.Shell : Type

A wrapping head above a CP: [Dea26] Table 79 attests D, N, and P; c is the base case, so the bare-CP inventory is [.c].

• c : Shell

  The CP itself (always present).

• d : Shell

  D shell.

• n : Shell

  N shell (between D and CP).

• p : Shell

  P shell.

@[implicit_reducible]

instance Slot.instDecidableEqShell : DecidableEq Shell

Equations

• Slot.instDecidableEqShell x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Slot.instReprShell : Repr Shell

Equations

• Slot.instReprShell = { reprPrec := Slot.instReprShell.repr }

def Slot.instReprShell.repr : Shell → ℕ → Std.Format

Equations

• Slot.instReprShell.repr Slot.Shell.c prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Slot.Shell.c")).group prec✝
• Slot.instReprShell.repr Slot.Shell.d prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Slot.Shell.d")).group prec✝
• Slot.instReprShell.repr Slot.Shell.n prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Slot.Shell.n")).group prec✝
• Slot.instReprShell.repr Slot.Shell.p prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Slot.Shell.p")).group prec✝

@[reducible, inline]

abbrev Slot.ShellInventory : Type

An ordered shell list, innermost first: [.c, .d] = D wraps CP, [.c, .n, .d] = D wraps N wraps CP.

Equations

• Slot.ShellInventory = List Slot.Shell

def Slot.ShellInventory.isAttested : ShellInventory → Bool

The shell inventory is a [Dea26] Table 79 cell.

Equations

• Slot.ShellInventory.isAttested [Slot.Shell.c] = true
• Slot.ShellInventory.isAttested [Slot.Shell.c, Slot.Shell.d] = true
• Slot.ShellInventory.isAttested [Slot.Shell.c, Slot.Shell.n, Slot.Shell.d] = true
• Slot.ShellInventory.isAttested [Slot.Shell.c, Slot.Shell.d, Slot.Shell.p] = true
• x✝.isAttested = false

def Slot.ShellInventory.bareCP : ShellInventory

The bare-CP cell (Nez Perce; English think).

Equations

• Slot.ShellInventory.bareCP = [Slot.Shell.c]

def Slot.ShellInventory.dCP : ShellInventory

The V D CP cell (Washo, [BH21]).

Equations

• Slot.ShellInventory.dCP = [Slot.Shell.c, Slot.Shell.d]

def Slot.ShellInventory.dnCP : ShellInventory

The V D N CP cell (Adyghe, [CP11a]).

Equations

• Slot.ShellInventory.dnCP = [Slot.Shell.c, Slot.Shell.n, Slot.Shell.d]

def Slot.ShellInventory.pdCP : ShellInventory

The V P D CP cell (Bulgarian, [Kra10]; Ndebele, [Pie19]).

Equations

• Slot.ShellInventory.pdCP = [Slot.Shell.c, Slot.Shell.d, Slot.Shell.p]

theorem Slot.ShellInventory.named_shells_attested : bareCP.isAttested = true ∧ dCP.isAttested = true ∧ dnCP.isAttested = true ∧ pdCP.isAttested = true

The four named witnesses are all attested.

theorem Slot.ShellInventory.pdCP_contains_p_and_d : Shell.p ∈ pdCP ∧ Shell.d ∈ pdCP

P-shelling co-occurs with D-shelling.

theorem Slot.ShellInventory.dnCP_contains_n_and_d : Shell.n ∈ dnCP ∧ Shell.d ∈ dnCP

N appears only inside a D shell.

theorem Slot.ShellInventory.named_shells_contain_c : Shell.c ∈ bareCP ∧ Shell.c ∈ dCP ∧ Shell.c ∈ dnCP ∧ Shell.c ∈ pdCP

Every named shell contains C.

theorem Slot.ShellInventory.pCP_not_attested : isAttested [Shell.c, Shell.p] = false

V P CP (P with no D shell) is not a Table 79 cell.

theorem Slot.ShellInventory.nCP_not_attested : isAttested [Shell.c, Shell.n] = false

V N CP (N with no D shell) is not a Table 79 cell.

def Slot.ShellInventory.hasNominalShell (inv : ShellInventory) : Prop

The clause complex is wrapped in a nominal projection: its shell contains D (Washo dCP, Adyghe dnCP, Bulgarian/Ndebele pdCP; bareCP is not). On [Dea26]'s attested cells this coincides with ≠ bareCP (pCP/nCP are unattested); D-membership is the definitional content, not the complement of a special case.

Equations

• inv.hasNominalShell = (Slot.Shell.d ∈ inv)

@[implicit_reducible]

instance Slot.ShellInventory.instDecidablePredHasNominalShell : DecidablePred hasNominalShell

Equations

• inv.instDecidablePredHasNominalShell = Slot.ShellInventory.instDecidablePredHasNominalShell._aux_1 inv

Complement-frame axes

inductive Slot.Cat : Type

Syntactic category of a complement slot.

• nominal : Cat
• adpositional : Cat
• clausal : Cat

@[implicit_reducible]

instance Slot.instDecidableEqCat : DecidableEq Cat

Equations

• Slot.instDecidableEqCat x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Slot.instReprCat.repr : Cat → ℕ → Std.Format

Equations

• Slot.instReprCat.repr Slot.Cat.nominal prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Slot.Cat.nominal")).group prec✝
• Slot.instReprCat.repr Slot.Cat.adpositional prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Slot.Cat.adpositional")).group prec✝
• Slot.instReprCat.repr Slot.Cat.clausal prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Slot.Cat.clausal")).group prec✝

@[implicit_reducible]

instance Slot.instReprCat : Repr Cat

Equations

• Slot.instReprCat = { reprPrec := Slot.instReprCat.repr }

inductive Slot.EmbeddedSubject : Type

Embedded-subject requirement of a clausal slot: obligatorily null (control/raising infinitives) or overt, optionally with a fixed case (genitive subjects of nominalized clauses, [Bon22]).

• obligatorilyNull : EmbeddedSubject
• overt (subjCase : Option Case) : EmbeddedSubject

@[implicit_reducible]

instance Slot.instDecidableEqEmbeddedSubject : DecidableEq EmbeddedSubject

Equations

• Slot.instDecidableEqEmbeddedSubject = Slot.instDecidableEqEmbeddedSubject.decEq

def Slot.instDecidableEqEmbeddedSubject.decEq (x✝ x✝¹ : EmbeddedSubject) : Decidable (x✝ = x✝¹)

Equations

• Slot.instDecidableEqEmbeddedSubject.decEq Slot.EmbeddedSubject.obligatorilyNull Slot.EmbeddedSubject.obligatorilyNull = isTrue ⋯
• Slot.instDecidableEqEmbeddedSubject.decEq Slot.EmbeddedSubject.obligatorilyNull (Slot.EmbeddedSubject.overt subjCase) = isFalse ⋯
• Slot.instDecidableEqEmbeddedSubject.decEq (Slot.EmbeddedSubject.overt subjCase) Slot.EmbeddedSubject.obligatorilyNull = isFalse ⋯
• Slot.instDecidableEqEmbeddedSubject.decEq (Slot.EmbeddedSubject.overt a) (Slot.EmbeddedSubject.overt b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Slot.instReprEmbeddedSubject : Repr EmbeddedSubject

Equations

• Slot.instReprEmbeddedSubject = { reprPrec := Slot.instReprEmbeddedSubject.repr }

def Slot.instReprEmbeddedSubject.repr : EmbeddedSubject → ℕ → Std.Format

Equations

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

The frame object

structure Slot : Type

One complement position of a verb's frame: its category plus, for clausal slots, the recorded clausal axes. On non-clausal slots the clausal axes are none (Slot.WellFormed); on clausal slots none means unrecorded. Frame-conditioned readings and control are not slot data — they live on Verb.Reading.

• cat : Cat
• marking : Option Case

  Case marking on the slot (case-marked nominalized clauses, NPs).

• shell : Option ShellInventory

  CP-external wrapping shell ([Dea26] Table 79).

• clauseForm : Option Features.ClauseForm

  Clause form (declarative vs embedded question).

• coding : Option NoonanCompType

  [Noo07] coding of the complement clause.

• embeddedSubject : Option EmbeddedSubject

  Embedded-subject requirement.

@[implicit_reducible]

instance instDecidableEqSlot : DecidableEq Slot

Equations

• instDecidableEqSlot = instDecidableEqSlot.decEq

def instDecidableEqSlot.decEq (x✝ x✝¹ : Slot) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance instReprSlot : Repr Slot

Equations

• instReprSlot = { reprPrec := instReprSlot.repr }

def instReprSlot.repr : Slot → ℕ → Std.Format

Equations

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

def Slot.WellFormed (s : Slot) : Prop

Clausal axes are reserved for clausal slots.

Equations

• s.WellFormed = (s.cat = Slot.Cat.clausal ∨ s.shell = none ∧ s.clauseForm = none ∧ s.coding = none ∧ s.embeddedSubject = none)

@[implicit_reducible]

instance instDecidablePredSlotWellFormed : DecidablePred Slot.WellFormed

Equations

• instDecidablePredSlotWellFormed s = id inferInstance

def Slot.isClausal (s : Slot) : Prop

The slot is clausal.

Equations

• s.isClausal = (s.cat = Slot.Cat.clausal)

@[reducible, inline]

abbrev Frame : Type

A complement frame: the verb's selected complement positions in order. Intransitive = []; double object = two slots.

Equations

• Frame = List Slot

def Frame.codings (fr : Frame) : List NoonanCompType

The [Noo07] codings recorded across the frame's slots.

Equations

• fr.codings = List.filterMap (fun (x : Slot) => x.coding) fr

def Frame.hasClauseForm (fr : Frame) (cf : Features.ClauseForm) : Prop

Some slot of the frame records clause form cf.

Equations

• fr.hasClauseForm cf = ∃ s ∈ fr, s.clauseForm = some cf

@[implicit_reducible]

instance Frame.instDecidableHasClauseForm (fr : Frame) (cf : Features.ClauseForm) : Decidable (fr.hasClauseForm cf)

Equations

• fr.instDecidableHasClauseForm cf = id inferInstance

def Frame.hasCoding (fr : Frame) (t : NoonanCompType) : Prop

Some slot of the frame records [Noo07] coding t.

Equations

• fr.hasCoding t = ∃ s ∈ fr, s.coding = some t

@[implicit_reducible]

instance Frame.instDecidableHasCoding (fr : Frame) (t : NoonanCompType) : Decidable (fr.hasCoding t)

Equations

• fr.instDecidableHasCoding t = id inferInstance

Smart constructors — the legacy ComplementType cells

def Frame.np : Frame

Transitive: one nominal slot.

Equations

• Frame.np = [{ cat := Slot.Cat.nominal }]

def Frame.np_np : Frame

Double object: two nominal slots.

Equations

• Frame.np_np = [{ cat := Slot.Cat.nominal }, { cat := Slot.Cat.nominal }]

def Frame.np_pp : Frame

NP + PP: a nominal plus an adpositional slot.

Equations

• Frame.np_pp = [{ cat := Slot.Cat.nominal }, { cat := Slot.Cat.adpositional }]

def Frame.finiteClause : Frame

Finite declarative clause.

Equations

• Frame.finiteClause = [{ cat := Slot.Cat.clausal, clauseForm := some Features.ClauseForm.declarative, coding := some NoonanCompType.indicative }]

def Frame.infinitival : Frame

Infinitival clause: obligatorily null embedded subject.

Equations

• Frame.infinitival = [{ cat := Slot.Cat.clausal, coding := some NoonanCompType.infinitive, embeddedSubject := some Slot.EmbeddedSubject.obligatorilyNull }]

def Frame.gerund : Frame

Gerund / nominalized clause.

Equations

• Frame.gerund = [{ cat := Slot.Cat.clausal, coding := some NoonanCompType.nominalized }]

def Frame.smallClause : Frame

Small clause (paratactic coding).

Equations

• Frame.smallClause = [{ cat := Slot.Cat.clausal, coding := some NoonanCompType.paratactic }]

def Frame.question : Frame

Embedded question.

Equations

• Frame.question = [{ cat := Slot.Cat.clausal, clauseForm := some Features.ClauseForm.embeddedQuestion }]

The legacy enum view

def ComplementType.toFrame : ComplementType → Frame

The Frame cell of a legacy ComplementType (.none ↦ []).

Equations

• ComplementType.none.toFrame = []
• ComplementType.np.toFrame = Frame.np
• ComplementType.np_np.toFrame = Frame.np_np
• ComplementType.np_pp.toFrame = Frame.np_pp
• ComplementType.finiteClause.toFrame = Frame.finiteClause
• ComplementType.infinitival.toFrame = Frame.infinitival
• ComplementType.gerund.toFrame = Frame.gerund
• ComplementType.smallClause.toFrame = Frame.smallClause
• ComplementType.question.toFrame = Frame.question

def Frame.toComplementType (fr : Frame) : Option ComplementType

Partial inverse of ComplementType.toFrame: the legacy enum cell a frame instantiates, none on frames richer than any cell.

Equations

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

theorem toComplementType_toFrame (ct : ComplementType) : ct.toFrame.toComplementType = some ct

The enum view round-trips over the smart-constructor cells.