Documentation

Linglib.Typology.Complementation

Typology.Complementation #

@cite{noonan-2007} @cite{dryer-2013-wals} @cite{dryer-haspelmath-2013}

Per-language typological substrate for complementation, subordination, and complement-taking predicates (CTPs), covering @cite{noonan-2007}'s typology plus seven WALS chapters:

Ch 94 (@cite{dryer-2013-wals}): Order of adverbial subordinator and clause.
Ch 95 (@cite{dryer-2013-wals}): OV order × adposition type.
Ch 124--128 (Cristofaro): 'Want' complement subjects, purpose clauses, 'when' clauses, reason clauses, utterance complement clauses.

Mirrors the Linglib/Typology/{Possession,Negation,Comparison,Coordination, Modality,Gender,Alignment,ArgumentStructure,Copulas,Morphology} substrate- extension pattern. Fragment-importable.

What lives here #

§1. Noonan complement typology: NoonanCompType, CTPClass, RealityStatus, ctpRealityStatus, CTPDatum, NoonanCompType.isReduced.
§2. Subordination typology (Ch 94--95): SubordinatorOrder, OVAdpositionType, ComplementizerPosition, RelativeClausePosition, PurposeClauseStrategy, SubordinationProfile + helpers.
§3. WALSCount row struct + totalOf.
§4. Cristofaro complementation typology (Ch 124--128): BalancedDeranked, WantCompStrategy, ComplementationProfile.
§5. WALS converters fromWALS{124A,125A,126A,127A,128A}.
§6. WALS aggregate sample-size theorems.
§7. Corpus-only generalisations: initial subordinator dominance, harmonic-pattern dominance, OV-postpositions strength, utterance-complements-mostly-balanced, purpose-deranked-more-than-utterance.

Theory-laden caveats #

RealityStatus is Noonan's binary realis/irrealis split; finer modal/evidential distinctions live elsewhere.
BalancedDeranked is Cristofaro's coarse classification; it conflates the Noonan-style finer typology (indicative/subjunctive/infinitive/...) into three buckets. The Noonan ↔ Cristofaro mapping is non-trivial: balanced ≈ indicative/subjunctive, deranked ≈ infinitive/nominalized/ participle, balancedDeranked = both.
ctpRealityStatus's default for phasal is realis (start/stop/continue presuppose the event has happened), but specific lexical items can override.

Out of scope #

The CTP per-verb data (Sections E-G of the original file: english_say, latin_dicere, etc.) and Noonan's verified generalizations (G1--G4: realis/irrealis split, equi-deletion restriction, negative raising, indicative hierarchy) live in Phenomena/Complementation/Studies/ Noonan2007.lean.
The 20-language SubordinationProfile sample, the Q1--Q12 typological generalizations, and areal pattern theorems live in Phenomena/Complementation/Studies/Dryer2013.lean.
The 19-language ComplementationProfile sample and W/X cross-chapter generalizations live in Phenomena/Complementation/Studies/Cristofaro2013.lean.

inductive Typology.Complementation.NoonanCompType :

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

Instances For

@[implicit_reducible]

instance Typology.Complementation.instDecidableEqNoonanCompType :

DecidableEq NoonanCompType

Equations

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

def Typology.Complementation.instReprNoonanCompType.repr :

NoonanCompType → Nat → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Typology.Complementation.instReprNoonanCompType :

Repr NoonanCompType

Equations

Typology.Complementation.instReprNoonanCompType = { reprPrec := Typology.Complementation.instReprNoonanCompType.repr }

def Typology.Complementation.NoonanCompType.isReduced :

NoonanCompType → Bool

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

Equations

Typology.Complementation.NoonanCompType.infinitive.isReduced = true
Typology.Complementation.NoonanCompType.nominalized.isReduced = true
Typology.Complementation.NoonanCompType.participle.isReduced = true
x✝.isReduced = false

Instances For

inductive Typology.Complementation.CTPClass :

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

The ordering follows @cite{noonan-2007} 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 (@cite{noonan-2007} §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).

Instances For

@[implicit_reducible]

instance Typology.Complementation.instDecidableEqCTPClass :

