Relative clauses: structural core

Theory-neutral types for cross-linguistic relative-clause data: the [KC77] Accessibility Hierarchy, the relative-clause position relative to the head noun, what occupies the relativized position (NP_rel), and the Marker schema fragments instantiate. Fragments use these to encode relative-clause markers and their distributional properties; phenomenon studies use them to verify typological generalizations like the Accessibility Hierarchy. Mirrors Case for case inventories.

Main declarations

• RelativeClause.AHPosition — grammatical positions on the [KC77] Accessibility Hierarchy, with rank and the contiguousOnAH segment predicate (HC₂).
• RelativeClause.RCPosition — position of the relative clause with respect to the head noun (post-nominal, pre-nominal, internally-headed, correlative).
• RelativeClause.NPRelType — what occupies the relativized position (gap, resumptive, relative pronoun, …).
• RelativeClause.Realization — what one derivation realizes (AH position + NP_rel type); the framework-neutral hook a syntactic account projects to.
• RelativeClause.Marker — a relative-clause marker or construction, with the Covers / IsContinuous / IsPrimary predicates fragments and studies consume.

Implementation notes

The contiguity machinery (contiguousOnAH, AHPosition.rank) mirrors Core.validInventory for the case hierarchy ([Bla94b]); the contiguousOnAH : Bool kernel with a ContiguousOnAH : Prop wrapper is the load-bearing form for the decide-checked case analyses in Studies/KeenanComrie1977.lean. Coverage predicates (Covers, IsContinuous, IsPrimary) are stated as Prop with Decidable instances — no parallel Bool projections.

Grammatical positions on the Accessibility Hierarchy

inductive RelativeClause.AHPosition : Type

Grammatical positions on the [KC77] 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 RelativeClause.instDecidableEqAHPosition : DecidableEq AHPosition

Equations

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

@[implicit_reducible]

instance RelativeClause.instReprAHPosition : Repr AHPosition

Equations

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

def RelativeClause.instReprAHPosition.repr : AHPosition → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance RelativeClause.instFintypeAHPosition : Fintype AHPosition

Equations

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

def RelativeClause.AHPosition.rank : AHPosition → ℕ

Numeric rank of a position on the Accessibility Hierarchy. Higher rank = more accessible = more languages can relativize it.

Equations

• RelativeClause.AHPosition.subject.rank = 6
• RelativeClause.AHPosition.directObject.rank = 5
• RelativeClause.AHPosition.indirectObject.rank = 4
• RelativeClause.AHPosition.oblique.rank = 3
• RelativeClause.AHPosition.genitive.rank = 2
• RelativeClause.AHPosition.objComparison.rank = 1

@[implicit_reducible]

instance RelativeClause.instLinearOrderAHPosition : LinearOrder AHPosition

The accessibility order on AHPosition (the scale mixin): p₁ ≤ p₂ iff p₁ is no more accessible than p₂. Lets HC₂ continuity and the PRC be stated through mathlib's Set.OrdConnected / IsUpperSet rather than bespoke rank arithmetic.

Equations

• RelativeClause.instLinearOrderAHPosition = LinearOrder.lift' RelativeClause.AHPosition.rank RelativeClause.instLinearOrderAHPosition._proof_1

def RelativeClause.AHPosition.atLeastAsAccessible (p1 p2 : AHPosition) : Prop

Position p1 is at least as accessible as p2 on the hierarchy.

Equations

• p1.atLeastAsAccessible p2 = (p1.rank ≥ p2.rank)

@[implicit_reducible]

instance RelativeClause.instDecidableAtLeastAsAccessible (p1 p2 : AHPosition) : Decidable (p1.atLeastAsAccessible p2)

Equations

• RelativeClause.instDecidableAtLeastAsAccessible p1 p2 = RelativeClause.instDecidableAtLeastAsAccessible._aux_1 p1 p2

def RelativeClause.AHPosition.moreAccessible (p1 p2 : AHPosition) : Prop

