Complementation — complement selection and control

[Noo07]

Per-entry complementation features: the legacy complement-type enum (ComplementType, the flat view over the typed Frame of Syntax/Clause/Frame.lean) and, for infinitival complements, its control type (ControlType).

The cross-linguistic complementation typology also lives here: [Noo07]'s six complement-clause types (NoonanCompType, linearly ordered from most to least finite via rank) and twelve complement-taking-predicate classes (CTPClass) with their default reality status (RealityStatus, ctpRealityStatus). The adapter between the two enum inventories (ComplementType.toNoonan) lives in Syntax/Clause/Complementation.lean.

Main declarations

• ComplementType — complement frame a predicate selects (English-leaning inventory: NP, double object, clausal, …)
• ControlType — subject/object control vs raising for infinitival complements
• NoonanCompType + isReduced + rank — [Noo07]'s complement-clause types with their finiteness order
• CTPClass, RealityStatus, ctpRealityStatus — [Noo07]'s CTP classification and realis/irrealis defaults

inductive ComplementType : Type

Complement type that the verb selects.

• Finite: "that" clauses ("John knows that Mary left")
• Infinitival: "to" complements ("John managed to leave")
• Gerund: "-ing" complements ("John stopped smoking")
• NP: Direct object ("John kicked the ball")
• None: Intransitive ("John slept")

• none : ComplementType
• np : ComplementType
• np_np : ComplementType
• np_pp : ComplementType
• finiteClause : ComplementType
• infinitival : ComplementType
• gerund : ComplementType
• smallClause : ComplementType
• question : ComplementType

@[implicit_reducible]

instance instDecidableEqComplementType : DecidableEq ComplementType

Equations

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

@[implicit_reducible]

instance instReprComplementType : Repr ComplementType

Equations

• instReprComplementType = { reprPrec := instReprComplementType.repr }

def instReprComplementType.repr : ComplementType → ℕ → Std.Format

Equations

• instReprComplementType.repr ComplementType.none prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ComplementType.none")).group prec✝
• instReprComplementType.repr ComplementType.np prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ComplementType.np")).group prec✝
• instReprComplementType.repr ComplementType.np_np prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ComplementType.np_np")).group prec✝
• instReprComplementType.repr ComplementType.np_pp prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ComplementType.np_pp")).group prec✝
• instReprComplementType.repr ComplementType.finiteClause prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ComplementType.finiteClause")).group prec✝
• instReprComplementType.repr ComplementType.infinitival prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ComplementType.infinitival")).group prec✝
• instReprComplementType.repr ComplementType.gerund prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ComplementType.gerund")).group prec✝
• instReprComplementType.repr ComplementType.smallClause prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ComplementType.smallClause")).group prec✝
• instReprComplementType.repr ComplementType.question prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ComplementType.question")).group prec✝

def ComplementType.isFinite : ComplementType → Bool

Is this complement type finite (i.e., does it contain a tense head)?

Finite complements (.finiteClause,.question) have independent tense morphology; non-finite complements (.infinitival,.gerund,.smallClause) do not.

Equations

• ComplementType.finiteClause.isFinite = true
• ComplementType.question.isFinite = true
• x✝.isFinite = false

def ComplementType.isNominal : ComplementType → Bool

Is this complement type a nominal (DP) argument?

Nominal complements project DP: the verb selects a noun phrase in object position. Relevant to c-selection in coordination: a verb that only selects nominal complements cannot independently license a CP conjunct ([Sch26]).

Equations

• ComplementType.np.isNominal = true
• ComplementType.np_np.isNominal = true
• ComplementType.np_pp.isNominal = true
• x✝.isNominal = false

def ComplementType.isClausal : ComplementType → Bool

Is this complement type a clausal (CP) argument?

Clausal complements project CP or reduced clausal structure. This covers finite clauses (dass-clauses), infinitivals, gerunds, small clauses, and embedded questions.

Equations

• ComplementType.finiteClause.isClausal = true
• ComplementType.infinitival.isClausal = true
• ComplementType.gerund.isClausal = true
• ComplementType.smallClause.isClausal = true
• ComplementType.question.isClausal = true
• x✝.isClausal = false

inductive ControlType : Type

Control type for verbs with infinitival complements.

• subjectControl : ControlType
• objectControl : ControlType
• raising : ControlType
• none : ControlType