DecidableEq CTPClass

Equations

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

def Typology.Complementation.instReprCTPClass.repr :

CTPClass → Nat → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Typology.Complementation.instReprCTPClass :

Equations

Typology.Complementation.instReprCTPClass = { reprPrec := Typology.Complementation.instReprCTPClass.repr }

inductive Typology.Complementation.RealityStatus :

The fundamental realis/irrealis split that predicts complement type selection. Realis CTPs tend toward indicative; irrealis toward subjunctive/infinitive (@cite{noonan-2007} §2.3).

realis : RealityStatus
irrealis : RealityStatus

Instances For

@[implicit_reducible]

instance Typology.Complementation.instDecidableEqRealityStatus :

DecidableEq RealityStatus

Equations

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

@[implicit_reducible]

instance Typology.Complementation.instReprRealityStatus :

Repr RealityStatus

Equations

Typology.Complementation.instReprRealityStatus = { reprPrec := Typology.Complementation.instReprRealityStatus.repr }

def Typology.Complementation.instReprRealityStatus.repr :

RealityStatus → Nat → Std.Format

Equations

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

Instances For

def Typology.Complementation.ctpRealityStatus :

CTPClass → RealityStatus

Default reality status of each CTP class (@cite{noonan-2007} Table 2.3).

Equations

Instances For

structure Typology.Complementation.CTPDatum :

A cross-linguistic datum about a complement-taking predicate.

Each datum records:

Language and verb identification
CTP class (Noonan Table 2.1)
Which complement types this verb allows in this language
Reality status (defaults to ctpRealityStatus ctpClass, but overridable for exceptions)
Control/raising properties (@cite{noonan-2007} §2.1--2.2)
Negative raising

language : String
verb : String
ctpClass : CTPClass
allowedCompTypes : List NoonanCompType
realityStatus : RealityStatus
hasEquiDeletion : Bool
hasRaising : Bool
hasNegativeRaising : Bool

Instances For

def Typology.Complementation.instDecidableEqCTPDatum.decEq (x✝ x✝¹ : CTPDatum) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

@[implicit_reducible]

instance Typology.Complementation.instDecidableEqCTPDatum :

DecidableEq CTPDatum

Equations

Typology.Complementation.instDecidableEqCTPDatum = Typology.Complementation.instDecidableEqCTPDatum.decEq

@[implicit_reducible]

instance Typology.Complementation.instReprCTPDatum :

Equations

Typology.Complementation.instReprCTPDatum = { reprPrec := Typology.Complementation.instReprCTPDatum.repr }

def Typology.Complementation.instReprCTPDatum.repr :

CTPDatum → Nat → Std.Format

Equations

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

Instances For

inductive Typology.Complementation.SubordinatorOrder :

WALS Ch 94: How adverbial subordinators are positioned relative to their clause.

initialWord : SubordinatorOrder
Subordinator is a free word preceding the clause. E.g., English "because he left", Arabic "li'anna-hu ghaadara".
finalWord : SubordinatorOrder
Subordinator is a free word following the clause. E.g., Japanese "kare-ga kaetta kara".
finalSuffix : SubordinatorOrder
Subordinator is a suffix on the verb at the end of the clause. E.g., Turkish "-dIgI icin".
mixed : SubordinatorOrder
Mixed or no dominant subordination pattern.

Instances For

@[implicit_reducible]

instance Typology.Complementation.instDecidableEqSubordinatorOrder :

DecidableEq SubordinatorOrder

Equations

Typology.Complementation.instDecidableEqSubordinatorOrder x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Typology.Complementation.instReprSubordinatorOrder :

Repr SubordinatorOrder

Equations

Typology.Complementation.instReprSubordinatorOrder = { reprPrec := Typology.Complementation.instReprSubordinatorOrder.repr }

def Typology.Complementation.instReprSubordinatorOrder.repr :

SubordinatorOrder → Nat → Std.Format

Equations

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

Instances For

inductive Typology.Complementation.OVAdpositionType :

WALS Ch 95: Four-way classification combining verb-object order with adposition type. The two "harmonic" patterns dominate; the two "disharmonic" patterns are rare.

