Relative clauses: typological survey (WALS)

[Com89] [KC77] [CK13c] [CK13b] [Dry13]

The cross-linguistic WALS-survey facet of the relative clause: relativization strategies (WALS Chs 122/123/90D), RC position, and the [KC77] Accessibility-Hierarchy cut-off, with the WALS converters and aggregate distribution theorems. Per-language values are bare defs in a Relativization namespace in Fragments/{Lang}/Relativization.lean.

Main declarations

• RelativeClause.SubjStrategy — subject relativization strategy (WALS Ch 122).
• RelativeClause.OblStrategy — oblique relativization strategy (WALS Ch 123), including the .notRelativizable value subjects structurally lack.
• RelativeClause.RCPosition, AHPosition — RC position and AH cut-off.
• RelativeClause.InternallyHeadedStrategy — status of the head-internal strategy (WALS Ch 90D).
• fromWALS122A / fromWALS123A / fromWALS90D — WALS raw-value converters.

Implementation notes

WALS Chs 122/123 do not distinguish a "mixed" category; .mixed profiles cannot be grounded against WALS via the converters. Subject relativization (Ch 122) has no "not possible" value — every language can relativize subjects (HC₁) — whereas oblique relativization (Ch 123) does, so OblStrategy carries .notRelativizable and SubjStrategy does not.

Subject relativization strategies (WALS Ch 122)

inductive RelativeClause.SubjStrategy : Type

WALS Ch 122: strategy used to relativize the subject position.

• gap : SubjStrategy

  The relativized position is empty. E.g., English "the man [that _ left]".

• pronounRetention : SubjStrategy

  A resumptive pronoun fills the position. E.g., dialectal Arabic.

• relativePronoun : SubjStrategy

  A dedicated wh-element / relative pronoun fills the position and typically fronts. E.g., German "der Mann [der ging]".

• nonReduction : SubjStrategy

  The head noun (or a full NP) is repeated inside the RC.

• mixed : SubjStrategy

  The language productively uses more than one of the above for subjects. WALS does not distinguish a "mixed" category; this is used only in our profiles.

@[implicit_reducible]

instance RelativeClause.instDecidableEqSubjStrategy : DecidableEq SubjStrategy

Equations

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

@[implicit_reducible]

instance RelativeClause.instReprSubjStrategy : Repr SubjStrategy

Equations

• RelativeClause.instReprSubjStrategy = { reprPrec := RelativeClause.instReprSubjStrategy.repr }

def RelativeClause.instReprSubjStrategy.repr : SubjStrategy → ℕ → Std.Format

Equations

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

Oblique relativization strategies (WALS Ch 123)

inductive RelativeClause.OblStrategy : Type

WALS Ch 123: strategy used to relativize oblique positions, or whether obliques can be relativized at all.

• gap : OblStrategy

  Gap on obliques (often with preposition stranding).

• pronounRetention : OblStrategy

  Resumptive pronoun on obliques (more common than for subjects).

• relativePronoun : OblStrategy

  Relative pronoun on obliques. E.g., English "in which", German "in der".

• nonReduction : OblStrategy

  Head noun repeated inside the RC.

• mixed : OblStrategy

  Multiple strategies productively used. WALS does not distinguish a "mixed" category; used only in our profiles.

• notRelativizable : OblStrategy

  Obliques cannot be relativized at all in this language.

@[implicit_reducible]

instance RelativeClause.instDecidableEqOblStrategy : DecidableEq OblStrategy

Equations

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

@[implicit_reducible]

instance RelativeClause.instReprOblStrategy : Repr OblStrategy

Equations

• RelativeClause.instReprOblStrategy = { reprPrec := RelativeClause.instReprOblStrategy.repr }

def RelativeClause.instReprOblStrategy.repr : OblStrategy → ℕ → Std.Format

Equations

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

Internally-headed strategy (WALS Ch 90D)

inductive RelativeClause.InternallyHeadedStrategy : Type