Position p1 is strictly more accessible than p2.

Equations

• p1.moreAccessible p2 = (p1.rank > p2.rank)

@[implicit_reducible]

instance RelativeClause.instDecidableMoreAccessible (p1 p2 : AHPosition) : Decidable (p1.moreAccessible p2)

Equations

• RelativeClause.instDecidableMoreAccessible p1 p2 = RelativeClause.instDecidableMoreAccessible._aux_1 p1 p2

def RelativeClause.AHPosition.all : List AHPosition

All AH positions in descending order of accessibility.

Equations

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

Relative-clause position

inductive RelativeClause.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 RelativeClause.instDecidableEqRCPosition : DecidableEq RCPosition

Equations

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

def RelativeClause.instReprRCPosition.repr : RCPosition → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance RelativeClause.instReprRCPosition : Repr RCPosition

Equations

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

NP_rel type (what occupies the relativized position)

inductive RelativeClause.NPRelType : Type

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

This is the core of [KC77]'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. [Sco21]

• 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. [Sco21]

• 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 RelativeClause.instDecidableEqNPRelType : DecidableEq NPRelType

Equations

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

def RelativeClause.instReprNPRelType.repr : NPRelType → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance RelativeClause.instReprNPRelType : Repr NPRelType

Equations

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

inductive RelativeClause.ResumptiveKind : Type

The movement/base-generation status of a resumptive pronoun, for languages where the two coexist morphologically ([Sco21] for Swahili, [Sic14] for Hebrew).

• movementCopy : ResumptiveKind

  A partially-pronounced lower copy of an Ā-movement chain.

• bound : ResumptiveKind

  A base-generated pronoun bound by the relative-clause head.

• unspecified : ResumptiveKind

  A resumptive whose movement-vs-base-generation status is unspecified (pre-[Sco21] typology).

@[implicit_reducible]

instance RelativeClause.instDecidableEqResumptiveKind : DecidableEq ResumptiveKind

Equations

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

@[implicit_reducible]

instance RelativeClause.instReprResumptiveKind : Repr ResumptiveKind

Equations

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

def RelativeClause.instReprResumptiveKind.repr : ResumptiveKind → ℕ → Std.Format

Equations

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

def RelativeClause.NPRelType.resumptiveKind : NPRelType → Option ResumptiveKind

The resumptive kind of an NPRelType, or none for non-resumptive types. Refines the movement-vs-bound contrast; unlike a tri-state Option Bool, it keeps "unspecified resumptive" and "not a resumptive" as genuinely distinct outcomes.

Equations

• RelativeClause.NPRelType.resumptiveMovement.resumptiveKind = some RelativeClause.ResumptiveKind.movementCopy
• RelativeClause.NPRelType.resumptiveBound.resumptiveKind = some RelativeClause.ResumptiveKind.bound
• RelativeClause.NPRelType.resumptive.resumptiveKind = some RelativeClause.ResumptiveKind.unspecified
• x✝.resumptiveKind = none

Realization

structure RelativeClause.Realization : Type

What a single relative-clause derivation realizes, stated framework-neutrally: the relativized [KC77] AH position and the NP_rel type occupying it.

This is the hook by which a syntactic framework's derivation connects to the shared relativization substrate: HPSG's GAP/MOD derivation, Minimalism's trace + predicate-abstraction, etc. each project to a Realization, even though their derivation mechanisms are framework-specific and not unified. Distinct from the per-language WALS Profile (a typological survey of a language's strategies); a Realization describes one derivation.

• position : AHPosition

  The relativized position on the Accessibility Hierarchy.

• npRel : NPRelType

  What occupies the relativized position (gap, resumptive, …).

def RelativeClause.instDecidableEqRealization.decEq (x✝ x✝¹ : Realization) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance RelativeClause.instDecidableEqRealization : DecidableEq Realization

Equations

• RelativeClause.instDecidableEqRealization = RelativeClause.instDecidableEqRealization.decEq

