Relativization: Basic Types

Theory-neutral types for cross-linguistic relativization data. These types are used by language fragments to encode relative clause markers and their distributional properties, and by phenomenon studies to verify typological generalizations like the @cite{keenan-comrie-1977} Accessibility Hierarchy.

Mirrors Core.Case.Basic / Core.Case.Hierarchy for case inventories.

inductive Core.AHPosition : Type

Grammatical positions on the @cite{keenan-comrie-1977} Accessibility Hierarchy (AH).

The hierarchy ranks grammatical relations by their accessibility to relativization. Higher positions are more accessible: more languages can relativize them, and simpler strategies (gap) suffice.

Subject > DirectObject > IndirectObject > Oblique > Genitive > ObjComparison

• subject : AHPosition

  Subject: the most accessible position. Virtually all languages with relative clauses can relativize subjects.

• directObject : AHPosition

  Direct object: the second most accessible position.

• indirectObject : AHPosition

  Indirect object: third position.

• oblique : AHPosition

  Oblique: fourth position (instrumentals, locatives, etc.).

• genitive : AHPosition

  Genitive: fifth position (possessors).

• objComparison : AHPosition

  Object of comparison: the least accessible position ("the person [that I am taller than _]").

@[implicit_reducible]

instance Core.instDecidableEqAHPosition : DecidableEq AHPosition

Equations

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

@[implicit_reducible]

instance Core.instReprAHPosition : Repr AHPosition

Equations

• Core.instReprAHPosition = { reprPrec := Core.instReprAHPosition.repr }

def Core.instReprAHPosition.repr : AHPosition → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Core.instReprAHPosition.repr Core.AHPosition.subject prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.AHPosition.subject")).group prec✝
• Core.instReprAHPosition.repr Core.AHPosition.directObject prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.AHPosition.directObject")).group prec✝
• Core.instReprAHPosition.repr Core.AHPosition.oblique prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.AHPosition.oblique")).group prec✝
• Core.instReprAHPosition.repr Core.AHPosition.genitive prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.AHPosition.genitive")).group prec✝

inductive Core.RCPosition : Type

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

Post-nominal is the dominant type cross-linguistically; pre-nominal correlates with OV word order; internally-headed and correlative (double-headed) types are rare but typologically significant.

• postNominal : RCPosition

  Post-nominal: RC follows the head noun. E.g., English "the man [who left]", Arabic "ar-rajul [alladhi ghadara]".

• preNominal : RCPosition

  Pre-nominal: RC precedes the head noun. E.g., Japanese "[ _ kaetta] hito", Korean "[ _ tteonagan] saram".

• internallyHeaded : RCPosition

  Internally-headed: the head noun appears inside the RC. E.g., Bambara.

• correlative : RCPosition

  Correlative (double-headed): the head noun appears both inside and outside the RC. E.g., Hindi-Urdu "jo aadmii aayaa, vo aadmii meraa bhaaii hai".

@[implicit_reducible]

instance Core.instDecidableEqRCPosition : DecidableEq RCPosition

Equations

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

def Core.instReprRCPosition.repr : RCPosition → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Core.instReprRCPosition.repr Core.RCPosition.postNominal prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.RCPosition.postNominal")).group prec✝
• Core.instReprRCPosition.repr Core.RCPosition.preNominal prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.RCPosition.preNominal")).group prec✝
• Core.instReprRCPosition.repr Core.RCPosition.correlative prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.RCPosition.correlative")).group prec✝

@[implicit_reducible]

instance Core.instReprRCPosition : Repr RCPosition

Equations

• Core.instReprRCPosition = { reprPrec := Core.instReprRCPosition.repr }

inductive Core.NPRelType : Type

What occupies the relativized position (NP_rel) inside the RC.

This is the core of @cite{keenan-comrie-1977}'s ±case distinction: -case strategies delete NP_rel (gap), while +case strategies retain a pronominal element that bears case marking.

• gap : NPRelType

  Gap: NP_rel is deleted; no overt element at the extraction site. The "lightest" strategy. E.g., English "the man [that _ left]".

• resumptive : NPRelType

  Resumptive pronoun: NP_rel is a personal pronoun (usually bearing case). E.g., Arabic "al-madina [illi saafartu ila-ha]" 'the-city [that I-traveled to-it]'.

• resumptiveMovement : NPRelType

  Movement resumptive: a lower copy of an Ā-movement chain that is partially pronounced rather than fully deleted. Featurally reduced relative to a bound resumptive (e.g., personless in Swahili). Diagnosed by parasitic gap constructions. @cite{scott-2021} @cite{sichel-2014}

• resumptiveBound : NPRelType

  Bound resumptive: a base-generated pronoun syntactically bound by the head of the relative clause. Not a movement copy — immune to chain reduction. Retains full person features. Diagnosed by obligatory presence inside adjunct islands. @cite{scott-2021} @cite{sichel-2014}

• relPronoun : NPRelType

  Relative pronoun: NP_rel is a dedicated relative pronoun that typically fronts to clause-initial position and bears case. E.g., English "the man [who left]", German "der Mann [der ging]".

