From 02d5d740b82f174dad4b20cb14db3b640b945ea6 Mon Sep 17 00:00:00 2001 From: Robert Hawkins Date: Sat, 30 May 2026 17:45:29 -0700 Subject: [PATCH] refactor(Typology): unify relativization substrate into RelativeClause --- Linglib.lean | 7 +- Linglib/Core/Relativization/Basic.lean | 182 --------- Linglib/Core/Relativization/Hierarchy.lean | 138 ------- .../Arabic/ModernStandard/Relativization.lean | 18 +- Linglib/Fragments/Bambara/Relativization.lean | 6 +- Linglib/Fragments/English/Relativization.lean | 14 +- Linglib/Fragments/Finnish/Relativization.lean | 14 +- Linglib/Fragments/French/Relativization.lean | 6 +- Linglib/Fragments/German/Relativization.lean | 6 +- Linglib/Fragments/Hebrew/Relativization.lean | 20 +- .../Fragments/HindiUrdu/Relativization.lean | 6 +- .../Fragments/Japanese/Relativization.lean | 6 +- Linglib/Fragments/Korean/Relativization.lean | 14 +- .../Fragments/Malagasy/Relativization.lean | 12 +- .../Fragments/Mandarin/Relativization.lean | 6 +- .../Fragments/Mayan/Mam/Relativization.lean | 6 +- Linglib/Fragments/Navajo/Relativization.lean | 6 +- .../Slavic/Russian/Relativization.lean | 6 +- Linglib/Fragments/Swahili/Relativization.lean | 16 +- Linglib/Fragments/Tagalog/Relativization.lean | 6 +- .../Fragments/TobaBatak/Relativization.lean | 14 +- Linglib/Fragments/Turkish/Relativization.lean | 6 +- Linglib/Fragments/Welsh/Relativization.lean | 14 +- Linglib/Fragments/Yoruba/Relativization.lean | 20 +- Linglib/Studies/Comrie1989.lean | 10 +- Linglib/Studies/Erlewine2018.lean | 10 +- Linglib/Studies/KeenanComrie1977.lean | 70 ++-- Linglib/Studies/Landau2026.lean | 10 +- Linglib/Studies/Scott2021.lean | 2 +- Linglib/Syntax/HPSG/Core/RelativeClauses.lean | 6 +- Linglib/Typology/Extraction.lean | 4 +- Linglib/Typology/RelativeClause/Basic.lean | 347 ++++++++++++++++++ .../Defs.lean => RelativeClause/WALS.lean} | 150 +++++--- Linglib/Typology/Relativization/Basic.lean | 87 ----- .../Relativization/ExtractionBridge.lean | 85 ----- 35 files changed, 609 insertions(+), 721 deletions(-) delete mode 100644 Linglib/Core/Relativization/Basic.lean delete mode 100644 Linglib/Core/Relativization/Hierarchy.lean create mode 100644 Linglib/Typology/RelativeClause/Basic.lean rename Linglib/Typology/{Relativization/Defs.lean => RelativeClause/WALS.lean} (51%) delete mode 100644 Linglib/Typology/Relativization/Basic.lean delete mode 100644 Linglib/Typology/Relativization/ExtractionBridge.lean diff --git a/Linglib.lean b/Linglib.lean index 6afde3385..d39ad9d7b 100644 --- a/Linglib.lean +++ b/Linglib.lean @@ -285,9 +285,8 @@ import Linglib.Morphology.DegreeContainment import Linglib.Morphology.DM.DomainLocality import Linglib.Morphology.Case.Allomorphy import Linglib.Morphology.DM.ContainmentVI -import Linglib.Core.Relativization.Basic -import Linglib.Typology.Relativization.ExtractionBridge -import Linglib.Core.Relativization.Hierarchy +import Linglib.Typology.RelativeClause.Basic +import Linglib.Typology.RelativeClause.WALS import Linglib.Typology.ClassifierSystem import Linglib.Core.Scales.Roundness import Linglib.Core.Scales.Predicate @@ -1340,8 +1339,6 @@ import Linglib.Studies.Merchant2013 import Linglib.Phenomena.Entailment.Basic import Linglib.Phenomena.Entailment.Monotonicity import Linglib.Phenomena.WordOrder.CrossSerial -import Linglib.Typology.Relativization.Defs -import Linglib.Typology.Relativization.Basic import Linglib.Phenomena.Focus.Basic import Linglib.Studies.KratzerSelkirk2020 import Linglib.Studies.Roberts2012 diff --git a/Linglib/Core/Relativization/Basic.lean b/Linglib/Core/Relativization/Basic.lean deleted file mode 100644 index bed81fb26..000000000 --- a/Linglib/Core/Relativization/Basic.lean +++ /dev/null @@ -1,182 +0,0 @@ -import Linglib.Features.Definiteness - -/-! -# 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 `Features.Case` for case inventories. --/ - -namespace Core - --- ============================================================================ --- § 1: Grammatical Positions on the Accessibility Hierarchy --- ============================================================================ - -/-- 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 -/ -inductive AHPosition where - /-- Subject: the most accessible position. Virtually all languages - with relative clauses can relativize subjects. -/ - | subject - /-- Direct object: the second most accessible position. -/ - | directObject - /-- Indirect object: third position. -/ - | indirectObject - /-- Oblique: fourth position (instrumentals, locatives, etc.). -/ - | oblique - /-- Genitive: fifth position (possessors). -/ - | genitive - /-- Object of comparison: the least accessible position - ("the person [that I am taller than _]"). -/ - | objComparison - deriving DecidableEq, Repr - --- ============================================================================ --- § 2: Relative Clause Position --- ============================================================================ - -/-- 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. -/ -inductive RCPosition where - /-- Post-nominal: RC follows the head noun. E.g., English "the man - [who left]", Arabic "ar-rajul [alladhi ghadara]". -/ - | postNominal - /-- Pre-nominal: RC precedes the head noun. E.g., Japanese - "[ _ kaetta] hito", Korean "[ _ tteonagan] saram". -/ - | preNominal - /-- Internally-headed: the head noun appears inside the RC. E.g., - Bambara. -/ - | internallyHeaded - /-- 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". -/ - | correlative - deriving DecidableEq, Repr - --- ============================================================================ --- § 3: NP_rel Type (what occupies the relativized position) --- ============================================================================ - -/-- 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. -/ -inductive NPRelType where - /-- Gap: NP_rel is deleted; no overt element at the extraction site. - The "lightest" strategy. E.g., English "the man [that _ left]". -/ - | gap - /-- 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]'. -/ - | resumptive - /-- 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} -/ - | resumptiveMovement - /-- 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} -/ - | resumptiveBound - /-- 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]". -/ - | relPronoun - /-- Non-reduction: NP_rel is a full NP — the head noun is repeated - inside the RC. E.g., Bambara. -/ - | nonReduction - deriving DecidableEq, Repr - --- ============================================================================ --- § 4: Relative Clause Marker --- ============================================================================ - -/-- 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) -/ -structure RelClauseMarker where - /-- Surface form of the marker (e.g., "a", "joka", "that/∅", "-(n)ɨn"). -/ - form : String - /-- What occupies the relativized position in this construction. -/ - npRel : NPRelType - /-- Whether the relative element bears case marking (±case). -/ - bearsCaseMarking : Bool - /-- Position of the RC with respect to the head noun. -/ - rcPosition : RCPosition - /-- Which grammatical positions can be relativized using this marker. -/ - positions : List AHPosition - /-- 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. -/ - headDefiniteness : Option Features.Definiteness.Definiteness := none - /-- Additional notes. -/ - notes : String := "" - deriving BEq, Repr - -/-- Does this marker cover a given AH position? -/ -def RelClauseMarker.Covers (m : RelClauseMarker) (p : AHPosition) : Prop := - p ∈ m.positions - -instance (m : RelClauseMarker) (p : AHPosition) : Decidable (m.Covers p) := by - unfold RelClauseMarker.Covers; infer_instance - -/-- 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`. -/ -def RelClauseMarker.covers (m : RelClauseMarker) (p : AHPosition) : Bool := - decide (m.Covers p) - -@[simp] theorem RelClauseMarker.covers_eq_decide (m : RelClauseMarker) (p : AHPosition) : - m.covers p = decide (m.Covers p) := rfl - -/-- 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). -/ -def NPRelType.isMovementCopy : NPRelType → Option Bool - | .resumptiveMovement => some true - | .resumptiveBound => some false - | .resumptive => none -- unspecified (pre-Scott typology) - | _ => none -- non-resumptive - -end Core diff --git a/Linglib/Core/Relativization/Hierarchy.lean b/Linglib/Core/Relativization/Hierarchy.lean deleted file mode 100644 index 5dea40e57..000000000 --- a/Linglib/Core/Relativization/Hierarchy.lean +++ /dev/null @@ -1,138 +0,0 @@ -import Linglib.Core.Relativization.Basic - -/-! -# Accessibility Hierarchy: Ordering and Contiguity -@cite{keenan-comrie-1977} - -Defines the rank function and contiguity predicate for the Accessibility -Hierarchy. Mirrors `Features.Case` for Blake's case hierarchy. --/ - -namespace Core - --- ============================================================================ --- § 1: Rank --- ============================================================================ - -/-- Numeric rank of a position on the Accessibility Hierarchy. - Higher rank = more accessible = more languages can relativize it. -/ -def AHPosition.rank : AHPosition → Nat - | .subject => 6 - | .directObject => 5 - | .indirectObject => 4 - | .oblique => 3 - | .genitive => 2 - | .objComparison => 1 - -/-- Position p1 is at least as accessible as p2 on the hierarchy. -/ -def AHPosition.atLeastAsAccessible (p1 p2 : AHPosition) : Prop := - p1.rank ≥ p2.rank - -instance (p1 p2 : AHPosition) : Decidable (p1.atLeastAsAccessible p2) := - inferInstanceAs (Decidable (_ ≥ _)) - -/-- Position p1 is strictly more accessible than p2. -/ -def AHPosition.moreAccessible (p1 p2 : AHPosition) : Prop := - p1.rank > p2.rank - -instance (p1 p2 : AHPosition) : Decidable (p1.moreAccessible p2) := - inferInstanceAs (Decidable (_ > _)) - -/-- All AH positions in descending order of accessibility. -/ -def AHPosition.all : List AHPosition := - [.subject, .directObject, .indirectObject, .oblique, .genitive, .objComparison] - --- ============================================================================ --- § 2: Contiguity Predicate --- ============================================================================ - -/-- Whether a list of AH positions contains at least one position at rank r. -/ -def hasAHRank (positions : List AHPosition) (r : Nat) : Bool := - positions.any fun p => p.rank == r - -/-- 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 (@cite{blake-1994}). - - This formalizes HC₂ of @cite{keenan-comrie-1977}: "Any RC-forming - strategy must apply to a continuous segment of the AH." -/ -def contiguousOnAH (positions : List AHPosition) : Bool := - positions.all fun p1 => - positions.all fun p2 => - if p2.rank > p1.rank then - let lo := p1.rank - let hi := p2.rank - List.range hi |>.all fun r => - if r > lo && r < hi then hasAHRank positions r - else true - else true - -/-- 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. -/ -def ContiguousOnAH (positions : List AHPosition) : Prop := - contiguousOnAH positions = true - -instance (positions : List AHPosition) : Decidable (ContiguousOnAH positions) := - inferInstanceAs (Decidable (_ = _)) - -/-- A marker's positions form a contiguous segment of the AH. -/ -def RelClauseMarker.IsContinuous (m : RelClauseMarker) : Prop := - ContiguousOnAH m.positions - -instance (m : RelClauseMarker) : Decidable m.IsContinuous := - inferInstanceAs (Decidable (ContiguousOnAH _)) - -/-- A marker is **primary** (in K&C 1977's sense, p. 67-68) if it can be - used to relativize subjects. HC₁ requires every language to have at - least one primary marker. -/ -def RelClauseMarker.IsPrimary (m : RelClauseMarker) : Prop := - m.Covers .subject - -instance (m : RelClauseMarker) : Decidable m.IsPrimary := - inferInstanceAs (Decidable (m.Covers .subject)) - -/-- Bool version of `IsPrimary`, retained as a transitional shim for - Bool-list equality theorems (`(markers.map (·.isPrimary)) = [true, ...]`). -/ -def RelClauseMarker.isPrimary (m : RelClauseMarker) : Bool := - m.covers .subject - -/-- Bool version of `RelClauseMarker.IsContinuous`, retained as a - transitional shim while `StrategyEntry` (slated for deletion in the - K&C study refactor) still consumes Bool-shaped contiguity. -/ -def RelClauseMarker.isContinuous (m : RelClauseMarker) : Bool := - contiguousOnAH m.positions - -@[simp] theorem RelClauseMarker.isContinuous_eq (m : RelClauseMarker) : - m.isContinuous = contiguousOnAH m.positions := rfl - --- ============================================================================ --- § 3: Ordering Theorems --- ============================================================================ - -/-- 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 ah_rank_injective (a b : AHPosition) (h : a.rank = b.rank) : a = b := by - cases a <;> cases b <;> simp_all [AHPosition.rank] - -/-- All ranks are between 1 and 6. -/ -theorem ah_rank_bounded (p : AHPosition) : 1 ≤ p.rank ∧ p.rank ≤ 6 := by - cases p <;> simp [AHPosition.rank] - -/-- Accessibility is reflexive (follows from `≥` on ℕ). -/ -theorem ah_reflexive (p : AHPosition) : p.atLeastAsAccessible p := by - simp [AHPosition.atLeastAsAccessible] - -/-- Accessibility is transitive (follows from `≥` on ℕ). -/ -theorem ah_transitive (a b c : AHPosition) - (h1 : a.atLeastAsAccessible b) (h2 : b.atLeastAsAccessible c) : - a.atLeastAsAccessible c := by - simp [AHPosition.atLeastAsAccessible] at *; omega - -/-! The K&C-anchored contiguity examples and the Primary Relativization -Constraint general proof live in `Studies/KeenanComrie1977.lean`. -/ - -end Core diff --git a/Linglib/Fragments/Arabic/ModernStandard/Relativization.lean b/Linglib/Fragments/Arabic/ModernStandard/Relativization.lean index 1604488d4..4473c00cb 100644 --- a/Linglib/Fragments/Arabic/ModernStandard/Relativization.lean +++ b/Linglib/Fragments/Arabic/ModernStandard/Relativization.lean @@ -1,5 +1,5 @@ -import Linglib.Core.Relativization.Basic -import Linglib.Typology.Relativization.Defs +import Linglib.Typology.RelativeClause.Basic +import Linglib.Typology.RelativeClause.WALS /-! # Modern Standard Arabic Relativization Fragment @@ -35,7 +35,7 @@ already mixed; a future split into `Fragments/StandardArabic/` and namespace Fragments.Arabic.ModernStandard -open Core +open RelativeClause /-- Relative pronoun *alladhī* (masc.sg.) / *allatii* (fem.sg.) — head of a nine-form paradigm marked for number/gender (and, in the dual, case); @@ -47,7 +47,7 @@ open Core E.g., "hiya llatii ʾarsalat-i l-duktuur-a" 'she is the one who sent the doctor' (Ryding §14.2). -/ -def relAlladhi : RelClauseMarker := +def relAlladhi : Marker := { form := "alladhī/allatii" , npRel := .gap , bearsCaseMarking := false @@ -68,7 +68,7 @@ def relAlladhi : RelClauseMarker := E.g., "al-kitaab-u alladhii qaraʾ-naa-hu" 'the book that we read (it)' (Ryding §14.4). -/ -def relResumptive : RelClauseMarker := +def relResumptive : Marker := { form := "alladhī/allatii + resumptive" , npRel := .resumptive , bearsCaseMarking := true @@ -86,7 +86,7 @@ def relResumptive : RelClauseMarker := E.g., "fii ziyaarat-in li-dimashq-a ta-staghriq-u ʾusbuuʿ-an" 'on a visit to Damascus [which] lasts a week' (Ryding §14.3). -/ -def relAsyndeticGap : RelClauseMarker := +def relAsyndeticGap : Marker := { form := "∅" , npRel := .gap , bearsCaseMarking := false @@ -113,7 +113,7 @@ def relAsyndeticGap : RelClauseMarker := E.g., "wa-qaal-a fii muʾtamar-in SiHaafiyy-in ʿaqad-a-hu ʾams-i" 'he said in a press conference [which] he held (it) yesterday' (Ryding §14.4.2). -/ -def relAsyndeticResumptive : RelClauseMarker := +def relAsyndeticResumptive : Marker := { form := "∅ + resumptive" , npRel := .resumptive , bearsCaseMarking := true @@ -130,7 +130,7 @@ def relAsyndeticResumptive : RelClauseMarker := indefinite-headed pair (`relAsyndeticGap`, `relAsyndeticResumptive`). The free relatives *maa* / *man* of §14.5 are a separate construction (no head NP) and are not included. -/ -def relMarkers : List RelClauseMarker := +def relMarkers : List Marker := [relAlladhi, relResumptive, relAsyndeticGap, relAsyndeticResumptive] /-- Arabic relativization profile (WALS-style summary). @@ -147,7 +147,7 @@ def relMarkers : List RelClauseMarker := `arabic_kc_covers_deeper_than_wals` in `Studies/KeenanComrie1977.lean` documents the systematic K&C-vs-WALS asymmetry. -/ -def relativization : Typology.Relativization.RelativizationProfile := +def relativization : RelativeClause.Profile := { subjStrategy := .gap , oblStrategy := .pronounRetention , rcPosition := .postNominal diff --git a/Linglib/Fragments/Bambara/Relativization.lean b/Linglib/Fragments/Bambara/Relativization.lean index 4dd02a441..07ade508e 100644 --- a/Linglib/Fragments/Bambara/Relativization.lean +++ b/Linglib/Fragments/Bambara/Relativization.lean @@ -1,9 +1,9 @@ -import Linglib.Typology.Relativization.Defs +import Linglib.Typology.RelativeClause.WALS /-! # Bambara relativization profile -Typological-summary `RelativizationProfile` for Bambara (ISO `bam`). +Typological-summary `RelativeClause.Profile` for Bambara (ISO `bam`). -/ namespace Fragments.Bambara @@ -11,7 +11,7 @@ namespace Fragments.Bambara /-- Bambara relativization: internally-headed RC; non-reduction strategy; relativization limited to subject and direct object on AH; obliques not relativizable. -/ -def relativization : Typology.Relativization.RelativizationProfile := +def relativization : RelativeClause.Profile := { subjStrategy := .nonReduction , oblStrategy := .notRelativizable , rcPosition := .internallyHeaded diff --git a/Linglib/Fragments/English/Relativization.lean b/Linglib/Fragments/English/Relativization.lean index 6762e51f8..ddc95333e 100644 --- a/Linglib/Fragments/English/Relativization.lean +++ b/Linglib/Fragments/English/Relativization.lean @@ -1,5 +1,5 @@ -import Linglib.Core.Relativization.Basic -import Linglib.Typology.Relativization.Defs +import Linglib.Typology.RelativeClause.Basic +import Linglib.Typology.RelativeClause.WALS /-! # English Relativization Fragment @@ -14,12 +14,12 @@ Data from @cite{keenan-comrie-1977} Table 1. namespace Fragments.English -open Core +open RelativeClause /-- Complementizer *that* or zero (∅). NP_rel is deleted (gap). Covers subject and direct object relativization. E.g., "the man [that _ left]", "the book [∅ I read _]". -/ -def relThat : RelClauseMarker := +def relThat : Marker := { form := "that/∅" , npRel := .gap , bearsCaseMarking := false @@ -32,7 +32,7 @@ def relThat : RelClauseMarker := Covers IO–OCOMP via pied-piping. E.g., "the man [to whom I gave the book]", "the man [whose book I read _]". -/ -def relWhom : RelClauseMarker := +def relWhom : Marker := { form := "who/whom/which/whose" , npRel := .relPronoun , bearsCaseMarking := true @@ -41,10 +41,10 @@ def relWhom : RelClauseMarker := , notes := "Relative pronoun with case (who/whom/whose); pied-piping" } /-- All English relative clause markers. -/ -def relMarkers : List RelClauseMarker := [relThat, relWhom] +def relMarkers : List Marker := [relThat, relWhom] /-- English relativization profile (typological summary). -/ -def relativization : Typology.Relativization.RelativizationProfile := +def relativization : RelativeClause.Profile := { subjStrategy := .mixed , oblStrategy := .mixed , rcPosition := .postNominal diff --git a/Linglib/Fragments/Finnish/Relativization.lean b/Linglib/Fragments/Finnish/Relativization.lean index f3081f293..13692b1c5 100644 --- a/Linglib/Fragments/Finnish/Relativization.lean +++ b/Linglib/Fragments/Finnish/Relativization.lean @@ -1,5 +1,5 @@ -import Linglib.Core.Relativization.Basic -import Linglib.Typology.Relativization.Defs +import Linglib.Typology.RelativeClause.Basic +import Linglib.Typology.RelativeClause.WALS /-! # Finnish Relativization Fragment @@ -18,14 +18,14 @@ Data from @cite{keenan-comrie-1977} Table 1. namespace Fragments.Finnish -open Core +open RelativeClause /-- Relative pronoun *joka*. Declines for case (agreeing with the role inside the RC). Postnominal RC. Covers SU–GEN. OCOMP does not exist as a distinct category in Finnish. E.g., "mies [joka lähti]" 'man [who left]', "kaupunki [jossa asuin]" 'city [where I-lived]'. -/ -def relJoka : RelClauseMarker := +def relJoka : Marker := { form := "joka" , npRel := .relPronoun , bearsCaseMarking := true @@ -36,7 +36,7 @@ def relJoka : RelClauseMarker := /-- Participial construction. Prenominal RC formed with a participle. NP_rel is a gap. Covers SU and DO only. E.g., "[ _ lähtenyt] mies" '[ _ left] man'. -/ -def relParticipial : RelClauseMarker := +def relParticipial : Marker := { form := "participle" , npRel := .gap , bearsCaseMarking := false @@ -45,10 +45,10 @@ def relParticipial : RelClauseMarker := , notes := "Participial; prenominal; covers SU/DO only" } /-- All Finnish relative clause markers. -/ -def relMarkers : List RelClauseMarker := [relJoka, relParticipial] +def relMarkers : List Marker := [relJoka, relParticipial] /-- Finnish relativization profile (typological summary). -/ -def relativization : Typology.Relativization.RelativizationProfile := +def relativization : RelativeClause.Profile := { subjStrategy := .relativePronoun , oblStrategy := .relativePronoun , rcPosition := .postNominal diff --git a/Linglib/Fragments/French/Relativization.lean b/Linglib/Fragments/French/Relativization.lean index 2f37c1bc6..7731e19d0 100644 --- a/Linglib/Fragments/French/Relativization.lean +++ b/Linglib/Fragments/French/Relativization.lean @@ -1,16 +1,16 @@ -import Linglib.Typology.Relativization.Defs +import Linglib.Typology.RelativeClause.WALS /-! # French relativization profile -Typological-summary `RelativizationProfile` for French (ISO `fra`). +Typological-summary `RelativeClause.Profile` for French (ISO `fra`). -/ namespace Fragments.French /-- French relativization: relative pronoun system *qui* (SU), *que* (DO), *dont* (GEN), *lequel* (OBL); covers all AH positions; postnominal RC. -/ -def relativization : Typology.Relativization.RelativizationProfile := +def relativization : RelativeClause.Profile := { subjStrategy := .relativePronoun , oblStrategy := .relativePronoun , rcPosition := .postNominal diff --git a/Linglib/Fragments/German/Relativization.lean b/Linglib/Fragments/German/Relativization.lean index 7a7604c17..b964bdfe8 100644 --- a/Linglib/Fragments/German/Relativization.lean +++ b/Linglib/Fragments/German/Relativization.lean @@ -1,9 +1,9 @@ -import Linglib.Typology.Relativization.Defs +import Linglib.Typology.RelativeClause.WALS /-! # German relativization profile -Typological-summary `RelativizationProfile` for German (ISO `deu`). +Typological-summary `RelativeClause.Profile` for German (ISO `deu`). -/ namespace Fragments.German @@ -11,7 +11,7 @@ namespace Fragments.German /-- German relativization: relative pronoun *der/die/das* on both subjects and obliques; postnominal RC; all AH positions relativizable. -/ -def relativization : Typology.Relativization.RelativizationProfile := +def relativization : RelativeClause.Profile := { subjStrategy := .relativePronoun , oblStrategy := .relativePronoun , rcPosition := .postNominal diff --git a/Linglib/Fragments/Hebrew/Relativization.lean b/Linglib/Fragments/Hebrew/Relativization.lean index 6f3bda123..c8d91ed07 100644 --- a/Linglib/Fragments/Hebrew/Relativization.lean +++ b/Linglib/Fragments/Hebrew/Relativization.lean @@ -1,5 +1,5 @@ -import Linglib.Core.Relativization.Basic -import Linglib.Typology.Relativization.Defs +import Linglib.Typology.RelativeClause.Basic +import Linglib.Typology.RelativeClause.WALS /-! # Hebrew Relativization Fragment @@ -31,12 +31,12 @@ Data from @cite{keenan-comrie-1977} Table 1 and §1.3.2. namespace Fragments.Hebrew -open Core +open RelativeClause /-- Complementizer *she-*. NP_rel is deleted (gap). Covers subject and direct object. E.g., "ha-ish [she-halakh _]" 'the-man [that-left _]'. -/ -def relSheGap : RelClauseMarker := +def relSheGap : Marker := { form := "she-" , npRel := .gap , bearsCaseMarking := false @@ -48,7 +48,7 @@ def relSheGap : RelClauseMarker := introduces the RC, but NP_rel is a resumptive personal pronoun. Covers DO–OCOMP (DO shared with gap construction). E.g., "ha-ir [she-garti ba-h]" 'the-city [that-lived-I in-it]'. -/ -def relSheResumptive : RelClauseMarker := +def relSheResumptive : Marker := { form := "she- + pronoun" , npRel := .resumptive , bearsCaseMarking := true @@ -61,7 +61,7 @@ def relSheResumptive : RelClauseMarker := reconstruction effects, indicating movement copy. @cite{sichel-2014}: "ha-ec she-hu tipes alav" 'the tree that he climbed on.it' — idiomatic reading preserved = reconstruction. -/ -def relSheMovementResumptive : RelClauseMarker := +def relSheMovementResumptive : Marker := { form := "she- + movement RP" , npRel := .resumptiveMovement , bearsCaseMarking := true @@ -74,7 +74,7 @@ def relSheMovementResumptive : RelClauseMarker := pronoun (no reconstruction, weak crossover sensitivity). @cite{sichel-2014}: "ze ha-yeled she-imo šelo ohevet oto" 'this is the boy who his mother loves him' — oto is bound. -/ -def relSheBoundResumptive : RelClauseMarker := +def relSheBoundResumptive : Marker := { form := "she- + bound RP" , npRel := .resumptiveBound , bearsCaseMarking := true @@ -86,14 +86,14 @@ def relSheBoundResumptive : RelClauseMarker := marker is retained for backward compatibility with @cite{keenan-comrie-1977}-level typology. The Sichel markers provide finer-grained two-type classification. -/ -def relMarkers : List RelClauseMarker := [relSheGap, relSheResumptive] +def relMarkers : List Marker := [relSheGap, relSheResumptive] /-- Sichel-refined markers distinguishing bound vs. movement resumption. -/ -def relMarkersSichel : List RelClauseMarker := +def relMarkersSichel : List Marker := [relSheGap, relSheBoundResumptive, relSheMovementResumptive] /-- Hebrew relativization profile (typological summary). -/ -def relativization : Typology.Relativization.RelativizationProfile := +def relativization : RelativeClause.Profile := { subjStrategy := .gap , oblStrategy := .pronounRetention , rcPosition := .postNominal diff --git a/Linglib/Fragments/HindiUrdu/Relativization.lean b/Linglib/Fragments/HindiUrdu/Relativization.lean index 588a89c0a..5cb5083f9 100644 --- a/Linglib/Fragments/HindiUrdu/Relativization.lean +++ b/Linglib/Fragments/HindiUrdu/Relativization.lean @@ -1,9 +1,9 @@ -import Linglib.Typology.Relativization.Defs +import Linglib.Typology.RelativeClause.WALS /-! # Hindi/Urdu relativization profile -Typological-summary `RelativizationProfile` for Hindi (ISO `hin`). +Typological-summary `RelativeClause.Profile` for Hindi (ISO `hin`). -/ namespace Fragments.HindiUrdu @@ -11,7 +11,7 @@ namespace Fragments.HindiUrdu /-- Hindi/Urdu relativization: correlative *jo...vo*; declining relative pronoun *jo*; correlative position; postnominal RC also possible in formal register. -/ -def relativization : Typology.Relativization.RelativizationProfile := +def relativization : RelativeClause.Profile := { subjStrategy := .relativePronoun , oblStrategy := .relativePronoun , rcPosition := .correlative diff --git a/Linglib/Fragments/Japanese/Relativization.lean b/Linglib/Fragments/Japanese/Relativization.lean index ff015dc99..540f8f1a7 100644 --- a/Linglib/Fragments/Japanese/Relativization.lean +++ b/Linglib/Fragments/Japanese/Relativization.lean @@ -1,16 +1,16 @@ -import Linglib.Typology.Relativization.Defs +import Linglib.Typology.RelativeClause.WALS /-! # Japanese relativization profile -Typological-summary `RelativizationProfile` for Japanese (ISO `jpn`). +Typological-summary `RelativeClause.Profile` for Japanese (ISO `jpn`). -/ namespace Fragments.Japanese /-- Japanese relativization: gap throughout; pre-nominal RC; no relative pronoun; genitive position relativizable but rare. -/ -def relativization : Typology.Relativization.RelativizationProfile := +def relativization : RelativeClause.Profile := { subjStrategy := .gap , oblStrategy := .gap , rcPosition := .preNominal diff --git a/Linglib/Fragments/Korean/Relativization.lean b/Linglib/Fragments/Korean/Relativization.lean index 1f8d42a67..7d8ad60f4 100644 --- a/Linglib/Fragments/Korean/Relativization.lean +++ b/Linglib/Fragments/Korean/Relativization.lean @@ -1,5 +1,5 @@ -import Linglib.Core.Relativization.Basic -import Linglib.Typology.Relativization.Defs +import Linglib.Typology.RelativeClause.Basic +import Linglib.Typology.RelativeClause.WALS /-! # Korean Relativization Fragment @@ -18,14 +18,14 @@ Data from @cite{keenan-comrie-1977} Table 1. namespace Fragments.Korean -open Core +open RelativeClause /-- Adnominal verb suffix. The verb takes an adnominal (relative) form: *-(n)ɨn* (present), *-n* (past), *-l* (prospective/future). No relative pronoun or complementizer. NP_rel + case marker deleted. Prenominal RC. Covers SU, DO, IO, OBL. E.g., "[ _ tteonagan] saram" '[ _ left] person'. -/ -def relAdnominal : RelClauseMarker := +def relAdnominal : Marker := { form := "-(n)ɨn, -n, -l" , npRel := .gap , bearsCaseMarking := false @@ -36,7 +36,7 @@ def relAdnominal : RelClauseMarker := /-- Genitive construction. The possessor position is relativized using the genitive marker *-uy*. Prenominal RC. Covers GEN only. -/ -def relGenitive : RelClauseMarker := +def relGenitive : Marker := { form := "-uy" , npRel := .gap , bearsCaseMarking := true @@ -45,10 +45,10 @@ def relGenitive : RelClauseMarker := , notes := "Genitive marker; covers GEN only" } /-- All Korean relative clause markers. -/ -def relMarkers : List RelClauseMarker := [relAdnominal, relGenitive] +def relMarkers : List Marker := [relAdnominal, relGenitive] /-- Korean relativization profile (typological summary). -/ -def relativization : Typology.Relativization.RelativizationProfile := +def relativization : RelativeClause.Profile := { subjStrategy := .gap , oblStrategy := .gap , rcPosition := .preNominal diff --git a/Linglib/Fragments/Malagasy/Relativization.lean b/Linglib/Fragments/Malagasy/Relativization.lean index 5c604f55b..802afb8da 100644 --- a/Linglib/Fragments/Malagasy/Relativization.lean +++ b/Linglib/Fragments/Malagasy/Relativization.lean @@ -1,5 +1,5 @@ -import Linglib.Core.Relativization.Basic -import Linglib.Typology.Relativization.Defs +import Linglib.Typology.RelativeClause.Basic +import Linglib.Typology.RelativeClause.WALS /-! # Malagasy Relativization Fragment @@ -18,12 +18,12 @@ Data from @cite{keenan-comrie-1977} Table 1. namespace Fragments.Malagasy -open Core +open RelativeClause /-- Gap construction. Postnominal RC. Only the pivot (subject) can be relativized. Voice alternation required for underlying non-subjects. E.g., "ny lehilahy [izay nandao _]" 'the man [that left _]'. -/ -def relGap : RelClauseMarker := +def relGap : Marker := { form := "izay/∅" , npRel := .gap , bearsCaseMarking := false @@ -32,10 +32,10 @@ def relGap : RelClauseMarker := , notes := "Only pivot (subject) relativizable; voice alternation for non-SU" } /-- All Malagasy relative clause markers. -/ -def relMarkers : List RelClauseMarker := [relGap] +def relMarkers : List Marker := [relGap] /-- Malagasy relativization profile (typological summary). -/ -def relativization : Typology.Relativization.RelativizationProfile := +def relativization : RelativeClause.Profile := { subjStrategy := .gap , oblStrategy := .notRelativizable , rcPosition := .postNominal diff --git a/Linglib/Fragments/Mandarin/Relativization.lean b/Linglib/Fragments/Mandarin/Relativization.lean index a5f4098a6..8c94e39fd 100644 --- a/Linglib/Fragments/Mandarin/Relativization.lean +++ b/Linglib/Fragments/Mandarin/Relativization.lean @@ -1,16 +1,16 @@ -import Linglib.Typology.Relativization.Defs +import Linglib.Typology.RelativeClause.WALS /-! # Mandarin relativization profile -Typological-summary `RelativizationProfile` for Mandarin (ISO `cmn`). +Typological-summary `RelativeClause.Profile` for Mandarin (ISO `cmn`). -/ namespace Fragments.Mandarin /-- Mandarin relativization: gap + relativizer *de*; pre-nominal RC (SVO main clause but RC-N order). -/ -def relativization : Typology.Relativization.RelativizationProfile := +def relativization : RelativeClause.Profile := { subjStrategy := .gap , oblStrategy := .gap , rcPosition := .preNominal diff --git a/Linglib/Fragments/Mayan/Mam/Relativization.lean b/Linglib/Fragments/Mayan/Mam/Relativization.lean index 5cc36f9d6..b6c6f34ff 100644 --- a/Linglib/Fragments/Mayan/Mam/Relativization.lean +++ b/Linglib/Fragments/Mayan/Mam/Relativization.lean @@ -1,17 +1,17 @@ -import Linglib.Typology.Relativization.Defs +import Linglib.Typology.RelativeClause.WALS /-! # Mam relativization profile @cite{elkins-torrence-brown-2026} -Typological-summary `RelativizationProfile` for Mam (ISO `mam`). +Typological-summary `RelativeClause.Profile` for Mam (ISO `mam`). -/ namespace Fragments.Mayan.Mam /-- Mam relativization: gap on subjects (with Agent Focus morphology); *=(y)a'* clitic marks oblique extraction; postnominal RC; Mayan. -/ -def relativization : Typology.Relativization.RelativizationProfile := +def relativization : RelativeClause.Profile := { subjStrategy := .gap , oblStrategy := .gap , rcPosition := .postNominal diff --git a/Linglib/Fragments/Navajo/Relativization.lean b/Linglib/Fragments/Navajo/Relativization.lean index e0d7c64db..c45cf5dc4 100644 --- a/Linglib/Fragments/Navajo/Relativization.lean +++ b/Linglib/Fragments/Navajo/Relativization.lean @@ -1,16 +1,16 @@ -import Linglib.Typology.Relativization.Defs +import Linglib.Typology.RelativeClause.WALS /-! # Navajo relativization profile -Typological-summary `RelativizationProfile` for Navajo (ISO `nav`). +Typological-summary `RelativeClause.Profile` for Navajo (ISO `nav`). -/ namespace Fragments.Navajo /-- Navajo relativization: gap on subject and direct object; limited relativization on lower AH positions; pre-nominal RC; SOV. -/ -def relativization : Typology.Relativization.RelativizationProfile := +def relativization : RelativeClause.Profile := { subjStrategy := .gap , oblStrategy := .notRelativizable , rcPosition := .preNominal diff --git a/Linglib/Fragments/Slavic/Russian/Relativization.lean b/Linglib/Fragments/Slavic/Russian/Relativization.lean index c287715c2..f0075879a 100644 --- a/Linglib/Fragments/Slavic/Russian/Relativization.lean +++ b/Linglib/Fragments/Slavic/Russian/Relativization.lean @@ -1,16 +1,16 @@ -import Linglib.Typology.Relativization.Defs +import Linglib.Typology.RelativeClause.WALS /-! # Russian relativization profile -Typological-summary `RelativizationProfile` for Russian (ISO `rus`). +Typological-summary `RelativeClause.Profile` for Russian (ISO `rus`). -/ namespace Fragments.Slavic.Russian /-- Russian relativization: declining relative pronoun *kotoryj*; all AH positions; postnominal RC. -/ -def relativization : Typology.Relativization.RelativizationProfile := +def relativization : RelativeClause.Profile := { subjStrategy := .relativePronoun , oblStrategy := .relativePronoun , rcPosition := .postNominal diff --git a/Linglib/Fragments/Swahili/Relativization.lean b/Linglib/Fragments/Swahili/Relativization.lean index 0a73a0302..3e2c21a1d 100644 --- a/Linglib/Fragments/Swahili/Relativization.lean +++ b/Linglib/Fragments/Swahili/Relativization.lean @@ -1,5 +1,5 @@ -import Linglib.Core.Relativization.Basic -import Linglib.Typology.Relativization.Defs +import Linglib.Typology.RelativeClause.Basic +import Linglib.Typology.RelativeClause.WALS import Linglib.Fragments.Swahili.Basic /-! @@ -59,7 +59,7 @@ rather than nesting them under a sub-namespace. namespace Fragments.Swahili -open Core +open RelativeClause -- ============================================================================ -- § 1: Amba-RC Markers @@ -68,7 +68,7 @@ open Core /-- The *amba*-complementizer with gap (subject and direct object extraction). Subject and object agreement are obligatory on the verb; no resumptive pronoun appears. -/ -def ambaGap : RelClauseMarker := +def ambaGap : Marker := { form := "amba" , npRel := .gap , bearsCaseMarking := false @@ -80,7 +80,7 @@ def ambaGap : RelClauseMarker := (person-matching). Objects of monosyllabic prepositions inside adjunct islands obligatorily surface with person features. @cite{scott-2021} examples (31)–(33). -/ -def ambaBound : RelClauseMarker := +def ambaBound : Marker := { form := "amba + bound RP" , npRel := .resumptiveBound , bearsCaseMarking := true @@ -92,7 +92,7 @@ def ambaBound : RelClauseMarker := (personless). Objects of monosyllabic prepositions in parasitic gap constructions surface without person features. @cite{scott-2021} examples (36)–(37). -/ -def ambaMovement : RelClauseMarker := +def ambaMovement : Marker := { form := "amba + movement RP" , npRel := .resumptiveMovement , bearsCaseMarking := true @@ -101,10 +101,10 @@ def ambaMovement : RelClauseMarker := , notes := "amba-RC; movement resumptive (personless); in parasitic gaps" } /-- All Swahili relative clause markers. -/ -def relMarkers : List RelClauseMarker := [ambaGap, ambaBound, ambaMovement] +def relMarkers : List Marker := [ambaGap, ambaBound, ambaMovement] /-- Swahili relativization profile (typological summary). -/ -def relativization : Typology.Relativization.RelativizationProfile := +def relativization : RelativeClause.Profile := { subjStrategy := .gap , oblStrategy := .pronounRetention , rcPosition := .postNominal diff --git a/Linglib/Fragments/Tagalog/Relativization.lean b/Linglib/Fragments/Tagalog/Relativization.lean index 0cf55c9cc..6617af301 100644 --- a/Linglib/Fragments/Tagalog/Relativization.lean +++ b/Linglib/Fragments/Tagalog/Relativization.lean @@ -1,9 +1,9 @@ -import Linglib.Typology.Relativization.Defs +import Linglib.Typology.RelativeClause.WALS /-! # Tagalog relativization profile -Typological-summary `RelativizationProfile` for Tagalog (ISO `tgl`). +Typological-summary `RelativeClause.Profile` for Tagalog (ISO `tgl`). -/ namespace Fragments.Tagalog @@ -11,7 +11,7 @@ namespace Fragments.Tagalog /-- Tagalog relativization: gap on subjects (*ang*-phrase only); voice alternation required for non-subject relativization; linker *na/ng*; obliques not directly relativizable. -/ -def relativization : Typology.Relativization.RelativizationProfile := +def relativization : RelativeClause.Profile := { subjStrategy := .gap , oblStrategy := .notRelativizable , rcPosition := .postNominal diff --git a/Linglib/Fragments/TobaBatak/Relativization.lean b/Linglib/Fragments/TobaBatak/Relativization.lean index 88678e06e..c17858360 100644 --- a/Linglib/Fragments/TobaBatak/Relativization.lean +++ b/Linglib/Fragments/TobaBatak/Relativization.lean @@ -1,5 +1,5 @@ -import Linglib.Core.Relativization.Basic -import Linglib.Typology.Relativization.Defs +import Linglib.Typology.RelativeClause.Basic +import Linglib.Typology.RelativeClause.WALS /-! # Toba Batak Relativization Fragment @@ -17,12 +17,12 @@ Data from @cite{keenan-comrie-1977} Table 1 and §1.3.2. namespace Fragments.TobaBatak -open Core +open RelativeClause /-- Gap construction. NP_rel is deleted. Postnominal RC. Covers subject only. The -case strategy is maximally restricted (like Arabic). -/ -def relGap : RelClauseMarker := +def relGap : Marker := { form := "∅" , npRel := .gap , bearsCaseMarking := false @@ -34,7 +34,7 @@ def relGap : RelClauseMarker := bearing case. Postnominal RC. Covers IO, OBL, GEN. Crucially does NOT cover DO — neither strategy can relativize direct objects in Toba Batak. -/ -def relResumptive : RelClauseMarker := +def relResumptive : Marker := { form := "pronoun" , npRel := .resumptive , bearsCaseMarking := true @@ -43,13 +43,13 @@ def relResumptive : RelClauseMarker := , notes := "Resumptive; IO/OBL/GEN; DO gap genuine; §1.3.2" } /-- All Toba Batak relative clause markers. -/ -def relMarkers : List RelClauseMarker := [relGap, relResumptive] +def relMarkers : List Marker := [relGap, relResumptive] /-- Toba Batak relativization profile (typological summary). The `subjStrategy = .gap` + `oblStrategy = .pronounRetention` pair is K&C's canonical "DO-gap-with-resumptive-elsewhere" datapoint; DO is a genuine gap in AH coverage (neither strategy can relativize it). -/ -def relativization : Typology.Relativization.RelativizationProfile := +def relativization : RelativeClause.Profile := { subjStrategy := .gap , oblStrategy := .pronounRetention , rcPosition := .postNominal diff --git a/Linglib/Fragments/Turkish/Relativization.lean b/Linglib/Fragments/Turkish/Relativization.lean index 424ea98e2..84d2e5244 100644 --- a/Linglib/Fragments/Turkish/Relativization.lean +++ b/Linglib/Fragments/Turkish/Relativization.lean @@ -1,16 +1,16 @@ -import Linglib.Typology.Relativization.Defs +import Linglib.Typology.RelativeClause.WALS /-! # Turkish relativization profile -Typological-summary `RelativizationProfile` for Turkish (ISO `tur`). +Typological-summary `RelativeClause.Profile` for Turkish (ISO `tur`). -/ namespace Fragments.Turkish /-- Turkish relativization: gap throughout; participial suffixes *-en* (SU) and *-dik* (non-SU); pre-nominal RC. -/ -def relativization : Typology.Relativization.RelativizationProfile := +def relativization : RelativeClause.Profile := { subjStrategy := .gap , oblStrategy := .gap , rcPosition := .preNominal diff --git a/Linglib/Fragments/Welsh/Relativization.lean b/Linglib/Fragments/Welsh/Relativization.lean index 6f3648bd9..ace5fddbc 100644 --- a/Linglib/Fragments/Welsh/Relativization.lean +++ b/Linglib/Fragments/Welsh/Relativization.lean @@ -1,5 +1,5 @@ -import Linglib.Core.Relativization.Basic -import Linglib.Typology.Relativization.Defs +import Linglib.Typology.RelativeClause.Basic +import Linglib.Typology.RelativeClause.WALS /-! # Welsh Relativization Fragment @@ -14,12 +14,12 @@ Data from @cite{keenan-comrie-1977} Table 1 and §1.3.2. namespace Fragments.Welsh -open Core +open RelativeClause /-- Relative particle *a*. Introduces postnominal RCs with gap in NP_rel. Covers subject and direct object. E.g., "Y dyn [a adawodd _]" 'the man [PRT left _]'. -/ -def relParticleA : RelClauseMarker := +def relParticleA : Marker := { form := "a" , npRel := .gap , bearsCaseMarking := false @@ -32,7 +32,7 @@ def relParticleA : RelClauseMarker := Covers IO–OCOMP. E.g., "Y dyn [y rhoddais i'r llyfr iddo]" 'the man [PRT I-gave the book to-him]'. -/ -def relParticleY : RelClauseMarker := +def relParticleY : Marker := { form := "y" , npRel := .resumptive , bearsCaseMarking := true @@ -41,10 +41,10 @@ def relParticleY : RelClauseMarker := , notes := "Relative particle; resumptive pronoun in NP_rel; §1.3.2" } /-- All Welsh relative clause markers. -/ -def relMarkers : List RelClauseMarker := [relParticleA, relParticleY] +def relMarkers : List Marker := [relParticleA, relParticleY] /-- Welsh relativization profile (typological summary). -/ -def relativization : Typology.Relativization.RelativizationProfile := +def relativization : RelativeClause.Profile := { subjStrategy := .gap , oblStrategy := .pronounRetention , rcPosition := .postNominal diff --git a/Linglib/Fragments/Yoruba/Relativization.lean b/Linglib/Fragments/Yoruba/Relativization.lean index f8f65e27f..a94c9f3a6 100644 --- a/Linglib/Fragments/Yoruba/Relativization.lean +++ b/Linglib/Fragments/Yoruba/Relativization.lean @@ -1,5 +1,5 @@ -import Linglib.Core.Relativization.Basic -import Linglib.Typology.Relativization.Defs +import Linglib.Typology.RelativeClause.Basic +import Linglib.Typology.RelativeClause.WALS /-! # Yoruba Relativization Fragment @@ -36,7 +36,7 @@ ex. 125–128. namespace Fragments.Yoruba -open Core +open RelativeClause /-- §6.19: Subject relativization. The relativized subject is replaced by the high-tone third-person singular pronoun `ó`. @@ -44,7 +44,7 @@ open Core `bearsCaseMarking := false` per @cite{keenan-comrie-1979}'s analysis of `ó` as verb agreement (K&C 1977 Table 1 p. 79 codes Yoruba's SU-strategy as -case). -/ -def relTiSubject : RelClauseMarker := +def relTiSubject : Marker := { form := "tí + ó" , npRel := .resumptive , bearsCaseMarking := false @@ -59,7 +59,7 @@ def relTiSubject : RelClauseMarker := /-- §6.20: Direct object relativization. The relativized object is dropped completely (gap strategy). E.g. `Ọkùnrin tí mo rí` 'the man I saw'. -/ -def relTiObject : RelClauseMarker := +def relTiObject : Marker := { form := "tí + ∅" , npRel := .gap , bearsCaseMarking := false @@ -75,10 +75,10 @@ def relTiObject : RelClauseMarker := object completely (gap, §6.21); the preposition `ní` triggers complex restructuring (drop + repositioning, with `tí` insertion for place nouns and exceptions for `wà`/`gbé`, §6.22). The single-cell - `RelClauseMarker.npRel` cannot encode the split, so we record the + `Marker.npRel` cannot encode the split, so we record the dominant pattern (`gap`) and document the `ní` case in `notes`. E.g. `Ọbẹ tí mo fi gé e` 'the knife I cut it with'. -/ -def relTiOblique : RelClauseMarker := +def relTiOblique : Marker := { form := "tí + ∅ (5 preps); tí + restructuring (ní)" , npRel := .gap , bearsCaseMarking := false @@ -101,7 +101,7 @@ def relTiOblique : RelClauseMarker := +case, GEN=+). The genitive-form pronouns `rẹ̀`/`wọn` are morphologically distinct from subject `ó` and object `i`/`un`/`ó`, so per Awobuluyi §2.21's polymorphic-noun classification they encode their case role lexically. -/ -def relTiGenitive : RelClauseMarker := +def relTiGenitive : Marker := { form := "tí + rẹ̀/wọn" , npRel := .resumptive , bearsCaseMarking := true @@ -117,11 +117,11 @@ def relTiGenitive : RelClauseMarker := /-- All Yoruba relative clause markers, anchored to @cite{awobuluyi-1978} §6.19–6.23 + @cite{keenan-comrie-1979} ex. 125–128. All four share the introducer `tí` (high tone, §6.18). -/ -def relMarkers : List RelClauseMarker := +def relMarkers : List Marker := [relTiSubject, relTiObject, relTiOblique, relTiGenitive] /-- Yoruba relativization profile (typological summary). -/ -def relativization : Typology.Relativization.RelativizationProfile := +def relativization : RelativeClause.Profile := { subjStrategy := .pronounRetention , oblStrategy := .gap , rcPosition := .postNominal diff --git a/Linglib/Studies/Comrie1989.lean b/Linglib/Studies/Comrie1989.lean index 774d480c0..2fe543135 100644 --- a/Linglib/Studies/Comrie1989.lean +++ b/Linglib/Studies/Comrie1989.lean @@ -1,5 +1,5 @@ import Linglib.Features.Prominence -import Linglib.Core.Relativization.Hierarchy +import Linglib.Typology.RelativeClause.Basic import Linglib.Phenomena.Subjecthood.SubjectProperties import Linglib.Semantics.Causation.Morphological import Linglib.Typology.Alignment @@ -30,7 +30,7 @@ grammatical domains: Same `AnimacyLevel` type governs the split threshold. - **Relativization** (Ch 7): The @cite{keenan-comrie-1977} Accessibility Hierarchy orders grammatical relations by extraction accessibility - (`Core.Relativization.Hierarchy`, `FillerGap.Studies.KeenanComrie1977`). + (`Typology.RelativeClause.Basic`, `FillerGap.Studies.KeenanComrie1977`). The AH positions (Subject > DO > IO > OBL) mirror the GR hierarchy that governs causee demotion. - **Causatives** (Ch 8): Morphological complexity correlates with semantic @@ -52,7 +52,7 @@ in accusative languages and diverge under ergativity. Formalized in Relativization typology is formalized in `KeenanComrie1977` and -`Core.Relativization.Hierarchy`. The AH concerns accessibility to +`Typology.RelativeClause.Basic`. The AH concerns accessibility to extraction — a filler-gap dependency — which is why the study file lives under `FillerGap/`. Non-extraction relative clause types (correlatives, internally-headed RCs) fall outside the AH's scope: @@ -280,7 +280,7 @@ theorem intransitive_causee_above_transitive_causee : -- § 5: The Accessibility Hierarchy as a GR Hierarchy -- ============================================================================ -open Core (AHPosition) +open RelativeClause (AHPosition) /-- The top of the AH is the subject position — @cite{comrie-1989} Ch 7: "A language must be able to relativize subjects" (HC₁). The subject @@ -316,7 +316,7 @@ accessibility (Ch 7): Subject > Direct Object > Indirect Object > Oblique `CauseeSlot` (in `Semantics.Causation.Morphological`) and -`AHPosition` (in `Core.Relativization.Hierarchy`) encode overlapping +`AHPosition` (in `Typology.RelativeClause.Basic`) encode overlapping portions of this hierarchy independently. The bridge function `causeeToAH` maps causee slots to their corresponding AH positions, and the order-preservation theorem proves the mapping is monotone — diff --git a/Linglib/Studies/Erlewine2018.lean b/Linglib/Studies/Erlewine2018.lean index 3d0294db8..2793cb925 100644 --- a/Linglib/Studies/Erlewine2018.lean +++ b/Linglib/Studies/Erlewine2018.lean @@ -1,7 +1,7 @@ import Linglib.Syntax.Minimalist.HeadFunction import Linglib.Fragments.TobaBatak.Basic import Linglib.Fragments.TobaBatak.Relativization -import Linglib.Typology.Relativization.ExtractionBridge +import Linglib.Typology.RelativeClause.Basic import Linglib.Syntax.Minimalist.Position import Linglib.Syntax.Minimalist.Derivation import Linglib.Syntax.Minimalist.Movement.Remnant @@ -198,8 +198,8 @@ theorem profile_matches_data : position that is covered by some Toba Batak relativization marker. -/ theorem extractable_positions_are_relativizable : tbExtractionProfile.markedPositions.all (λ et => - let ahPos := Typology.Relativization.extractionTargetToAH et - relMarkers.any (·.covers ahPos)) = true := by + let ahPos := RelativeClause.extractionTargetToAH et + relMarkers.any (fun m => decide (m.Covers ahPos))) = true := by decide /-- Full chain (all three links as a single conjunction). -/ @@ -213,8 +213,8 @@ theorem extraction_profile_relativization_chain : (tbExtractionProfile.Marks .subject) ∧ -- Link 3: every marked position is relativizable via AH (tbExtractionProfile.markedPositions.all (λ et => - let ahPos := Typology.Relativization.extractionTargetToAH et - relMarkers.any (·.covers ahPos))) := by + let ahPos := RelativeClause.extractionTargetToAH et + relMarkers.any (fun m => decide (m.Covers ahPos)))) := by decide -- ============================================================================ diff --git a/Linglib/Studies/KeenanComrie1977.lean b/Linglib/Studies/KeenanComrie1977.lean index 51f392e76..f5f1e7f57 100644 --- a/Linglib/Studies/KeenanComrie1977.lean +++ b/Linglib/Studies/KeenanComrie1977.lean @@ -1,4 +1,4 @@ -import Linglib.Core.Relativization.Hierarchy +import Linglib.Typology.RelativeClause.Basic import Linglib.Fragments.English.Relativization import Linglib.Fragments.Welsh.Relativization import Linglib.Fragments.Arabic.ModernStandard.Relativization @@ -21,11 +21,11 @@ verified against a subset of the paper's Table 1 data (pp. 76-79). ## Architecture This file derives K&C's typological theorems **directly from** -`Fragments.{Lang}.relMarkers : List RelClauseMarker`, the per-language +`Fragments.{Lang}.relMarkers : List Marker`, the per-language data layer encoding actual linguistic markers (particles, pronouns, verbal suffixes). No intermediate `KCProfile`/`StrategyEntry` schema — -predicates and aggregations are stated over `List RelClauseMarker` -directly, projecting through `RelClauseMarker.{positions, +predicates and aggregations are stated over `List Marker` +directly, projecting through `Marker.{positions, bearsCaseMarking, rcPosition}` as needed. The Fragment files cite @cite{keenan-comrie-1979} (the per-language @@ -70,24 +70,24 @@ with serial-verb-mediated obliques (Yoruba). namespace KeenanComrie1977 -open Core +open RelativeClause -- ============================================================================ --- § 1: Predicates over List RelClauseMarker +-- § 1: Predicates over List Marker -- ============================================================================ /-- HC₁: a language can relativize subjects iff some marker covers SU. -/ -def SatisfiesHC1 (markers : List RelClauseMarker) : Prop := +def SatisfiesHC1 (markers : List Marker) : Prop := ∃ m ∈ markers, m.Covers .subject -instance (markers : List RelClauseMarker) : Decidable (SatisfiesHC1 markers) := by +instance (markers : List Marker) : Decidable (SatisfiesHC1 markers) := by unfold SatisfiesHC1; infer_instance /-- HC₂: every marker covers a contiguous segment of the AH. -/ -def SatisfiesHC2 (markers : List RelClauseMarker) : Prop := +def SatisfiesHC2 (markers : List Marker) : Prop := ∀ m ∈ markers, m.IsContinuous -instance (markers : List RelClauseMarker) : Decidable (SatisfiesHC2 markers) := by +instance (markers : List Marker) : Decidable (SatisfiesHC2 markers) := by unfold SatisfiesHC2; infer_instance /-- PRC: every primary marker is upward-closed on the AH. If marker `m` @@ -95,19 +95,19 @@ instance (markers : List RelClauseMarker) : Decidable (SatisfiesHC2 markers) := above `pos`. This is the paper's Primary Relativization Constraint (p. 68), which follows from HC₂ for primary strategies (see `prc_from_hc2` below for the general derivation). -/ -def SatisfiesPRC (markers : List RelClauseMarker) : Prop := +def SatisfiesPRC (markers : List Marker) : Prop := ∀ m ∈ markers, m.IsPrimary → ∀ pos ∈ AHPosition.all, m.Covers pos → ∀ above ∈ AHPosition.all, above.rank > pos.rank → m.Covers above -instance (markers : List RelClauseMarker) : Decidable (SatisfiesPRC markers) := by +instance (markers : List Marker) : Decidable (SatisfiesPRC markers) := by unfold SatisfiesPRC; infer_instance /-- The lowest AH position covered by any marker in the list (i.e., the deepest the language can reach). Returns `.subject` if even SU is uncovered (vacuously, since HC₁ would be violated). -/ -def lowestCovered (markers : List RelClauseMarker) : AHPosition := - let coversAny (pos : AHPosition) := markers.any (·.covers pos) +def lowestCovered (markers : List Marker) : AHPosition := + let coversAny (pos : AHPosition) := markers.any (fun m => decide (m.Covers pos)) if coversAny .objComparison then .objComparison else if coversAny .genitive then .genitive else if coversAny .oblique then .oblique @@ -131,7 +131,7 @@ abbrev welsh := Fragments.Welsh.relMarkers §14.4.2, exposed in the Fragment as `relAsyndeticGap` and `relAsyndeticResumptive` — but K&C 1977 does not record them, so this study works with the K&C-documented subset. -/ -abbrev arabic : List Core.RelClauseMarker := +abbrev arabic : List Marker := [Fragments.Arabic.ModernStandard.relAlladhi, Fragments.Arabic.ModernStandard.relResumptive] abbrev hebrew := Fragments.Hebrew.relMarkers @@ -142,13 +142,13 @@ abbrev malagasy := Fragments.Malagasy.relMarkers abbrev yoruba := Fragments.Yoruba.relMarkers /-- The 8-language sub-sample from the original paper Table 1 (pp. 76-79). -/ -def originalSample : List (List RelClauseMarker) := +def originalSample : List (List Marker) := [english, welsh, arabic, hebrew, tobaBatak, korean, finnish, malagasy] /-- The original 8-language sample plus Yoruba (the only post-1977 addition; refutes one of the paper's implicit ±case generalizations — see `yoruba_refutes_minus_case_covers_subjects` below). -/ -def allSamples : List (List RelClauseMarker) := +def allSamples : List (List Marker) := originalSample ++ [yoruba] theorem sample_size : allSamples.length = 9 := by decide @@ -170,7 +170,7 @@ theorem hc2_verified : theorem prc_verified : ∀ markers ∈ allSamples, SatisfiesPRC markers := by decide -/-- Restating HC₁ in terms of `RelClauseMarker.IsPrimary`: every language +/-- Restating HC₁ in terms of `Marker.IsPrimary`: every language has at least one primary marker. -/ theorem every_language_has_primary : ∀ markers ∈ allSamples, ∃ m ∈ markers, m.IsPrimary := by decide @@ -247,38 +247,38 @@ theorem english_full_coverage : covers IO/OBL/GEN/OCOMP. -/ theorem welsh_strategy_split : welsh.length = 2 ∧ - (welsh.map (·.covers .subject)) = [true, false] ∧ - (welsh.map (·.covers .directObject)) = [true, false] ∧ - (welsh.map (·.covers .indirectObject)) = [false, true] ∧ - (welsh.map (·.covers .objComparison)) = [false, true] := by decide + (welsh.map (fun m => decide (m.Covers .subject))) = [true, false] ∧ + (welsh.map (fun m => decide (m.Covers .directObject))) = [true, false] ∧ + (welsh.map (fun m => decide (m.Covers .indirectObject))) = [false, true] ∧ + (welsh.map (fun m => decide (m.Covers .objComparison))) = [false, true] := by decide /-- Arabic (MSA) (Table 1 p. 76): the relative pronoun *alladhī/allatii* used alone (-case strategy) covers SU only; *alladhī/allatii* with a resumptive pronoun (+case strategy) covers DO–OCOMP. -/ theorem arabic_primary_su_only : - (arabic.map (·.covers .subject)) = [true, false] ∧ - (arabic.map (·.covers .directObject)) = [false, true] := by decide + (arabic.map (fun m => decide (m.Covers .subject))) = [true, false] ∧ + (arabic.map (fun m => decide (m.Covers .directObject))) = [false, true] := by decide /-- Malagasy (Table 1 p. 78; paper §1.3.1 p. 69-70): single marker, SU only. -/ theorem malagasy_su_only : malagasy.length = 1 ∧ - (malagasy.map (·.covers .subject)) = [true] ∧ - (malagasy.map (·.covers .directObject)) = [false] := by decide + (malagasy.map (fun m => decide (m.Covers .subject))) = [true] ∧ + (malagasy.map (fun m => decide (m.Covers .directObject))) = [false] := by decide /-- Korean (Table 1 p. 78; paper §1.3.4 p. 74): -case adnominal verb suffix covers SU/DO/IO/OBL but not GEN; +case genitive marker covers GEN only. -/ theorem korean_primary_su_to_obl : - (korean.map (·.covers .subject)) = [true, false] ∧ - (korean.map (·.covers .oblique)) = [true, false] ∧ - (korean.map (·.covers .genitive)) = [false, true] := by decide + (korean.map (fun m => decide (m.Covers .subject))) = [true, false] ∧ + (korean.map (fun m => decide (m.Covers .oblique))) = [true, false] ∧ + (korean.map (fun m => decide (m.Covers .genitive))) = [false, true] := by decide /-- Finnish (Table 1 p. 76; paper §1.3.2 p. 70-71): the +case marker *joka* is the broader/primary one (covers SU–GEN); the -case participial marker also covers SU but is narrower (SU/DO only). -/ theorem finnish_plus_case_is_primary : (finnish.map (·.bearsCaseMarking)) = [true, false] ∧ - (finnish.map (·.isPrimary)) = [true, true] := by decide + (finnish.map (fun m => decide m.IsPrimary)) = [true, true] := by decide /-- Yoruba: 4 per-position markers. relTiSubject (-case, primary, only SU); relTiObject (-case, NOT primary, only DO); relTiOblique (-case, @@ -287,13 +287,13 @@ theorem finnish_plus_case_is_primary : theorem yoruba_strategy_breakdown : yoruba.length = 4 ∧ (yoruba.map (·.bearsCaseMarking)) = [false, false, false, true] ∧ - (yoruba.map (·.isPrimary)) = [true, false, false, false] := by decide + (yoruba.map (fun m => decide m.IsPrimary)) = [true, false, false, false] := by decide -- ============================================================================ --- § 7: Bridge to RelativizationProfile (Typology layer) +-- § 7: Bridge to RelativeClause.Profile (Typology layer) -- ============================================================================ -/-! K&C 1977 Table 1's per-position coverage and `RelativizationProfile`'s +/-! K&C 1977 Table 1's per-position coverage and `RelativeClause.Profile`'s WALS-derived `lowestRelativizable` encode complementary views of the same data. Bridge theorems below verify agreement on the lowest position covered, language by language. K&C's Table 1 is strictly more detailed @@ -354,7 +354,7 @@ theorem kc_at_least_as_detailed_as_wals : /-! HC₂ ("any RC-forming strategy must apply to a continuous segment of the AH") is a paper-anchored claim. The contiguity machinery (`contiguousOnAH`, -`AHPosition.rank`) lives in `Core/Relativization/Hierarchy.lean` because it +`AHPosition.rank`) lives in `Typology/RelativeClause/Basic.lean` because it mirrors `Core/Case/Hierarchy.lean::validInventory` and is genuinely framework-agnostic. The specific contiguous-segment witnesses below exemplify HC₂ on the AH and are part of @cite{keenan-comrie-1977}'s core @@ -386,7 +386,7 @@ theorem su_do_obl_not_contiguous : /-! The PRC is the paper's main derivation: it follows from HC₁ + HC₂ rather than being an independent stipulation. The general proof lives here (paper -content), not in `Core/Relativization/Hierarchy.lean` (substrate). -/ +content), not in `Typology/RelativeClause/Basic.lean` (substrate). -/ /-- BEq agrees with propositional equality for AH positions. -/ private theorem ah_beq_iff (a b : AHPosition) : diff --git a/Linglib/Studies/Landau2026.lean b/Linglib/Studies/Landau2026.lean index a3b803b09..5d4e140ed 100644 --- a/Linglib/Studies/Landau2026.lean +++ b/Linglib/Studies/Landau2026.lean @@ -1,4 +1,4 @@ -import Linglib.Core.Relativization.Basic +import Linglib.Typology.RelativeClause.Basic import Linglib.Fragments.Hebrew.Relativization /-! @@ -49,7 +49,7 @@ EIR diagnoses contested "mixed anaphors" as deep: namespace Landau2026 -open Core +open RelativeClause -- ═══════════════════════════════════════════════════════════════ -- § 1: Types @@ -412,7 +412,7 @@ theorem mixed_anaphors_deep : /-- Hebrew has a productive resumptive strategy in relativization — the prerequisite for applying the EIR test. The same - resumptive pronoun type that `Core.NPRelType.resumptive` models + resumptive pronoun type that `RelativeClause.NPRelType.resumptive` models for relative clauses is what the EIR test probes for inside ellipsis sites. -/ theorem hebrew_has_resumptive_strategy : @@ -423,12 +423,12 @@ theorem hebrew_has_resumptive_strategy : where possessive resumptive pronouns (the most common type in the EIR data) sit. -/ theorem resumptive_covers_genitive : - Fragments.Hebrew.relSheResumptive.covers .genitive = true := rfl + Fragments.Hebrew.relSheResumptive.Covers .genitive := by decide /-- The gap strategy does NOT cover genitive — this is why possessive dependencies in Hebrew require resumption, making the EIR test applicable. -/ theorem gap_excludes_genitive : - Fragments.Hebrew.relSheGap.covers .genitive = false := rfl + ¬ Fragments.Hebrew.relSheGap.Covers .genitive := by decide end Landau2026 diff --git a/Linglib/Studies/Scott2021.lean b/Linglib/Studies/Scott2021.lean index 62c8de0b1..30c5e73e6 100644 --- a/Linglib/Studies/Scott2021.lean +++ b/Linglib/Studies/Scott2021.lean @@ -1,4 +1,4 @@ -import Linglib.Core.Relativization.Basic +import Linglib.Typology.RelativeClause.Basic import Linglib.Core.Tree import Linglib.Fragments.Swahili.Relativization import Linglib.Morphology.DM.VocabularyInsertion diff --git a/Linglib/Syntax/HPSG/Core/RelativeClauses.lean b/Linglib/Syntax/HPSG/Core/RelativeClauses.lean index 366c9981f..d1bf1be98 100644 --- a/Linglib/Syntax/HPSG/Core/RelativeClauses.lean +++ b/Linglib/Syntax/HPSG/Core/RelativeClauses.lean @@ -159,7 +159,7 @@ private def clause_tracked : TrackedSign := private def relClause : RelClauseDerivation := { rel := relThat gappedClause := clause_tracked - gapCompatible := .inr (by native_decide) } + gapCompatible := .inr (by decide) } -- The result is a modifier with MOD = NOUN #guard relClause.isMod @@ -211,7 +211,7 @@ private def subj_gapped_clause : TrackedSign := private def who_relClause : RelClauseDerivation := { rel := relWho gappedClause := subj_gapped_clause - gapCompatible := .inr (by native_decide) } + gapCompatible := .inr (by decide) } #guard who_relClause.isMod #guard who_relClause.result.sign.synsem.mod == some .NOUN @@ -237,7 +237,7 @@ theorem relClause_is_modifier (d : RelClauseDerivation) : /-- Any category matches itself under `categoriesMatch`. -/ private theorem categoriesMatch_refl (c : UD.UPOS) : categoriesMatch c c = true := by - cases c <;> native_decide + cases c <;> decide /-- Head-Modifier succeeds when MOD matches the head's category. -/ theorem headMod_succeeds_when_mod_matches (headNoun : Sign) (relClause : TrackedSign) diff --git a/Linglib/Typology/Extraction.lean b/Linglib/Typology/Extraction.lean index a9a81bd72..c672e8bd7 100644 --- a/Linglib/Typology/Extraction.lean +++ b/Linglib/Typology/Extraction.lean @@ -127,8 +127,8 @@ inductive Extractee where which positions are marked, and whether the marking distinguishes between different extracted positions. - Follows the `RelativizationProfile` pattern from - `Typology/Relativization/Defs.lean`. -/ + Follows the `RelativeClause.Profile` pattern from + `Typology/RelativeClause/WALS.lean`. -/ structure ExtractionProfile where /-- Language name -/ language : String diff --git a/Linglib/Typology/RelativeClause/Basic.lean b/Linglib/Typology/RelativeClause/Basic.lean new file mode 100644 index 000000000..95fcb86ab --- /dev/null +++ b/Linglib/Typology/RelativeClause/Basic.lean @@ -0,0 +1,347 @@ +import Linglib.Features.Definiteness +import Linglib.Typology.Extraction + +/-! +# Relative clauses: structural core + +Theory-neutral types for cross-linguistic relative-clause data: the +@cite{keenan-comrie-1977} 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 `Features.Case` for case inventories. + +## Main declarations + +* `RelativeClause.AHPosition` — grammatical positions on the + @cite{keenan-comrie-1977} 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.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 (@cite{blake-1994}); 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. +-/ + +set_option autoImplicit false + +namespace RelativeClause + +open Typology (ExtractionTarget) + +/-! ### Grammatical positions on the Accessibility Hierarchy -/ + +/-- 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 -/ +inductive AHPosition where + /-- Subject: the most accessible position. Virtually all languages + with relative clauses can relativize subjects. -/ + | subject + /-- Direct object: the second most accessible position. -/ + | directObject + /-- Indirect object: third position. -/ + | indirectObject + /-- Oblique: fourth position (instrumentals, locatives, etc.). -/ + | oblique + /-- Genitive: fifth position (possessors). -/ + | genitive + /-- Object of comparison: the least accessible position + ("the person [that I am taller than _]"). -/ + | objComparison + deriving DecidableEq, Repr + +/-- Numeric rank of a position on the Accessibility Hierarchy. + Higher rank = more accessible = more languages can relativize it. -/ +def AHPosition.rank : AHPosition → Nat + | .subject => 6 + | .directObject => 5 + | .indirectObject => 4 + | .oblique => 3 + | .genitive => 2 + | .objComparison => 1 + +/-- Position p1 is at least as accessible as p2 on the hierarchy. -/ +def AHPosition.atLeastAsAccessible (p1 p2 : AHPosition) : Prop := + p1.rank ≥ p2.rank + +instance (p1 p2 : AHPosition) : Decidable (p1.atLeastAsAccessible p2) := + inferInstanceAs (Decidable (_ ≥ _)) + +/-- Position p1 is strictly more accessible than p2. -/ +def AHPosition.moreAccessible (p1 p2 : AHPosition) : Prop := + p1.rank > p2.rank + +instance (p1 p2 : AHPosition) : Decidable (p1.moreAccessible p2) := + inferInstanceAs (Decidable (_ > _)) + +/-- All AH positions in descending order of accessibility. -/ +def AHPosition.all : List AHPosition := + [.subject, .directObject, .indirectObject, .oblique, .genitive, .objComparison] + +/-! ### Relative-clause position -/ + +/-- 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. -/ +inductive RCPosition where + /-- Post-nominal: RC follows the head noun. E.g., English "the man + [who left]", Arabic "ar-rajul [alladhi ghadara]". -/ + | postNominal + /-- Pre-nominal: RC precedes the head noun. E.g., Japanese + "[ _ kaetta] hito", Korean "[ _ tteonagan] saram". -/ + | preNominal + /-- Internally-headed: the head noun appears inside the RC. E.g., + Bambara. -/ + | internallyHeaded + /-- 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". -/ + | correlative + deriving DecidableEq, Repr + +/-! ### NP_rel type (what occupies the relativized position) -/ + +/-- 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. -/ +inductive NPRelType where + /-- Gap: NP_rel is deleted; no overt element at the extraction site. + The "lightest" strategy. E.g., English "the man [that _ left]". -/ + | gap + /-- 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]'. -/ + | resumptive + /-- 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} -/ + | resumptiveMovement + /-- 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} -/ + | resumptiveBound + /-- 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]". -/ + | relPronoun + /-- Non-reduction: NP_rel is a full NP — the head noun is repeated + inside the RC. E.g., Bambara. -/ + | nonReduction + deriving DecidableEq, Repr + +/-- 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). -/ +def NPRelType.isMovementCopy : NPRelType → Option Bool + | .resumptiveMovement => some true + | .resumptiveBound => some false + | .resumptive => none -- unspecified (pre-Scott typology) + | _ => none -- non-resumptive + +/-! ### Relative-clause marker -/ + +/-- 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) -/ +structure Marker where + /-- Surface form of the marker (e.g., "a", "joka", "that/∅", "-(n)ɨn"). -/ + form : String + /-- What occupies the relativized position in this construction. -/ + npRel : NPRelType + /-- Whether the relative element bears case marking (±case). -/ + bearsCaseMarking : Bool + /-- Position of the RC with respect to the head noun. -/ + rcPosition : RCPosition + /-- Which grammatical positions can be relativized using this marker. -/ + positions : List AHPosition + /-- 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; @cite{ryding-2005}): MSA *alladhī* + with definite antecedents vs Ø-relative-pronoun with indefinite + antecedents. Substrate makes no claim about syntactic mechanism. -/ + headDefiniteness : Option Features.Definiteness.Definiteness := none + /-- Additional notes. -/ + notes : String := "" + deriving BEq, Repr + +/-- Does this marker cover a given AH position? -/ +def Marker.Covers (m : Marker) (p : AHPosition) : Prop := + p ∈ m.positions + +instance (m : Marker) (p : AHPosition) : Decidable (m.Covers p) := by + unfold Marker.Covers; infer_instance + +/-! ### Accessibility-Hierarchy contiguity (HC₂) -/ + +/-- Whether a list of AH positions contains at least one position at rank r. -/ +def hasAHRank (positions : List AHPosition) (r : Nat) : Bool := + positions.any fun p => p.rank == r + +/-- 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 (@cite{blake-1994}). + + This formalizes HC₂ of @cite{keenan-comrie-1977}: "Any RC-forming + strategy must apply to a continuous segment of the AH." -/ +def contiguousOnAH (positions : List AHPosition) : Bool := + positions.all fun p1 => + positions.all fun p2 => + if p2.rank > p1.rank then + let lo := p1.rank + let hi := p2.rank + List.range hi |>.all fun r => + if r > lo && r < hi then hasAHRank positions r + else true + else true + +/-- 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. -/ +def ContiguousOnAH (positions : List AHPosition) : Prop := + contiguousOnAH positions = true + +instance (positions : List AHPosition) : Decidable (ContiguousOnAH positions) := + inferInstanceAs (Decidable (_ = _)) + +/-- A marker's positions form a contiguous segment of the AH. -/ +def Marker.IsContinuous (m : Marker) : Prop := + ContiguousOnAH m.positions + +instance (m : Marker) : Decidable m.IsContinuous := + inferInstanceAs (Decidable (ContiguousOnAH _)) + +/-- A marker is **primary** in @cite{keenan-comrie-1977}'s sense if it can be + used to relativize subjects. HC₁ requires every language to have at + least one primary marker. -/ +def Marker.IsPrimary (m : Marker) : Prop := + m.Covers .subject + +instance (m : Marker) : Decidable m.IsPrimary := + inferInstanceAs (Decidable (m.Covers .subject)) + +/-! ### Ordering theorems -/ + +/-- 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 ah_rank_injective (a b : AHPosition) (h : a.rank = b.rank) : a = b := by + cases a <;> cases b <;> simp_all [AHPosition.rank] + +/-- All ranks are between 1 and 6. -/ +theorem ah_rank_bounded (p : AHPosition) : 1 ≤ p.rank ∧ p.rank ≤ 6 := by + cases p <;> simp [AHPosition.rank] + +/-- Accessibility is reflexive (follows from `≥` on ℕ). -/ +theorem ah_reflexive (p : AHPosition) : p.atLeastAsAccessible p := by + simp [AHPosition.atLeastAsAccessible] + +/-- Accessibility is transitive (follows from `≥` on ℕ). -/ +theorem ah_transitive (a b c : AHPosition) + (h1 : a.atLeastAsAccessible b) (h2 : b.atLeastAsAccessible c) : + a.atLeastAsAccessible c := by + simp [AHPosition.atLeastAsAccessible] at *; omega + +/-! ### Extraction bridge + +Maps between `Typology.ExtractionTarget` (5 structural positions from +extraction morphology, in `Typology/Extraction.lean`) and `AHPosition` (6 +positions on the @cite{keenan-comrie-1977} 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`. -/ + +/-- Map an extraction target to its AH position. Possessor extraction + corresponds to the genitive position on the AH. -/ +def extractionTargetToAH : ExtractionTarget → AHPosition + | .subject => .subject + | .directObject => .directObject + | .indirectObject => .indirectObject + | .oblique => .oblique + | .possessor => .genitive + +/-- Map an AH position to an extraction target (partial: + `objComparison` has no standard `ExtractionTarget` equivalent). -/ +def ahToExtractionTarget : AHPosition → Option ExtractionTarget + | .subject => some .subject + | .directObject => some .directObject + | .indirectObject => some .indirectObject + | .oblique => some .oblique + | .genitive => some .possessor + | .objComparison => none + +/-- ExtractionTarget → AH → ExtractionTarget is the identity. -/ +theorem extraction_ah_roundtrip (t : ExtractionTarget) : + ahToExtractionTarget (extractionTargetToAH t) = some t := by + cases t <;> rfl + +/-- AH → ExtractionTarget → AH is the identity for every position + except `objComparison` (which has no `ExtractionTarget`). -/ +theorem ah_extraction_roundtrip (p : AHPosition) (h : p ≠ .objComparison) : + ∃ t, ahToExtractionTarget p = some t ∧ extractionTargetToAH t = p := by + cases p with + | objComparison => exact absurd rfl h + | subject => exact ⟨.subject, rfl, rfl⟩ + | directObject => exact ⟨.directObject, rfl, rfl⟩ + | indirectObject => exact ⟨.indirectObject, rfl, rfl⟩ + | oblique => exact ⟨.oblique, rfl, rfl⟩ + | genitive => exact ⟨.possessor, rfl, rfl⟩ + +/-- `objComparison` is the only AH position without an `ExtractionTarget`. -/ +theorem objComparison_no_extraction_target : + ahToExtractionTarget .objComparison = none := rfl + +/-- Every non-`objComparison` AH position has an `ExtractionTarget` equivalent. -/ +theorem non_ocomp_have_extraction_target (p : AHPosition) (h : p ≠ .objComparison) : + (ahToExtractionTarget p).isSome := by + cases p <;> first | rfl | exact absurd rfl h + +end RelativeClause diff --git a/Linglib/Typology/Relativization/Defs.lean b/Linglib/Typology/RelativeClause/WALS.lean similarity index 51% rename from Linglib/Typology/Relativization/Defs.lean rename to Linglib/Typology/RelativeClause/WALS.lean index 7dfddb702..2343640cb 100644 --- a/Linglib/Typology/Relativization/Defs.lean +++ b/Linglib/Typology/RelativeClause/WALS.lean @@ -1,41 +1,46 @@ -import Linglib.Core.Relativization.Basic +import Linglib.Typology.RelativeClause.Basic import Linglib.Data.WALS.Features.F90D import Linglib.Data.WALS.Features.F122A import Linglib.Data.WALS.Features.F123A /-! -# `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. +# Relative clauses: typological survey (WALS) +@cite{comrie-1989} @cite{keenan-comrie-1977} @cite{comrie-2013} + +The cross-linguistic WALS-survey facet of the relative clause: the per-language +`Profile` summarizing relativization strategies (WALS Chs 122/123/90D), the RC +position, and the @cite{keenan-comrie-1977} Accessibility-Hierarchy cut-off, +with the WALS converters and the aggregate distribution theorems. Per-language +values live in `Fragments/{Lang}/Relativization.lean` as +`def relativization : RelativeClause.Profile`. + +## 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.InternallyHeadedStrategy` — status of the head-internal + strategy (WALS Ch 90D). +* `RelativeClause.Profile` — per-language relativization summary. +* `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. -/ -namespace Typology.Relativization +set_option autoImplicit false --- ============================================================================ --- Subject relativization strategies (WALS Ch 122) --- ============================================================================ +namespace RelativeClause + +/-! ### Subject relativization strategies (WALS Ch 122) -/ /-- WALS Ch 122: strategy used to relativize the subject position. -/ -inductive SubjRelStrategy where +inductive SubjStrategy where /-- The relativized position is empty. E.g., English "the man [that _ left]". -/ | gap /-- A resumptive pronoun fills the position. E.g., dialectal Arabic. -/ @@ -51,13 +56,11 @@ inductive SubjRelStrategy where | mixed deriving DecidableEq, Repr --- ============================================================================ --- Oblique relativization strategies (WALS Ch 123) --- ============================================================================ +/-! ### Oblique relativization strategies (WALS Ch 123) -/ /-- WALS Ch 123: strategy used to relativize oblique positions, or -whether obliques can be relativized at all. -/ -inductive OblRelStrategy where + whether obliques can be relativized at all. -/ +inductive OblStrategy where /-- Gap on obliques (often with preposition stranding). -/ | gap /-- Resumptive pronoun on obliques (more common than for subjects). -/ @@ -73,16 +76,14 @@ inductive OblRelStrategy where | notRelativizable deriving DecidableEq, Repr --- ============================================================================ --- Internally-headed strategy (WALS Ch 90D) --- ============================================================================ +/-! ### Internally-headed strategy (WALS Ch 90D) -/ /-- 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. -/ + 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. -/ inductive InternallyHeadedStrategy where /-- Internally-headed is the dominant strategy. -/ | dominant @@ -104,21 +105,19 @@ inductive InternallyHeadedStrategy where | absent deriving DecidableEq, Repr --- ============================================================================ --- Profile structure --- ============================================================================ +/-! ### Profile -/ /-- A language's relativization profile: WALS Chs 122/123 strategies plus -RC position and AH cut-off. -/ -structure RelativizationProfile where + RC position and AH cut-off. -/ +structure Profile where /-- Strategy used for relativizing subjects (Ch 122). -/ - subjStrategy : SubjRelStrategy + subjStrategy : SubjStrategy /-- Strategy used for relativizing obliques (Ch 123). -/ - oblStrategy : OblRelStrategy + oblStrategy : OblStrategy /-- Position of the relative clause with respect to the head noun. -/ - rcPosition : Core.RCPosition + rcPosition : RCPosition /-- Lowest @cite{keenan-comrie-1977} AH position that can be relativized. -/ - lowestRelativizable : Core.AHPosition + lowestRelativizable : AHPosition /-- 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. -/ @@ -128,24 +127,22 @@ structure RelativizationProfile where notes : String := "" deriving Repr, DecidableEq --- ============================================================================ --- WALS converters --- ============================================================================ +/-! ### WALS converters (Chs 122, 123, 90D) -/ -/-- Convert a WALS 122A subject relativization value to `SubjRelStrategy`. +/-- 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. -/ -def fromWALS122A : Data.WALS.F122A.SubjectRelativization → SubjRelStrategy +def fromWALS122A : Data.WALS.F122A.SubjectRelativization → SubjStrategy | .relativePronoun => .relativePronoun | .nonReduction => .nonReduction | .pronounRetention => .pronounRetention | .gap => .gap -/-- Convert a WALS 123A oblique relativization value to `OblRelStrategy`. +/-- Convert a WALS 123A oblique relativization value to `OblStrategy`. WALS `.notPossible` becomes `.notRelativizable`; `.mixed` profiles cannot be grounded against WALS via this converter. -/ -def fromWALS123A : Data.WALS.F123A.ObliqueRelativization → OblRelStrategy +def fromWALS123A : Data.WALS.F123A.ObliqueRelativization → OblStrategy | .relativePronoun => .relativePronoun | .nonReduction => .nonReduction | .pronounRetention => .pronounRetention @@ -165,4 +162,43 @@ def fromWALS90D : Data.WALS.F90D.InternallyHeadedRelativeClauses → | .occursAsNondominantType => .nondominant | .exists_ => .attested -end Typology.Relativization +/-! ### Distribution theorems + +WALS-aggregate findings on relative-clause formation strategies +(@cite{comrie-2013}). Ch 122 (subjects): 166 languages; gap dominates, +reflecting subjects' high accessibility on the @cite{keenan-comrie-1977} +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. -/ + +private abbrev ch122 := Data.WALS.F122A.allData +private abbrev ch123 := Data.WALS.F123A.allData + +set_option maxRecDepth 2000 in +/-- WALS Ch 122: gap is the most common subject relativization strategy, + followed by non-reduction, relative pronoun, and pronoun retention. -/ +theorem gap_most_common_for_subjects : + (ch122.filter (·.value == .gap)).length > + (ch122.filter (·.value == .nonReduction)).length ∧ + (ch122.filter (·.value == .nonReduction)).length > + (ch122.filter (·.value == .relativePronoun)).length ∧ + (ch122.filter (·.value == .relativePronoun)).length > + (ch122.filter (·.value == .pronounRetention)).length := by + refine ⟨?_, ?_, ?_⟩ <;> decide + +set_option maxRecDepth 2000 in +/-- WALS Chs 122/123: pronoun retention is more common for obliques than + for subjects — a key Accessibility-Hierarchy prediction + (@cite{keenan-comrie-1977}). -/ +theorem retention_increases_for_obliques : + (ch123.filter (·.value == .pronounRetention)).length > + (ch122.filter (·.value == .pronounRetention)).length := by decide + +set_option maxRecDepth 2000 in +/-- WALS Ch 123: some languages cannot relativize obliques at all, + contrasting with subjects, where the Ch 122 enum has no "not + possible" value. -/ +theorem obliques_sometimes_not_relativizable : + (ch123.filter (·.value == .notPossible)).length > 0 := by decide + +end RelativeClause diff --git a/Linglib/Typology/Relativization/Basic.lean b/Linglib/Typology/Relativization/Basic.lean deleted file mode 100644 index e8573e240..000000000 --- a/Linglib/Typology/Relativization/Basic.lean +++ /dev/null @@ -1,87 +0,0 @@ -import Linglib.Data.WALS.Features.F122A -import Linglib.Data.WALS.Features.F123A - -/-! -# Cross-Linguistic Typology of Relativization (WALS Chapters 122/123) -@cite{comrie-1989} @cite{keenan-comrie-1977} @cite{comrie-2013} - -WALS-aggregate findings on relative-clause formation strategies from two -WALS chapters by @cite{comrie-2013}. The `RelativizationProfile` struct -+ strategy enums + WALS converters live in `Typology/Relativization/Defs.lean`; -per-language data lives in `Fragments/{Lang}/Relativization.lean`. - -## Ch 122: Relativization on Subjects - -How languages form relative clauses on subject position. Strategies: gap -(the relativized position is empty), pronoun retention (a resumptive -pronoun fills the relativized position), relative pronoun (a dedicated -wh-element fills the position and typically fronts), non-reduction (head -noun repeated inside the relative clause). - -Sample: 166 languages (WALS v2020.4). Gap dominates for subjects, -reflecting the high accessibility of subject position on the -@cite{keenan-comrie-1977} hierarchy. - -## Ch 123: Relativization on Obliques - -Whether oblique positions can be relativized, and by what strategy. Many -gap-on-subject languages switch to pronoun retention or relative pronouns -for obliques, or cannot relativize obliques at all. - -Sample: 112 languages (WALS v2020.4). Gap remains the most common -strategy, but pronoun retention is much more common than for subjects, and -a sizeable minority of languages cannot relativize obliques at all. - -## @cite{keenan-comrie-1977} Accessibility Hierarchy - -The Accessibility Hierarchy ranks grammatical positions by their -accessibility to relativization: - - Subject > Direct Object > Indirect Object > Oblique > Genitive > Object of Comparison - -Three Hierarchy Constraints follow: - -1. **HC₁**: A language must be able to relativize subjects. -2. **HC₂ (Continuity)**: Any RC-forming strategy must apply to a continuous - segment of the AH. -3. **HC₃ (Cut-off)**: Strategies that apply at one point may cease at any - lower point. - -From these, the **Primary Relativization Constraint** follows: if a -language's primary strategy can apply to a low position, it can also apply -to all higher positions. --/ - -namespace Typology.Relativization - -private abbrev ch122 := Data.WALS.F122A.allData -private abbrev ch123 := Data.WALS.F123A.allData - -set_option maxRecDepth 2000 in -/-- WALS Ch 122: gap is the most common subject relativization strategy, - followed by non-reduction, relative pronoun, and pronoun retention. -/ -theorem gap_most_common_for_subjects : - (ch122.filter (·.value == .gap)).length > - (ch122.filter (·.value == .nonReduction)).length ∧ - (ch122.filter (·.value == .nonReduction)).length > - (ch122.filter (·.value == .relativePronoun)).length ∧ - (ch122.filter (·.value == .relativePronoun)).length > - (ch122.filter (·.value == .pronounRetention)).length := by - refine ⟨?_, ?_, ?_⟩ <;> decide - -set_option maxRecDepth 2000 in -/-- WALS Chs 122/123: pronoun retention is more common for obliques than - for subjects — a key Accessibility-Hierarchy prediction - (@cite{keenan-comrie-1977}). -/ -theorem retention_increases_for_obliques : - (ch123.filter (·.value == .pronounRetention)).length > - (ch122.filter (·.value == .pronounRetention)).length := by decide - -set_option maxRecDepth 2000 in -/-- WALS Ch 123: some languages cannot relativize obliques at all, - contrasting with subjects, where the Ch 122 enum has no "not - possible" value. -/ -theorem obliques_sometimes_not_relativizable : - (ch123.filter (·.value == .notPossible)).length > 0 := by decide - -end Typology.Relativization diff --git a/Linglib/Typology/Relativization/ExtractionBridge.lean b/Linglib/Typology/Relativization/ExtractionBridge.lean deleted file mode 100644 index 940dd2570..000000000 --- a/Linglib/Typology/Relativization/ExtractionBridge.lean +++ /dev/null @@ -1,85 +0,0 @@ -import Linglib.Core.Relativization.Basic -import Linglib.Typology.Extraction - -/-! -# Extraction Morphology ↔ Accessibility Hierarchy Bridge -@cite{keenan-comrie-1977} - -Maps between `Typology.ExtractionTarget` (5 structural positions from -extraction morphology, defined in `Typology/Extraction.lean`) and -`Core.AHPosition` (6 positions on the @cite{keenan-comrie-1977} -Accessibility Hierarchy). - -Both type systems encode overlapping Ā-movement phenomena: extraction -focuses on *where* extraction occurs (used by Mayan, Austronesian, -Celtic Fragments); the AH focuses on *what can be relativized* (used -by relativization Fragments and the Keenan-Comrie hierarchy -constraints). The bridge is partial: `AHPosition.objComparison` (object -of comparison, specific to the relativization literature) has no -standard `ExtractionTarget` equivalent. In the other direction, -`ExtractionTarget.possessor` maps to `AHPosition.genitive`. --/ - -namespace Typology.Relativization - -open Core (AHPosition) -open Typology (ExtractionTarget) - --- ============================================================================ --- § 1: ExtractionTarget → AHPosition --- ============================================================================ - -/-- Map an extraction target to its AH position. Possessor extraction - corresponds to the genitive position on the AH. -/ -def extractionTargetToAH : ExtractionTarget → AHPosition - | .subject => .subject - | .directObject => .directObject - | .indirectObject => .indirectObject - | .oblique => .oblique - | .possessor => .genitive - --- ============================================================================ --- § 2: AHPosition → ExtractionTarget (partial) --- ============================================================================ - -/-- Map an AH position to an extraction target (partial: - `objComparison` has no standard `ExtractionTarget` equivalent). -/ -def ahToExtractionTarget : AHPosition → Option ExtractionTarget - | .subject => some .subject - | .directObject => some .directObject - | .indirectObject => some .indirectObject - | .oblique => some .oblique - | .genitive => some .possessor - | .objComparison => none - --- ============================================================================ --- § 3: Roundtrip Theorems (compile-time exhaustive over constructors) --- ============================================================================ - -/-- ExtractionTarget → AH → ExtractionTarget is the identity. -/ -theorem extraction_ah_roundtrip (t : ExtractionTarget) : - ahToExtractionTarget (extractionTargetToAH t) = some t := by - cases t <;> rfl - -/-- AH → ExtractionTarget → AH is the identity for every position - except `objComparison` (which has no `ExtractionTarget`). -/ -theorem ah_extraction_roundtrip (p : AHPosition) (h : p ≠ .objComparison) : - ∃ t, ahToExtractionTarget p = some t ∧ extractionTargetToAH t = p := by - cases p with - | objComparison => exact absurd rfl h - | subject => exact ⟨.subject, rfl, rfl⟩ - | directObject => exact ⟨.directObject, rfl, rfl⟩ - | indirectObject => exact ⟨.indirectObject, rfl, rfl⟩ - | oblique => exact ⟨.oblique, rfl, rfl⟩ - | genitive => exact ⟨.possessor, rfl, rfl⟩ - -/-- `objComparison` is the only AH position without an `ExtractionTarget`. -/ -theorem objComparison_no_extraction_target : - ahToExtractionTarget .objComparison = none := rfl - -/-- Every non-`objComparison` AH position has an `ExtractionTarget` equivalent. -/ -theorem non_ocomp_have_extraction_target (p : AHPosition) (h : p ≠ .objComparison) : - (ahToExtractionTarget p).isSome := by - cases p <;> first | rfl | exact absurd rfl h - -end Typology.Relativization