voPrep : OVAdpositionType
VO order with prepositions (head-initial harmony).
ovPostp : OVAdpositionType
OV order with postpositions (head-final harmony).
voPostp : OVAdpositionType
VO order with postpositions (disharmonic; rare).
ovPrep : OVAdpositionType
OV order with prepositions (disharmonic; rare).

Instances For

@[implicit_reducible]

instance Typology.Complementation.instDecidableEqOVAdpositionType :

DecidableEq OVAdpositionType

Equations

Typology.Complementation.instDecidableEqOVAdpositionType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Typology.Complementation.instReprOVAdpositionType :

Repr OVAdpositionType

Equations

Typology.Complementation.instReprOVAdpositionType = { reprPrec := Typology.Complementation.instReprOVAdpositionType.repr }

def Typology.Complementation.instReprOVAdpositionType.repr :

OVAdpositionType → Nat → Std.Format

Equations

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

Instances For

inductive Typology.Complementation.ComplementizerPosition :

Position of the complementizer (the subordinating morpheme introducing a complement clause, e.g., English "that"). Strongly mirrors the subordinator order from WALS Ch 94.

Instances For

@[implicit_reducible]

instance Typology.Complementation.instDecidableEqComplementizerPosition :

DecidableEq ComplementizerPosition

Equations

Typology.Complementation.instDecidableEqComplementizerPosition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Typology.Complementation.instReprComplementizerPosition.repr :

ComplementizerPosition → Nat → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Typology.Complementation.instReprComplementizerPosition :

Repr ComplementizerPosition

Equations

Typology.Complementation.instReprComplementizerPosition = { reprPrec := Typology.Complementation.instReprComplementizerPosition.repr }

inductive Typology.Complementation.RelativeClausePosition :

Position of the relative clause with respect to the head noun. WALS Ch 90 documents the cross-linguistic distribution.

postNominal : RelativeClausePosition
preNominal : RelativeClausePosition
internallyHeaded : RelativeClausePosition
correlative : RelativeClausePosition

Instances For

@[implicit_reducible]

instance Typology.Complementation.instDecidableEqRelativeClausePosition :

DecidableEq RelativeClausePosition

Equations

Typology.Complementation.instDecidableEqRelativeClausePosition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Typology.Complementation.instReprRelativeClausePosition.repr :

RelativeClausePosition → Nat → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Typology.Complementation.instReprRelativeClausePosition :

Repr RelativeClausePosition

Equations

Typology.Complementation.instReprRelativeClausePosition = { reprPrec := Typology.Complementation.instReprRelativeClausePosition.repr }

inductive Typology.Complementation.PurposeClauseStrategy :

Strategy for expressing purpose clauses ("in order to V").

subjunctive : PurposeClauseStrategy
infinitive : PurposeClauseStrategy
nominalization : PurposeClauseStrategy
serialVerb : PurposeClauseStrategy

Instances For

@[implicit_reducible]

instance Typology.Complementation.instDecidableEqPurposeClauseStrategy :

DecidableEq PurposeClauseStrategy

Equations

Typology.Complementation.instDecidableEqPurposeClauseStrategy x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Typology.Complementation.instReprPurposeClauseStrategy.repr :

PurposeClauseStrategy → Nat → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Typology.Complementation.instReprPurposeClauseStrategy :

Repr PurposeClauseStrategy

Equations

Typology.Complementation.instReprPurposeClauseStrategy = { reprPrec := Typology.Complementation.instReprPurposeClauseStrategy.repr }

structure Typology.Complementation.SubordinationProfile :

A language's subordination profile combining all five dimensions.

language : String
iso : String
subordinatorOrder : SubordinatorOrder
Ch 94: order of adverbial subordinator and clause.
ovAdposition : OVAdpositionType
Ch 95: OV order × adposition type.
compPosition : ComplementizerPosition
Complementizer position (initial, final, or none).
rcPosition : RelativeClausePosition
Relative clause position.
purposeStrategy : PurposeClauseStrategy
Purpose clause strategy.
basicOrder : String
Basic word order label for cross-referencing.
notes : String
Notes on the subordination system.

Instances For

