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 (Complement.PredicateClass) with their default reality status (RealityStatus, Complement.PredicateClass.realityStatus), plus the control enum for infinitival complements (ControlType).

The argument frames live in Syntax/Category/Verb/ArgumentFrame/Basic.lean; the verb–complementizer compatibility relation in Syntax/Category/Verb/ArgumentFrame/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
• Complement.PredicateClass, RealityStatus, Complement.PredicateClass.realityStatus — [Noo07]'s predicate 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.Coding.IsFinite : Coding → Prop

The coding is finite: an indicative, subjunctive or paratactic clause.

Equations

• Complement.Coding.indicative.IsFinite = True
• Complement.Coding.subjunctive.IsFinite = True
• Complement.Coding.paratactic.IsFinite = True
• Complement.Coding.infinitive.IsFinite = False
• Complement.Coding.nominalized.IsFinite = False
• Complement.Coding.participle.IsFinite = False

@[instance_reducible]

instance Complement.instDecidablePredCodingIsFinite : DecidablePred Coding.IsFinite

Equations

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

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 ⋯

inductive Complement.PredicateClass : Type

Twelve of [Noo07]'s fourteen classes of complement-taking predicate (§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 the predicate

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

  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 Complement.instDecidableEqPredicateClass : DecidableEq PredicateClass

Equations

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

@[instance_reducible]

instance Complement.instReprPredicateClass : Repr PredicateClass

Equations

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

def Complement.instReprPredicateClass.repr : PredicateClass → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Complement.instBEqPredicateClass : BEq PredicateClass

Equations

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

def Complement.instBEqPredicateClass.beq : PredicateClass → PredicateClass → Bool

Equations

• Complement.instBEqPredicateClass.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] §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 ⋯

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✝

@[instance_reducible]

instance instReprRealityStatus : Repr RealityStatus

Equations

• instReprRealityStatus = { reprPrec := instReprRealityStatus.repr }

def Complement.PredicateClass.realityStatus : PredicateClass → RealityStatus

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

Equations

• Complement.PredicateClass.utterance.realityStatus = RealityStatus.realis
• Complement.PredicateClass.propAttitude.realityStatus = RealityStatus.realis
• Complement.PredicateClass.pretence.realityStatus = RealityStatus.irrealis
• Complement.PredicateClass.commentative.realityStatus = RealityStatus.realis
• Complement.PredicateClass.knowledge.realityStatus = RealityStatus.realis
• Complement.PredicateClass.perception.realityStatus = RealityStatus.realis
• Complement.PredicateClass.desiderative.realityStatus = RealityStatus.irrealis
• Complement.PredicateClass.manipulative.realityStatus = RealityStatus.irrealis
• Complement.PredicateClass.modal.realityStatus = RealityStatus.irrealis
• Complement.PredicateClass.achievement.realityStatus = RealityStatus.irrealis
• Complement.PredicateClass.phasal.realityStatus = RealityStatus.realis
• Complement.PredicateClass.negative.realityStatus = RealityStatus.irrealis