def RelativeClause.instReprRealization.repr : Realization → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance RelativeClause.instReprRealization : Repr Realization

Equations

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

Relative-clause marker

structure RelativeClause.Marker : 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) 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; [Ryd05]): MSA alladhī with definite antecedents vs Ø-relative-pronoun with indefinite antecedents. Substrate makes no claim about syntactic mechanism.

• notes : String

  Additional notes.

def RelativeClause.instBEqMarker.beq : Marker → Marker → Bool

Equations

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

@[implicit_reducible]

instance RelativeClause.instBEqMarker : BEq Marker

Equations

• RelativeClause.instBEqMarker = { beq := RelativeClause.instBEqMarker.beq }

def RelativeClause.instReprMarker.repr : Marker → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance RelativeClause.instReprMarker : Repr Marker

Equations

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

def RelativeClause.Marker.Covers (m : Marker) (p : AHPosition) : Prop

Does this marker cover a given AH position?

Equations

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

@[implicit_reducible]

instance RelativeClause.instDecidableCovers (m : Marker) (p : AHPosition) : Decidable (m.Covers p)

Equations

• RelativeClause.instDecidableCovers m p = RelativeClause.instDecidableCovers._aux_1 m p

Accessibility-Hierarchy contiguity (HC₂)

def RelativeClause.hasAHRank (positions : List AHPosition) (r : ℕ) : Bool

Whether a list of AH positions contains at least one position at rank r.

Equations

• RelativeClause.hasAHRank positions r = positions.any fun (p : RelativeClause.AHPosition) => p.rank == r

def RelativeClause.contiguousOnAH (positions : List AHPosition) : Bool

A set of AH positions forms a contiguous segment on the hierarchy: for every pair of positions in the set, every intermediate rank is also represented.

Mirrors Core.validInventory for the case hierarchy ([Bla94b]).

This formalizes HC₂ of [KC77]: "Any RC-forming strategy must apply to a continuous segment of the AH."

Equations

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

def RelativeClause.ContiguousOnAH (positions : List AHPosition) : Prop

Prop wrapper around contiguousOnAH. The Bool-shaped definition is structural and load-bearing for the PRC general-proof case-analysis in Studies/KeenanComrie1977.lean; this Prop version is the canonical user-facing predicate.

Equations

• RelativeClause.ContiguousOnAH positions = (RelativeClause.contiguousOnAH positions = true)

@[implicit_reducible]

instance RelativeClause.instDecidableContiguousOnAH (positions : List AHPosition) : Decidable (ContiguousOnAH positions)

Equations

• RelativeClause.instDecidableContiguousOnAH positions = RelativeClause.instDecidableContiguousOnAH._aux_1 positions

def RelativeClause.Marker.IsContinuous (m : Marker) : Prop

A marker's positions form a contiguous segment of the AH.

Equations

• m.IsContinuous = RelativeClause.ContiguousOnAH m.positions

@[implicit_reducible]

instance RelativeClause.instDecidableIsContinuous (m : Marker) : Decidable m.IsContinuous

Equations

• RelativeClause.instDecidableIsContinuous m = RelativeClause.instDecidableIsContinuous._aux_1 m

def RelativeClause.Marker.IsPrimary (m : Marker) : Prop

A marker is primary in [KC77]'s sense if it can be used to relativize subjects. HC₁ requires every language to have at least one primary marker.

Equations

• m.IsPrimary = m.Covers RelativeClause.AHPosition.subject

@[implicit_reducible]

instance RelativeClause.instDecidableIsPrimary (m : Marker) : Decidable m.IsPrimary

Equations

• RelativeClause.instDecidableIsPrimary m = RelativeClause.instDecidableIsPrimary._aux_1 m

Ordering theorems

theorem RelativeClause.ah_rank_injective (a b : AHPosition) (h : a.rank = b.rank) : a = b

The hierarchy rank is injective — no two positions share a rank. Combined with the natural order on ℕ, this makes the AH a total order.