WALS Ch 90D: status of the internally-headed strategy in a language.

WALS distinguishes whether the internally-headed strategy is the dominant relativization pattern, co-dominant with another (RelN, NRel, correlative, double-headed), present as a non-dominant alternative, merely attested, or absent entirely.

• dominant : InternallyHeadedStrategy

  Internally-headed is the dominant strategy.

• coRelN : InternallyHeadedStrategy

  Co-dominant with a relative-noun construction.

• coNRel : InternallyHeadedStrategy

  Co-dominant with a noun-relative construction.

• coCorrelative : InternallyHeadedStrategy

  Co-dominant with a correlative construction.

• coDoubleHeaded : InternallyHeadedStrategy

  Co-dominant with a double-headed construction.

• nondominant : InternallyHeadedStrategy

  Present as a non-dominant alternative.

• attested : InternallyHeadedStrategy

  Attested but not dominant or co-dominant (WALS lumps this as "exists").

• absent : InternallyHeadedStrategy

  The internally-headed strategy is not attested in this language. WALS 90D codes only languages that have the strategy in some form, so this case is for hand-coded profiles whose Fragment asserts absence.

@[implicit_reducible]

instance RelativeClause.instDecidableEqInternallyHeadedStrategy : DecidableEq InternallyHeadedStrategy

Equations

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

def RelativeClause.instReprInternallyHeadedStrategy.repr : InternallyHeadedStrategy → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance RelativeClause.instReprInternallyHeadedStrategy : Repr InternallyHeadedStrategy

Equations

• RelativeClause.instReprInternallyHeadedStrategy = { reprPrec := RelativeClause.instReprInternallyHeadedStrategy.repr }

WALS converters (Chs 122, 123, 90D)

def RelativeClause.fromWALS122A : Data.WALS.F122A.SubjectRelativization → SubjStrategy

Convert a WALS 122A subject relativization value to SubjStrategy. WALS does not distinguish a "mixed" category, so languages whose profile is .mixed cannot be grounded against WALS via this converter alone.

Equations

• RelativeClause.fromWALS122A Data.WALS.F122A.SubjectRelativization.relativePronoun = RelativeClause.SubjStrategy.relativePronoun
• RelativeClause.fromWALS122A Data.WALS.F122A.SubjectRelativization.nonReduction = RelativeClause.SubjStrategy.nonReduction
• RelativeClause.fromWALS122A Data.WALS.F122A.SubjectRelativization.pronounRetention = RelativeClause.SubjStrategy.pronounRetention
• RelativeClause.fromWALS122A Data.WALS.F122A.SubjectRelativization.gap = RelativeClause.SubjStrategy.gap

def RelativeClause.fromWALS123A : Data.WALS.F123A.ObliqueRelativization → OblStrategy

Convert a WALS 123A oblique relativization value to OblStrategy. WALS .notPossible becomes .notRelativizable; .mixed profiles cannot be grounded against WALS via this converter.

Equations

• RelativeClause.fromWALS123A Data.WALS.F123A.ObliqueRelativization.relativePronoun = RelativeClause.OblStrategy.relativePronoun
• RelativeClause.fromWALS123A Data.WALS.F123A.ObliqueRelativization.nonReduction = RelativeClause.OblStrategy.nonReduction
• RelativeClause.fromWALS123A Data.WALS.F123A.ObliqueRelativization.pronounRetention = RelativeClause.OblStrategy.pronounRetention
• RelativeClause.fromWALS123A Data.WALS.F123A.ObliqueRelativization.gap = RelativeClause.OblStrategy.gap
• RelativeClause.fromWALS123A Data.WALS.F123A.ObliqueRelativization.notPossible = RelativeClause.OblStrategy.notRelativizable

def RelativeClause.fromWALS90D : Data.WALS.F90D.InternallyHeadedRelativeClauses → InternallyHeadedStrategy