• nonReduction : NPRelType

  Non-reduction: NP_rel is a full NP — the head noun is repeated inside the RC. E.g., Bambara.

@[implicit_reducible]

instance Core.instDecidableEqNPRelType : DecidableEq NPRelType

Equations

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

def Core.instReprNPRelType.repr : NPRelType → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Core.instReprNPRelType.repr Core.NPRelType.gap prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.NPRelType.gap")).group prec✝
• Core.instReprNPRelType.repr Core.NPRelType.resumptive prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.NPRelType.resumptive")).group prec✝
• Core.instReprNPRelType.repr Core.NPRelType.relPronoun prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.NPRelType.relPronoun")).group prec✝
• Core.instReprNPRelType.repr Core.NPRelType.nonReduction prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.NPRelType.nonReduction")).group prec✝

@[implicit_reducible]

instance Core.instReprNPRelType : Repr NPRelType

Equations

• Core.instReprNPRelType = { reprPrec := Core.instReprNPRelType.repr }

structure Core.RelClauseMarker : Type

A relative clause marker or construction in a language.

Each marker introduces one type of relative clause with specific distributional properties. Fragments encode the actual linguistic objects — particles, pronouns, verbal suffixes — rather than typological strategy labels. The strategy classification is derived from marker properties in study files.

Examples:

• Welsh particle a (gap, -case, covers SU/DO)
• Finnish relative pronoun joka (+case, covers SU–GEN)
• Korean adnominal suffix -(n)ɨn (gap, -case, covers SU–OBL)

• form : String

  Surface form of the marker (e.g., "a", "joka", "that/∅", "-(n)ɨn").

• npRel : NPRelType

  What occupies the relativized position in this construction.

• bearsCaseMarking : Bool

  Whether the relative element bears case marking (±case).

• rcPosition : RCPosition

  Position of the RC with respect to the head noun.

• positions : List AHPosition

  Which grammatical positions can be relativized using this marker.

• headDefiniteness : Option Features.Definiteness.Definiteness

  Which head-NP definiteness context attests the marker (purely descriptive). Reuses Features.Definiteness.Definiteness rather than introducing a parallel enum. none if the language doesn't make a comparable definiteness contrast on relative-clause markers (the typical case — keeps the 18 sibling Relativization Fragments unchanged) or if the data hasn't been encoded. Languages whose RC marker is attested in BOTH definite- and indefinite-headed contexts split into separate marker entries (one per context), so the field stays single-valued.

  The descriptive distinction is the one Arabic grammars draw (Wright 1896; Cantarino 1974; @cite{ryding-2005} §14.2 vs §14.3): MSA alladhī with definite antecedents vs Ø-relative-pronoun with indefinite antecedents. Substrate makes no claim about syntactic mechanism.

• notes : String

  Additional notes.

def Core.instBEqRelClauseMarker.beq : RelClauseMarker → RelClauseMarker → Bool

Equations

• One or more equations did not get rendered due to their size.
• Core.instBEqRelClauseMarker.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Core.instBEqRelClauseMarker : BEq RelClauseMarker

Equations

• Core.instBEqRelClauseMarker = { beq := Core.instBEqRelClauseMarker.beq }

def Core.instReprRelClauseMarker.repr : RelClauseMarker → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Core.instReprRelClauseMarker : Repr RelClauseMarker

Equations

• Core.instReprRelClauseMarker = { reprPrec := Core.instReprRelClauseMarker.repr }

def Core.RelClauseMarker.Covers (m : RelClauseMarker) (p : AHPosition) : Prop

Does this marker cover a given AH position?

Equations

• m.Covers p = (p ∈ m.positions)

@[implicit_reducible]

instance Core.instDecidableCovers (m : RelClauseMarker) (p : AHPosition) : Decidable (m.Covers p)

Equations

• Core.instDecidableCovers m p = id inferInstance

def Core.RelClauseMarker.covers (m : RelClauseMarker) (p : AHPosition) : Bool

Bool version of RelClauseMarker.Covers, retained as a transitional shim while the K&C study still consumes Bool-shaped per-position coverage in StrategyEntry. The Decidable instance above is the canonical truth-value witness; m.covers p = m.Covers p |> decide.

Equations

• m.covers p = decide (m.Covers p)

@[simp]

theorem Core.RelClauseMarker.covers_eq_decide (m : RelClauseMarker) (p : AHPosition) : m.covers p = decide (m.Covers p)

def Core.NPRelType.isMovementCopy : NPRelType → Option Bool

Whether a resumptive pronoun type is a movement copy, a bound pronoun, or unspecified. For languages where the two types coexist and are morphologically distinct (@cite{scott-2021} for Swahili, @cite{sichel-2014} for Hebrew).

Equations

• Core.NPRelType.resumptiveMovement.isMovementCopy = some true
• Core.NPRelType.resumptiveBound.isMovementCopy = some false
• Core.NPRelType.resumptive.isMovementCopy = none
• x✝.isMovementCopy = none