def Typology.Complementation.instReprSubordinationProfile.repr :

SubordinationProfile → Nat → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Typology.Complementation.instReprSubordinationProfile :

Repr SubordinationProfile

Equations

Typology.Complementation.instReprSubordinationProfile = { reprPrec := Typology.Complementation.instReprSubordinationProfile.repr }

def Typology.Complementation.SubordinationProfile.hasInitialSubordinator (p : SubordinationProfile) :

Bool

Does this profile have an initial subordinator?

Equations

p.hasInitialSubordinator = (p.subordinatorOrder == Typology.Complementation.SubordinatorOrder.initialWord)

Instances For

def Typology.Complementation.SubordinationProfile.hasFinalSubordinator (p : SubordinationProfile) :

Bool

Does this profile have a final subordinator (word or suffix)?

Equations

p.hasFinalSubordinator = (p.subordinatorOrder == Typology.Complementation.SubordinatorOrder.finalWord || p.subordinatorOrder == Typology.Complementation.SubordinatorOrder.finalSuffix)

Instances For

def Typology.Complementation.SubordinationProfile.isVO (p : SubordinationProfile) :

Bool

Does this profile have VO order?

Equations

p.isVO = (p.ovAdposition == Typology.Complementation.OVAdpositionType.voPrep || p.ovAdposition == Typology.Complementation.OVAdpositionType.voPostp)

Instances For

def Typology.Complementation.SubordinationProfile.isOV (p : SubordinationProfile) :

Bool

Does this profile have OV order?

Equations

p.isOV = (p.ovAdposition == Typology.Complementation.OVAdpositionType.ovPostp || p.ovAdposition == Typology.Complementation.OVAdpositionType.ovPrep)

Instances For

def Typology.Complementation.SubordinationProfile.hasPreNominalRC (p : SubordinationProfile) :

Bool

Does this profile have pre-nominal RCs?

Equations

p.hasPreNominalRC = (p.rcPosition == Typology.Complementation.RelativeClausePosition.preNominal)

Instances For

def Typology.Complementation.SubordinationProfile.hasPostNominalRC (p : SubordinationProfile) :

Bool

Does this profile have post-nominal RCs?

Equations

p.hasPostNominalRC = (p.rcPosition == Typology.Complementation.RelativeClausePosition.postNominal)

Instances For

WALSCount + WALSCount.totalOf are imported from Linglib/Data/WALS/Aggregation.lean (shared with the other Typology files that consume WALS distributions).

inductive Typology.Complementation.BalancedDeranked :

Cristofaro's balanced/deranked typology for complement clauses (shared across WALS Chapters 125A--128A). "Balanced" means the complement retains main-clause morphology; "deranked" means it uses reduced/non-finite forms; "balancedDeranked" means both strategies exist.

balanced : BalancedDeranked
balancedDeranked : BalancedDeranked
deranked : BalancedDeranked

Instances For

@[implicit_reducible]

instance Typology.Complementation.instDecidableEqBalancedDeranked :

DecidableEq BalancedDeranked

Equations

Typology.Complementation.instDecidableEqBalancedDeranked x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Typology.Complementation.instReprBalancedDeranked :

Repr BalancedDeranked

Equations

Typology.Complementation.instReprBalancedDeranked = { reprPrec := Typology.Complementation.instReprBalancedDeranked.repr }

def Typology.Complementation.instReprBalancedDeranked.repr :

BalancedDeranked → Nat → Std.Format

Equations

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

Instances For

inductive Typology.Complementation.WantCompStrategy :

Cristofaro's 'want' complement subject typology (WALS Ch 124A). Captures whether desiderative CTPs leave the complement subject implicit or express it overtly -- plus the desiderative affix/particle alternative where 'want' is not a separate verb.

subjectImplicit : WantCompStrategy
subjectOvert : WantCompStrategy
both : WantCompStrategy
desidAffix : WantCompStrategy
desidParticle : WantCompStrategy

Instances For

@[implicit_reducible]

instance Typology.Complementation.instDecidableEqWantCompStrategy :

DecidableEq WantCompStrategy

Equations