Convert a WALS 90D internally-headed value to InternallyHeadedStrategy. WALS does not code an .absent case (the chapter only sampled languages that have the strategy), so absence is asserted by hand in the Fragment.

Equations

• RelativeClause.fromWALS90D Data.WALS.F90D.InternallyHeadedRelativeClauses.relativeClauseDominant = RelativeClause.InternallyHeadedStrategy.dominant
• RelativeClause.fromWALS90D Data.WALS.F90D.InternallyHeadedRelativeClauses.orReln = RelativeClause.InternallyHeadedStrategy.coRelN
• RelativeClause.fromWALS90D Data.WALS.F90D.InternallyHeadedRelativeClauses.orNrel = RelativeClause.InternallyHeadedStrategy.coNRel
• RelativeClause.fromWALS90D Data.WALS.F90D.InternallyHeadedRelativeClauses.orCorrelative = RelativeClause.InternallyHeadedStrategy.coCorrelative
• RelativeClause.fromWALS90D Data.WALS.F90D.InternallyHeadedRelativeClauses.orDoubleHeaded = RelativeClause.InternallyHeadedStrategy.coDoubleHeaded
• RelativeClause.fromWALS90D Data.WALS.F90D.InternallyHeadedRelativeClauses.occursAsNondominantType = RelativeClause.InternallyHeadedStrategy.nondominant
• RelativeClause.fromWALS90D Data.WALS.F90D.InternallyHeadedRelativeClauses.exists_ = RelativeClause.InternallyHeadedStrategy.attested

Distribution theorems

WALS-aggregate findings on relative-clause formation strategies ([CK13c] [CK13b] [Dry13]). Ch 122 (subjects): 166 languages; gap dominates, reflecting subjects' high accessibility on the [KC77] hierarchy. Ch 123 (obliques): 112 languages; gap remains most common, but pronoun retention is far more frequent than for subjects, and a sizeable minority cannot relativize obliques at all.

theorem RelativeClause.gap_most_common_for_subjects : (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F122A.SubjectRelativization) => x.value == Data.WALS.F122A.SubjectRelativization.gap) RelativeClause.ch122✝).length > (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F122A.SubjectRelativization) => x.value == Data.WALS.F122A.SubjectRelativization.nonReduction) RelativeClause.ch122✝).length ∧ (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F122A.SubjectRelativization) => x.value == Data.WALS.F122A.SubjectRelativization.nonReduction) RelativeClause.ch122✝).length > (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F122A.SubjectRelativization) => x.value == Data.WALS.F122A.SubjectRelativization.relativePronoun) RelativeClause.ch122✝).length ∧ (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F122A.SubjectRelativization) => x.value == Data.WALS.F122A.SubjectRelativization.relativePronoun) RelativeClause.ch122✝).length > (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F122A.SubjectRelativization) => x.value == Data.WALS.F122A.SubjectRelativization.pronounRetention) RelativeClause.ch122✝).length

WALS Ch 122: gap is the most common subject relativization strategy, followed by non-reduction, relative pronoun, and pronoun retention.

theorem RelativeClause.retention_increases_for_obliques : (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F123A.ObliqueRelativization) => x.value == Data.WALS.F123A.ObliqueRelativization.pronounRetention) RelativeClause.ch123✝).length > (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F122A.SubjectRelativization) => x.value == Data.WALS.F122A.SubjectRelativization.pronounRetention) RelativeClause.ch122✝).length

WALS Chs 122/123: pronoun retention is more common for obliques than for subjects — a key Accessibility-Hierarchy prediction ([KC77]).

theorem RelativeClause.obliques_sometimes_not_relativizable : (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F123A.ObliqueRelativization) => x.value == Data.WALS.F123A.ObliqueRelativization.notPossible) RelativeClause.ch123✝).length > 0

WALS Ch 123: some languages cannot relativize obliques at all, contrasting with subjects, where the Ch 122 enum has no "not possible" value.