theorem RelativeClause.ah_rank_bounded (p : AHPosition) : 1 ≤ p.rank ∧ p.rank ≤ 6

All ranks are between 1 and 6.

theorem RelativeClause.ah_reflexive (p : AHPosition) : p.atLeastAsAccessible p

Accessibility is reflexive (follows from ≥ on ℕ).

theorem RelativeClause.ah_transitive (a b c : AHPosition) (h1 : a.atLeastAsAccessible b) (h2 : b.atLeastAsAccessible c) : a.atLeastAsAccessible c

Accessibility is transitive (follows from ≥ on ℕ).

Extraction bridge

Maps between Extraction.ExtractionTarget (5 structural positions from extraction morphology, in Typology/Extraction.lean) and AHPosition (6 positions on the [KC77] Accessibility Hierarchy). Both encode overlapping Ā-movement phenomena: extraction focuses on where extraction occurs (Mayan, Austronesian, Celtic Fragments); the AH focuses on what can be relativized. The bridge is partial: AHPosition.objComparison has no standard ExtractionTarget equivalent; ExtractionTarget.possessor maps to AHPosition.genitive.

def RelativeClause.extractionTargetToAH : Extraction.ExtractionTarget → AHPosition

Map an extraction target to its AH position. Possessor extraction corresponds to the genitive position on the AH.

Equations

• RelativeClause.extractionTargetToAH Extraction.ExtractionTarget.subject = RelativeClause.AHPosition.subject
• RelativeClause.extractionTargetToAH Extraction.ExtractionTarget.directObject = RelativeClause.AHPosition.directObject
• RelativeClause.extractionTargetToAH Extraction.ExtractionTarget.indirectObject = RelativeClause.AHPosition.indirectObject
• RelativeClause.extractionTargetToAH Extraction.ExtractionTarget.oblique = RelativeClause.AHPosition.oblique
• RelativeClause.extractionTargetToAH Extraction.ExtractionTarget.possessor = RelativeClause.AHPosition.genitive

def RelativeClause.ahToExtractionTarget : AHPosition → Option Extraction.ExtractionTarget

Map an AH position to an extraction target (partial: objComparison has no standard ExtractionTarget equivalent).

Equations

• RelativeClause.ahToExtractionTarget RelativeClause.AHPosition.subject = some Extraction.ExtractionTarget.subject
• RelativeClause.ahToExtractionTarget RelativeClause.AHPosition.directObject = some Extraction.ExtractionTarget.directObject
• RelativeClause.ahToExtractionTarget RelativeClause.AHPosition.indirectObject = some Extraction.ExtractionTarget.indirectObject
• RelativeClause.ahToExtractionTarget RelativeClause.AHPosition.oblique = some Extraction.ExtractionTarget.oblique
• RelativeClause.ahToExtractionTarget RelativeClause.AHPosition.genitive = some Extraction.ExtractionTarget.possessor
• RelativeClause.ahToExtractionTarget RelativeClause.AHPosition.objComparison = none

theorem RelativeClause.extraction_ah_roundtrip (t : Extraction.ExtractionTarget) : ahToExtractionTarget (extractionTargetToAH t) = some t

ExtractionTarget → AH → ExtractionTarget is the identity.

theorem RelativeClause.ah_extraction_roundtrip (p : AHPosition) (h : p ≠ AHPosition.objComparison) : ∃ (t : Extraction.ExtractionTarget), ahToExtractionTarget p = some t ∧ extractionTargetToAH t = p

AH → ExtractionTarget → AH is the identity for every position except objComparison (which has no ExtractionTarget).

theorem RelativeClause.objComparison_no_extraction_target : ahToExtractionTarget AHPosition.objComparison = none

objComparison is the only AH position without an ExtractionTarget.

theorem RelativeClause.non_ocomp_have_extraction_target (p : AHPosition) (h : p ≠ AHPosition.objComparison) : (ahToExtractionTarget p).isSome = true

Every non-objComparison AH position has an ExtractionTarget equivalent.