Typology.Complementation.instDecidableEqWantCompStrategy x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Typology.Complementation.instReprWantCompStrategy.repr :

WantCompStrategy → Nat → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Typology.Complementation.instReprWantCompStrategy :

Repr WantCompStrategy

Equations

Typology.Complementation.instReprWantCompStrategy = { reprPrec := Typology.Complementation.instReprWantCompStrategy.repr }

structure Typology.Complementation.ComplementationProfile :

A language's complementation profile across WALS Chapters 124A--128A. Fields are optional because not every language appears in every WALS chapter's sample.

language : String
walsCode : String
wantComp : Option WantCompStrategy
Ch 124A: 'want' complement subject strategy.
purposeClause : Option BalancedDeranked
Ch 125A: purpose clause type.
whenClause : Option BalancedDeranked
Ch 126A: 'when' clause type.
reasonClause : Option BalancedDeranked
Ch 127A: reason clause type.
utteranceComp : Option BalancedDeranked
Ch 128A: utterance complement clause type.
notes : String
Notes on the complementation system.

Instances For

@[implicit_reducible]

instance Typology.Complementation.instReprComplementationProfile :

Repr ComplementationProfile

Equations

Typology.Complementation.instReprComplementationProfile = { reprPrec := Typology.Complementation.instReprComplementationProfile.repr }

def Typology.Complementation.instReprComplementationProfile.repr :

ComplementationProfile → Nat → Std.Format

Equations

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

Instances For

def Typology.Complementation.instDecidableEqComplementationProfile.decEq (x✝ x✝¹ : ComplementationProfile) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

@[implicit_reducible]

instance Typology.Complementation.instDecidableEqComplementationProfile :

DecidableEq ComplementationProfile

Equations

Typology.Complementation.instDecidableEqComplementationProfile = Typology.Complementation.instDecidableEqComplementationProfile.decEq

def Typology.Complementation.fromWALS124A :

Data.WALS.F124A.WantComplementSubject → WantCompStrategy

Map WALS F124A to WantCompStrategy.

Equations

Instances For

def Typology.Complementation.fromWALS125A :

Data.WALS.F125A.PurposeClauseType → BalancedDeranked

Map WALS F125A to BalancedDeranked.

Equations

Instances For

def Typology.Complementation.fromWALS126A :

Data.WALS.F126A.WhenClauseType → BalancedDeranked

Map WALS F126A to BalancedDeranked.

Equations

Instances For

def Typology.Complementation.fromWALS127A :

Data.WALS.F127A.ReasonClauseType → BalancedDeranked

Map WALS F127A to BalancedDeranked.

Equations

Instances For

def Typology.Complementation.fromWALS128A :

Data.WALS.F128A.UtteranceComplementType → BalancedDeranked

Map WALS F128A to BalancedDeranked.

Equations

Instances For

theorem Typology.Complementation.ch94_initial_word_most_common :

have init := (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F94A.OrderOfAdverbialSubordinatorAndClause) => x.value == Data.WALS.F94A.OrderOfAdverbialSubordinatorAndClause.initialSubordinatorWord) Typology.Complementation.ch94✝).length; init > (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F94A.OrderOfAdverbialSubordinatorAndClause) => x.value == Data.WALS.F94A.OrderOfAdverbialSubordinatorAndClause.finalSubordinatorWord) Typology.Complementation.ch94✝).length ∧ init > (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F94A.OrderOfAdverbialSubordinatorAndClause) => x.value == Data.WALS.F94A.OrderOfAdverbialSubordinatorAndClause.internalSubordinatorWord) Typology.Complementation.ch94✝).length ∧ init > (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F94A.OrderOfAdverbialSubordinatorAndClause) => x.value == Data.WALS.F94A.OrderOfAdverbialSubordinatorAndClause.subordinatingSuffix) Typology.Complementation.ch94✝).length ∧ init > (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F94A.OrderOfAdverbialSubordinatorAndClause) => x.value == Data.WALS.F94A.OrderOfAdverbialSubordinatorAndClause.mixed) Typology.Complementation.ch94✝).length

Ch 94: initial subordinator words are by far the most common type.

theorem Typology.Complementation.ch94_initial_dominates_final :