@[implicit_reducible]

instance instDecidableEqControlType : DecidableEq ControlType

Equations

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

@[implicit_reducible]

instance instReprControlType : Repr ControlType

Equations

• instReprControlType = { reprPrec := instReprControlType.repr }

def instReprControlType.repr : ControlType → ℕ → Std.Format

Equations

• instReprControlType.repr ControlType.subjectControl prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ControlType.subjectControl")).group prec✝
• instReprControlType.repr ControlType.objectControl prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ControlType.objectControl")).group prec✝
• instReprControlType.repr ControlType.raising prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ControlType.raising")).group prec✝
• instReprControlType.repr ControlType.none prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ControlType.none")).group prec✝

Noonan complement typology

inductive NoonanCompType : Type

The six major complement types attested cross-linguistically. Ordered roughly from most to least "finite" (Noonan's "balanced" to "deranked").

• indicative : NoonanCompType
• subjunctive : NoonanCompType
• paratactic : NoonanCompType
• infinitive : NoonanCompType
• nominalized : NoonanCompType
• participle : NoonanCompType

@[implicit_reducible]

instance instDecidableEqNoonanCompType : DecidableEq NoonanCompType

Equations

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

def instReprNoonanCompType.repr : NoonanCompType → ℕ → Std.Format

Equations

• instReprNoonanCompType.repr NoonanCompType.indicative prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "NoonanCompType.indicative")).group prec✝
• instReprNoonanCompType.repr NoonanCompType.subjunctive prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "NoonanCompType.subjunctive")).group prec✝
• instReprNoonanCompType.repr NoonanCompType.paratactic prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "NoonanCompType.paratactic")).group prec✝
• instReprNoonanCompType.repr NoonanCompType.infinitive prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "NoonanCompType.infinitive")).group prec✝
• instReprNoonanCompType.repr NoonanCompType.nominalized prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "NoonanCompType.nominalized")).group prec✝
• instReprNoonanCompType.repr NoonanCompType.participle prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "NoonanCompType.participle")).group prec✝

@[implicit_reducible]

instance instReprNoonanCompType : Repr NoonanCompType

Equations

• instReprNoonanCompType = { reprPrec := instReprNoonanCompType.repr }

@[implicit_reducible]

instance instBEqNoonanCompType : BEq NoonanCompType

Equations

• instBEqNoonanCompType = { beq := instBEqNoonanCompType.beq }

def instBEqNoonanCompType.beq : NoonanCompType → NoonanCompType → Bool

Equations

• instBEqNoonanCompType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def NoonanCompType.isReduced : NoonanCompType → Bool

Is this complement type "reduced" (non-finite)?

Equations

• NoonanCompType.infinitive.isReduced = true
• NoonanCompType.nominalized.isReduced = true
• NoonanCompType.participle.isReduced = true
• x✝.isReduced = false

def NoonanCompType.rank : NoonanCompType → ℕ

[Noo07]'s balanced-to-deranked order as a numeric rank (indicative most finite, participle most deranked).

Equations

• NoonanCompType.indicative.rank = 0
• NoonanCompType.subjunctive.rank = 1
• NoonanCompType.paratactic.rank = 2
• NoonanCompType.infinitive.rank = 3
• NoonanCompType.nominalized.rank = 4
• NoonanCompType.participle.rank = 5

@[implicit_reducible]

instance instLinearOrderNoonanCompType : LinearOrder NoonanCompType

The balanced-to-deranked order: t ≤ t' iff t is at least as finite as t'.

Equations

• instLinearOrderNoonanCompType = LinearOrder.lift' NoonanCompType.rank instLinearOrderNoonanCompType._proof_1

inductive CTPClass : Type

Noonan's twelve CTP classes, organized by semantic contribution.

The ordering follows [Noo07] Table 2.1 from most to least "assertive":

• Utterance/propAttitude/pretence: report/judge propositional content
• Commentative/knowledge: evaluate/know propositional content
• Perception: direct experience
• Desiderative/manipulative/modal: irrealis orientation
• Achievement/phasal: aspectual
• Negative: negation as CTP

