Complementation — Noonan typology and control

[Noo07]

The cross-linguistic complementation typology: [Noo07]'s six morphological complement codings (Complement.Coding, in his summary table's row order via rank) and twelve of his fourteen complement-taking-predicate classes (CTPClass) with their default reality status (RealityStatus, ctpRealityStatus), plus the control enum for infinitival complements (ControlType).

The typed complement-frame object, the flat ComplementType view, and the adapter (ComplementType.toCoding) live in Syntax/Category/Verb/Complement/Basic.lean; the verb–complementizer compatibility relation in Syntax/Category/Verb/Complement/Takes.lean. Data/Complementation/Schema.lean types its rows with these enums — the one deliberate theory-layer import in Data/, carrying descriptive typological vocabulary rather than analytical commitments.

Main declarations

• Complement.Coding + isReduced + rank — [Noo07]'s complement types, classified by the morphological coding of the complement clause
• CTPClass, RealityStatus, ctpRealityStatus — [Noo07]'s CTP classification and realis/irrealis defaults
• ControlType — subject/object control vs raising for infinitival complements

inductive ControlType : Type

Control type for verbs with infinitival complements.

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

@[instance_reducible]

instance instDecidableEqControlType : DecidableEq ControlType

Equations

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

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✝

@[instance_reducible]

instance instReprControlType : Repr ControlType

Equations

• instReprControlType = { reprPrec := instReprControlType.repr }

Noonan complement typology

inductive Complement.Coding : Type

The six major complement types of [Noo07]'s survey, classified by the morphological coding of the complement clause (part of speech of its predicate, subject relation, inflectional range).

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

@[instance_reducible]

instance Complement.instDecidableEqCoding : DecidableEq Coding

Equations

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

@[instance_reducible]

instance Complement.instReprCoding : Repr Coding

Equations

• Complement.instReprCoding = { reprPrec := Complement.instReprCoding.repr }

def Complement.instReprCoding.repr : Coding → ℕ → Std.Format

Equations

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

def Complement.instBEqCoding.beq : Coding → Coding → Bool

Equations

• Complement.instBEqCoding.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[instance_reducible]

instance Complement.instBEqCoding : BEq Coding

Equations

• Complement.instBEqCoding = { beq := Complement.instBEqCoding.beq }

def Complement.Coding.isReduced : Coding → Bool

Is this coding non-finite (infinitive, nominalized, participial)?

Equations

• Complement.Coding.infinitive.isReduced = true
• Complement.Coding.nominalized.isReduced = true
• Complement.Coding.participle.isReduced = true
• x✝.isReduced = false

def Complement.Coding.rank : Coding → ℕ

Position in [Noo07]'s summary-table row order (indicative first, participle last). A presentation order, not an inflectional finiteness scale: paratactic complements carry the same inflectional range as indicatives.

Equations

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

@[instance_reducible]

instance Complement.instLinearOrderCoding : LinearOrder Coding

The summary-table row order as a linear order.

Equations

• Complement.instLinearOrderCoding = LinearOrder.lift' Complement.Coding.rank Complement.instLinearOrderCoding._proof_1

inductive CTPClass : Type

Twelve of [Noo07]'s fourteen CTP classes (§3.2; predicates of fearing §3.2.6 and conjunctive predicates §3.2.14 are omitted), in the chapter's presentation order with perception hoisted next to the epistemic classes:

• 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).

@[instance_reducible]

instance instDecidableEqCTPClass : DecidableEq CTPClass

Equations

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

@[instance_reducible]

instance instReprCTPClass : Repr CTPClass

Equations

• instReprCTPClass = { reprPrec := instReprCTPClass.repr }

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✝

def instBEqCTPClass.beq : CTPClass → CTPClass → Bool

Equations

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

@[instance_reducible]

instance instBEqCTPClass : BEq CTPClass

Equations

• instBEqCTPClass = { beq := instBEqCTPClass.beq }

inductive RealityStatus : Type

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

• realis : RealityStatus
• irrealis : RealityStatus

@[instance_reducible]

instance instDecidableEqRealityStatus : DecidableEq RealityStatus

Equations

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

@[instance_reducible]

instance instReprRealityStatus : Repr RealityStatus

Equations

• instReprRealityStatus = { reprPrec := instReprRealityStatus.repr }

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✝

def ctpRealityStatus : CTPClass → RealityStatus

Default reality status of each CTP class, extending [Noo07]'s realis/irrealis mood distinction (§3.1.1) from complement roles to CTP classes. The phasal and perception assignments are extensions: Noonan assigns their complements determined time reference, not a mood value.

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