(List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F94A.OrderOfAdverbialSubordinatorAndClause) => x.value == Data.WALS.F94A.OrderOfAdverbialSubordinatorAndClause.initialSubordinatorWord) Typology.Complementation.ch94✝).length > (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F94A.OrderOfAdverbialSubordinatorAndClause) => x.value == Data.WALS.F94A.OrderOfAdverbialSubordinatorAndClause.finalSubordinatorWord) Typology.Complementation.ch94✝).length + (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F94A.OrderOfAdverbialSubordinatorAndClause) => x.value == Data.WALS.F94A.OrderOfAdverbialSubordinatorAndClause.subordinatingSuffix) Typology.Complementation.ch94✝).length

Ch 94: initial subordinator words outnumber final words plus suffixes combined.

theorem Typology.Complementation.ch94_initial_over_60_percent :

(List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F94A.OrderOfAdverbialSubordinatorAndClause) => x.value == Data.WALS.F94A.OrderOfAdverbialSubordinatorAndClause.initialSubordinatorWord) Typology.Complementation.ch94✝).length * 100 > Typology.Complementation.ch94✝.length * 60

Ch 94: initial subordinator words account for over 60% of the sample.

theorem Typology.Complementation.ch95_harmonic_dominant :

(List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F95A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdpositionAndNounPhrase) => x.value == Data.WALS.F95A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdpositionAndNounPhrase.voAndPrepositions) Typology.Complementation.ch95✝).length + (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F95A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdpositionAndNounPhrase) => x.value == Data.WALS.F95A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdpositionAndNounPhrase.ovAndPostpositions) Typology.Complementation.ch95✝).length > Typology.Complementation.ch95✝.length * 8 / 10

Ch 95: harmonic patterns (VO+Prep, OV+Postp) account for over 80% of sampled languages. The OV-postposition correlation is one of the strongest in typology.

theorem Typology.Complementation.ch95_ov_postp_most_common :

(List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F95A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdpositionAndNounPhrase) => x.value == Data.WALS.F95A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdpositionAndNounPhrase.ovAndPostpositions) Typology.Complementation.ch95✝).length > (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F95A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdpositionAndNounPhrase) => x.value == Data.WALS.F95A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdpositionAndNounPhrase.voAndPrepositions) Typology.Complementation.ch95✝).length

Ch 95: OV+Postpositions is the single most common pairing.

theorem Typology.Complementation.ch95_disharmonic_rare :

((List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F95A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdpositionAndNounPhrase) => x.value == Data.WALS.F95A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdpositionAndNounPhrase.voAndPostpositions) Typology.Complementation.ch95✝).length + (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F95A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdpositionAndNounPhrase) => x.value == Data.WALS.F95A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdpositionAndNounPhrase.ovAndPrepositions) Typology.Complementation.ch95✝).length) * 100 < Typology.Complementation.ch95✝.length * 6

Ch 95: disharmonic patterns are rare (under 6% of the sample).

theorem Typology.Complementation.utterance_comps_mostly_balanced :

(List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F128A.UtteranceComplementType) => x.value == Data.WALS.F128A.UtteranceComplementType.balanced) Typology.Complementation.ch128✝).length > (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F128A.UtteranceComplementType) => x.value == Data.WALS.F128A.UtteranceComplementType.deranked) Typology.Complementation.ch128✝).length * 10

Ch 128: utterance complements are overwhelmingly balanced; "say/tell" complements tend to retain main-clause morphology cross-linguistically.

theorem Typology.Complementation.purpose_more_deranked_than_utterance :

(List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F125A.PurposeClauseType) => x.value == Data.WALS.F125A.PurposeClauseType.deranked) Typology.Complementation.ch125✝).length > (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F128A.UtteranceComplementType) => x.value == Data.WALS.F128A.UtteranceComplementType.deranked) Typology.Complementation.ch128✝).length

Cross-chapter: purpose clauses (Ch 125) favor deranking more than utterance complements (Ch 128). Reflects the irrealis orientation of purpose clauses.

Theory-neutral surface enum #