• utterance : CTPClass
• propAttitude : CTPClass
• pretence : CTPClass
• commentative : CTPClass
• knowledge : CTPClass
• perception : CTPClass
• desiderative : CTPClass
• manipulative : CTPClass
• modal : CTPClass
• achievement : CTPClass
• phasal : CTPClass
• negative : CTPClass

  A CTP whose sole semantic content is sentential negation ([Noo07] §3.2.13). Typologically rare; canonical examples are Fijian sega and Shuswap negative predicates. English avoid, refrain, prevent are NOT in this class — they are negative achievement predicates (§3.2.10).

@[implicit_reducible]

instance instDecidableEqCTPClass : DecidableEq CTPClass

Equations

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

def instReprCTPClass.repr : CTPClass → ℕ → Std.Format

Equations

• instReprCTPClass.repr CTPClass.utterance prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "CTPClass.utterance")).group prec✝
• instReprCTPClass.repr CTPClass.propAttitude prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "CTPClass.propAttitude")).group prec✝
• instReprCTPClass.repr CTPClass.pretence prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "CTPClass.pretence")).group prec✝
• instReprCTPClass.repr CTPClass.commentative prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "CTPClass.commentative")).group prec✝
• instReprCTPClass.repr CTPClass.knowledge prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "CTPClass.knowledge")).group prec✝
• instReprCTPClass.repr CTPClass.perception prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "CTPClass.perception")).group prec✝
• instReprCTPClass.repr CTPClass.desiderative prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "CTPClass.desiderative")).group prec✝
• instReprCTPClass.repr CTPClass.manipulative prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "CTPClass.manipulative")).group prec✝
• instReprCTPClass.repr CTPClass.modal prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "CTPClass.modal")).group prec✝
• instReprCTPClass.repr CTPClass.achievement prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "CTPClass.achievement")).group prec✝
• instReprCTPClass.repr CTPClass.phasal prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "CTPClass.phasal")).group prec✝
• instReprCTPClass.repr CTPClass.negative prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "CTPClass.negative")).group prec✝

@[implicit_reducible]

instance instReprCTPClass : Repr CTPClass

Equations

• instReprCTPClass = { reprPrec := instReprCTPClass.repr }

@[implicit_reducible]

instance instBEqCTPClass : BEq CTPClass

Equations

• instBEqCTPClass = { beq := instBEqCTPClass.beq }

def instBEqCTPClass.beq : CTPClass → CTPClass → Bool

Equations

• instBEqCTPClass.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

inductive RealityStatus : Type

The fundamental realis/irrealis split that predicts complement type selection. Realis CTPs tend toward indicative; irrealis toward subjunctive/infinitive ([Noo07] §2.3).

• realis : RealityStatus
• irrealis : RealityStatus

@[implicit_reducible]

instance instDecidableEqRealityStatus : DecidableEq RealityStatus

Equations

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

def instReprRealityStatus.repr : RealityStatus → ℕ → Std.Format

Equations

• instReprRealityStatus.repr RealityStatus.realis prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "RealityStatus.realis")).group prec✝
• instReprRealityStatus.repr RealityStatus.irrealis prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "RealityStatus.irrealis")).group prec✝

@[implicit_reducible]

instance instReprRealityStatus : Repr RealityStatus

Equations

• instReprRealityStatus = { reprPrec := instReprRealityStatus.repr }

def ctpRealityStatus : CTPClass → RealityStatus

Default reality status of each CTP class ([Noo07] Table 2.3).

Equations

• ctpRealityStatus CTPClass.utterance = RealityStatus.realis
• ctpRealityStatus CTPClass.propAttitude = RealityStatus.realis
• ctpRealityStatus CTPClass.pretence = RealityStatus.irrealis
• ctpRealityStatus CTPClass.commentative = RealityStatus.realis
• ctpRealityStatus CTPClass.knowledge = RealityStatus.realis
• ctpRealityStatus CTPClass.perception = RealityStatus.realis
• ctpRealityStatus CTPClass.desiderative = RealityStatus.irrealis
• ctpRealityStatus CTPClass.manipulative = RealityStatus.irrealis
• ctpRealityStatus CTPClass.modal = RealityStatus.irrealis
• ctpRealityStatus CTPClass.achievement = RealityStatus.irrealis
• ctpRealityStatus CTPClass.phasal = RealityStatus.realis
• ctpRealityStatus CTPClass.negative = RealityStatus.irrealis