RelativizationProfile: per-language relativization typology

A WALS-style summary of a language's relativization system. Captures the two strategy dimensions (Chs 122/123), the relative-clause position with respect to the head noun, and the lowest position on the @cite{keenan-comrie-1977} Accessibility Hierarchy that can be relativized.

Per-language values live in Fragments/{Lang}/Relativization.lean as def relativization : RelativizationProfile. WALS-aggregate cross- linguistic findings live in Typology/Relativization/Basic.lean.

Layer placement

Located in Typology/ (not Core/) per the @cite{wals-2013}-aligned substrate convention: typological summary records that aggregate cross-linguistic data at the per-language level live alongside the other domain summaries (Typology/WordOrder.lean, Typology/Adposition.lean, Typology/Indefinite.lean, etc.). The lower-level relativization primitives (AHPosition, RCPosition, NPRelType, RelClauseMarker) remain in Core/Relativization/Basic.lean since they're framework- agnostic structural pieces, not typological summaries.

inductive Typology.Relativization.SubjRelStrategy : Type

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

• gap : SubjRelStrategy

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

• pronounRetention : SubjRelStrategy

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

• relativePronoun : SubjRelStrategy

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

• nonReduction : SubjRelStrategy

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

• mixed : SubjRelStrategy

  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 Typology.Relativization.instDecidableEqSubjRelStrategy : DecidableEq SubjRelStrategy

Equations

• Typology.Relativization.instDecidableEqSubjRelStrategy x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Typology.Relativization.instReprSubjRelStrategy.repr : SubjRelStrategy → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Typology.Relativization.instReprSubjRelStrategy : Repr SubjRelStrategy

Equations

• Typology.Relativization.instReprSubjRelStrategy = { reprPrec := Typology.Relativization.instReprSubjRelStrategy.repr }

inductive Typology.Relativization.OblRelStrategy : Type

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

• gap : OblRelStrategy

  Gap on obliques (often with preposition stranding).

• pronounRetention : OblRelStrategy

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

• relativePronoun : OblRelStrategy

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

• nonReduction : OblRelStrategy

  Head noun repeated inside the RC.

• mixed : OblRelStrategy

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

• notRelativizable : OblRelStrategy

  Obliques cannot be relativized at all in this language.

@[implicit_reducible]

instance Typology.Relativization.instDecidableEqOblRelStrategy : DecidableEq OblRelStrategy

Equations

• Typology.Relativization.instDecidableEqOblRelStrategy x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Typology.Relativization.instReprOblRelStrategy : Repr OblRelStrategy

Equations

• Typology.Relativization.instReprOblRelStrategy = { reprPrec := Typology.Relativization.instReprOblRelStrategy.repr }

def Typology.Relativization.instReprOblRelStrategy.repr : OblRelStrategy → Nat → Std.Format

Equations

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

inductive Typology.Relativization.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 Typology.Relativization.instDecidableEqInternallyHeadedStrategy : DecidableEq InternallyHeadedStrategy

Equations

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

@[implicit_reducible]

instance Typology.Relativization.instReprInternallyHeadedStrategy : Repr InternallyHeadedStrategy

Equations

• Typology.Relativization.instReprInternallyHeadedStrategy = { reprPrec := Typology.Relativization.instReprInternallyHeadedStrategy.repr }

def Typology.Relativization.instReprInternallyHeadedStrategy.repr : InternallyHeadedStrategy → Nat → Std.Format

Equations

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

structure Typology.Relativization.RelativizationProfile : Type

A language's relativization profile: WALS Chs 122/123 strategies plus RC position and AH cut-off.

• subjStrategy : SubjRelStrategy

  Strategy used for relativizing subjects (Ch 122).

• oblStrategy : OblRelStrategy

  Strategy used for relativizing obliques (Ch 123).

• rcPosition : Core.RCPosition

  Position of the relative clause with respect to the head noun.

• lowestRelativizable : Core.AHPosition

  Lowest @cite{keenan-comrie-1977} AH position that can be relativized.

• internallyHeaded : InternallyHeadedStrategy

  Status of the head-internal relativization strategy (WALS 90D). Defaults to .absent, since most languages outside East Asia, Mesoamerica, and a few isolates lack this construction.

• notes : String

  Free-text notes on the relativization system, including @cite{...} keys for hand-coded values.

def Typology.Relativization.instReprRelativizationProfile.repr : RelativizationProfile → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Typology.Relativization.instReprRelativizationProfile : Repr RelativizationProfile

Equations

• Typology.Relativization.instReprRelativizationProfile = { reprPrec := Typology.Relativization.instReprRelativizationProfile.repr }

@[implicit_reducible]

instance Typology.Relativization.instDecidableEqRelativizationProfile : DecidableEq RelativizationProfile

Equations

• Typology.Relativization.instDecidableEqRelativizationProfile = Typology.Relativization.instDecidableEqRelativizationProfile.decEq

def Typology.Relativization.instDecidableEqRelativizationProfile.decEq (x✝ x✝¹ : RelativizationProfile) : Decidable (x✝ = x✝¹)

Equations

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

def Typology.Relativization.fromWALS122A : Data.WALS.F122A.SubjectRelativization → SubjRelStrategy

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

Equations

• Typology.Relativization.fromWALS122A Data.WALS.F122A.SubjectRelativization.relativePronoun = Typology.Relativization.SubjRelStrategy.relativePronoun
• Typology.Relativization.fromWALS122A Data.WALS.F122A.SubjectRelativization.nonReduction = Typology.Relativization.SubjRelStrategy.nonReduction
• Typology.Relativization.fromWALS122A Data.WALS.F122A.SubjectRelativization.pronounRetention = Typology.Relativization.SubjRelStrategy.pronounRetention
• Typology.Relativization.fromWALS122A Data.WALS.F122A.SubjectRelativization.gap = Typology.Relativization.SubjRelStrategy.gap

def Typology.Relativization.fromWALS123A : Data.WALS.F123A.ObliqueRelativization → OblRelStrategy

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

Equations

• Typology.Relativization.fromWALS123A Data.WALS.F123A.ObliqueRelativization.relativePronoun = Typology.Relativization.OblRelStrategy.relativePronoun
• Typology.Relativization.fromWALS123A Data.WALS.F123A.ObliqueRelativization.nonReduction = Typology.Relativization.OblRelStrategy.nonReduction
• Typology.Relativization.fromWALS123A Data.WALS.F123A.ObliqueRelativization.pronounRetention = Typology.Relativization.OblRelStrategy.pronounRetention
• Typology.Relativization.fromWALS123A Data.WALS.F123A.ObliqueRelativization.gap = Typology.Relativization.OblRelStrategy.gap
• Typology.Relativization.fromWALS123A Data.WALS.F123A.ObliqueRelativization.notPossible = Typology.Relativization.OblRelStrategy.notRelativizable

def Typology.Relativization.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

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