Following the cross-framework reconciler discipline, ComplementClauseStructure describes the surface pattern a notional complement clause realises, without committing to one framework's internal analysis. Each Theory projects its native account into this enum: HPSG always projects headExternalModifier for true RCs; Minimalist (with @cite{deal-2026}) projects abarInternalCP for Nez Perce relative-embeddings (REs) and barePropositionalCP for English that-clauses.

inductive Typology.Complementation.ComplementClauseStructure :

Surface-pattern enumeration of notional-complement-clause shapes attested cross-linguistically.

@cite{deal-2026}'s typology dissolves the Kayne/Arsenij'evi'c (@cite{kayne-2008}, @cite{kayne-2014}, @cite{arsenijevic-2009}) universalist claim that all clausal complementation is relativization. The surface options are independent of any one framework's commitments about underlying structure.

The Kayne/Arsenij'evi'c universalist hypothesis is now a single decidable statement: ∀ c : ComplementClauseStructure, c = .abarInternalCP. Deal 2026 refutes it by exhibiting .barePropositionalCP as an attested cell (Nez Perce simplex embeddings and English think-complementation).

abarInternalCP : ComplementClauseStructure
CP with internal Ā-dependency from a high functional projection above TP. Nez Perce REs (@cite{deal-2026}), Adyghe REs (@cite{caponigro-polinsky-2011}), Bulgarian REs (@cite{krapova-2010}).
barePropositionalCP : ComplementClauseStructure
Bare CP with no internal Ā-dependency. Nez Perce simplex embeddings and English think-complementation (@cite{deal-2026}).
nominalization : ComplementClauseStructure
CP wrapped in a nominal projection (D, possibly with N). Washo factive complementation (@cite{hanink-bochnak-2017}, @cite{bochnak-hanink-2021}), Ndebele (@cite{pietraszko-2019}, with additional P shell).
headExternalModifier : ComplementClauseStructure
True relative clause: an adjunct modifier of a head noun. The pattern that Kayne/Arsenij'evi'c claim subsumes all others.
headInternalRelative : ComplementClauseStructure
Internally-headed relative clause (Bambara, Navajo).
adjunct : ComplementClauseStructure
High adjunct, not complementation at all. Amahuaca attitude reports (@cite{deal-2026} §3, citing Clem 2022 — needs separate bib entry).

Instances For

@[implicit_reducible]

instance Typology.Complementation.instDecidableEqComplementClauseStructure :

DecidableEq ComplementClauseStructure

Equations

Typology.Complementation.instDecidableEqComplementClauseStructure x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Typology.Complementation.instReprComplementClauseStructure.repr :

ComplementClauseStructure → Nat → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Typology.Complementation.instReprComplementClauseStructure :

Repr ComplementClauseStructure

Equations

Typology.Complementation.instReprComplementClauseStructure = { reprPrec := Typology.Complementation.instReprComplementClauseStructure.repr }

CP-external wrapping shells #

Where ComplementSize and ClauseSpine (Theories/Syntax/Minimalist/) record internal clause height (vP/TP/CP/NmlzP), CPShell records what wraps the CP externally. Deal 2026's Table 79 cross-classifies the two axes; this file houses the external axis as Fragment-importable substrate.

Anchored to @cite{deal-2026} Table 79; placement of individual languages in Table 79 cells consumes per-language Fragment data and lives in Phenomena/Complementation/Studies/Deal2026.lean.

inductive Typology.Complementation.CPShell :

A wrapping head category that may appear above a CP in a notional complement. @cite{deal-2026} Table 79 attests three: D (Washo, Adyghe), N (Adyghe), P (Bulgarian, Ndebele). C is included as the base case to give a uniform representation of bareCP as [.C].

c : CPShell
The CP itself (always present).
d : CPShell
D shell (determiner wrapping CP).
n : CPShell
N shell (nominal head between D and CP).
p : CPShell
P shell (preposition wrapping the CP-headed argument).

Instances For

@[implicit_reducible]

instance Typology.Complementation.instDecidableEqCPShell :

DecidableEq CPShell

Equations

Typology.Complementation.instDecidableEqCPShell x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Typology.Complementation.instReprCPShell.repr :

CPShell → Nat → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Typology.Complementation.instReprCPShell :

Equations

Typology.Complementation.instReprCPShell = { reprPrec := Typology.Complementation.instReprCPShell.repr }

@[reducible, inline]

abbrev Typology.Complementation.CPShellInventory :

An ordered shell list, innermost first.

Convention: head element is the C of the CP itself; subsequent elements are progressively more peripheral wrappers. So [.c, .d] = dCP (D wraps CP), [.c, .n, .d] = dnCP (D wraps N wraps CP), [.c, .d, .p] = pdCP (P wraps D wraps CP).

Equations

Typology.Complementation.CPShellInventory = List Typology.Complementation.CPShell

Instances For

def Typology.Complementation.isAttestedShell :

CPShellInventory → Bool

Predicate: this shell inventory is attested in @cite{deal-2026} Table 79.

Six attested shapes (one per cell), four shell-shapes:

[.c] = bareCP (V CP row)
[.c, .d] = dCP (V D CP — Washo per @cite{bochnak-hanink-2021})
[.c, .n, .d] = dnCP (V D N CP row — Adyghe)
[.c, .d, .p] = pdCP (V P D CP row — Bulgarian, Ndebele)

Equations

Instances For

def Typology.Complementation.bareCP :

CPShellInventory

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

Equations

Typology.Complementation.bareCP = [Typology.Complementation.CPShell.c]

Instances For

def Typology.Complementation.dCP :

CPShellInventory

The V D CP cell (Washo per @cite{bochnak-hanink-2021}).

Equations

Typology.Complementation.dCP = [Typology.Complementation.CPShell.c, Typology.Complementation.CPShell.d]

Instances For

def Typology.Complementation.dnCP :

CPShellInventory

The V D N CP cell (Adyghe REs per @cite{caponigro-polinsky-2011}).

Equations

Typology.Complementation.dnCP = [Typology.Complementation.CPShell.c, Typology.Complementation.CPShell.n, Typology.Complementation.CPShell.d]

Instances For

def Typology.Complementation.pdCP :

CPShellInventory

The V P D CP cell (Bulgarian REs per @cite{krapova-2010}; Ndebele per @cite{pietraszko-2019}).

Equations

Typology.Complementation.pdCP = [Typology.Complementation.CPShell.c, Typology.Complementation.CPShell.d, Typology.Complementation.CPShell.p]

Instances For

Concrete facts on the named witnesses #

The full implicational generalisations ("every attested inventory containing P also contains D") are folklore from inspection of the four named cells. We prove the consumed facts directly on the named shells; the universal claim is tracked in @cite{deal-2026} Table 79 commentary, not as a Lean theorem (general List.Mem reasoning over CPShellInventory would be substantial boilerplate without proportionate payoff).

theorem Typology.Complementation.named_shells_attested :

isAttestedShell bareCP = true ∧ isAttestedShell dCP = true ∧ isAttestedShell dnCP = true ∧ isAttestedShell pdCP = true

The four named witnesses are all attested (Deal 2026 Table 79).

theorem Typology.Complementation.pdCP_contains_p_and_d :

CPShell.p ∈ pdCP ∧ CPShell.d ∈ pdCP

The pdCP cell contains both P and D — the empirical generalisation that P-shelling co-occurs with D-shelling.

theorem Typology.Complementation.dnCP_contains_n_and_d :

CPShell.n ∈ dnCP ∧ CPShell.d ∈ dnCP

The dnCP cell contains both N and D — N appears only inside a D shell.

theorem Typology.Complementation.named_shells_contain_c :

CPShell.c ∈ bareCP ∧ CPShell.c ∈ dCP ∧ CPShell.c ∈ dnCP ∧ CPShell.c ∈ pdCP

Every named shell contains C (the CP itself).

theorem Typology.Complementation.pCP_not_attested :

isAttestedShell [CPShell.c, CPShell.p] = false

An unattested example: V P CP (P with no D shell) — @cite{deal-2026} Table 79 has no such cell.

theorem Typology.Complementation.nCP_not_attested :

isAttestedShell [CPShell.c, CPShell.n] = false

Another unattested example: V N CP (N with no D shell).