From 879d8aa0383d7ad406b807044e04b53c51f25891 Mon Sep 17 00:00:00 2001 From: Robert Hawkins Date: Sat, 30 May 2026 18:04:26 -0700 Subject: [PATCH 1/2] fix(Typology): correct WALS cites + ResumptiveKind in relativization --- Linglib/Studies/Erlewine2018.lean | 2 +- Linglib/Studies/Scott2021.lean | 6 ++-- Linglib/Typology/Extraction.lean | 2 +- Linglib/Typology/RelativeClause/Basic.lean | 39 ++++++++++++++-------- Linglib/Typology/RelativeClause/WALS.lean | 9 ++--- 5 files changed, 36 insertions(+), 22 deletions(-) diff --git a/Linglib/Studies/Erlewine2018.lean b/Linglib/Studies/Erlewine2018.lean index 2793cb925..f864fab76 100644 --- a/Linglib/Studies/Erlewine2018.lean +++ b/Linglib/Studies/Erlewine2018.lean @@ -171,7 +171,7 @@ theorem tb_distinguishes : /-! Connects three independent data sources through the AH bridge: 1. Individual extraction datums (from @cite{erlewine-2018}) 2. The ExtractionProfile summary (markedPositions) -3. RelClauseMarkers (from @cite{keenan-comrie-1977}) +3. Relative-clause markers (from @cite{keenan-comrie-1977}) If any link is wrong — e.g., listing `.directObject` as extractable when relativization markers don't cover DO — the chain breaks. diff --git a/Linglib/Studies/Scott2021.lean b/Linglib/Studies/Scott2021.lean index 30c5e73e6..9344b4a44 100644 --- a/Linglib/Studies/Scott2021.lean +++ b/Linglib/Studies/Scott2021.lean @@ -499,9 +499,9 @@ theorem fragment_consistency_1sg : /-- The movement marker in the Fragment is correctly classified. -/ theorem marker_classification : - ambaMovement.npRel.isMovementCopy = some true ∧ - ambaBound.npRel.isMovementCopy = some false ∧ - ambaGap.npRel.isMovementCopy = none := by + ambaMovement.npRel.resumptiveKind = some .movementCopy ∧ + ambaBound.npRel.resumptiveKind = some .bound ∧ + ambaGap.npRel.resumptiveKind = none := by exact ⟨rfl, rfl, rfl⟩ -- ============================================================================ diff --git a/Linglib/Typology/Extraction.lean b/Linglib/Typology/Extraction.lean index c672e8bd7..0a2ddbdf8 100644 --- a/Linglib/Typology/Extraction.lean +++ b/Linglib/Typology/Extraction.lean @@ -66,7 +66,7 @@ paper. They are not enum cases here. -/ /-- The grammatical position from which extraction occurs. This intersects with the @cite{keenan-comrie-1977} Accessibility Hierarchy - (see `Core/Relativization/Hierarchy.lean`), but is defined independently + (see `Typology/RelativeClause/Basic.lean`), but is defined independently because extraction morphology may make finer distinctions than relativization. -/ inductive ExtractionTarget where diff --git a/Linglib/Typology/RelativeClause/Basic.lean b/Linglib/Typology/RelativeClause/Basic.lean index 95fcb86ab..1a3d13960 100644 --- a/Linglib/Typology/RelativeClause/Basic.lean +++ b/Linglib/Typology/RelativeClause/Basic.lean @@ -139,13 +139,13 @@ inductive NPRelType where 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} -/ + @cite{scott-2021} -/ | 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} -/ + @cite{scott-2021} -/ | resumptiveBound /-- Relative pronoun: NP_rel is a dedicated relative pronoun that typically fronts to clause-initial position and bears case. @@ -156,15 +156,28 @@ inductive NPRelType where | 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 +/-- The movement/base-generation status of a resumptive pronoun, for + languages where the two coexist morphologically (@cite{scott-2021} for + Swahili, @cite{sichel-2014} for Hebrew). -/ +inductive ResumptiveKind where + /-- A partially-pronounced lower copy of an Ā-movement chain. -/ + | movementCopy + /-- A base-generated pronoun bound by the relative-clause head. -/ + | bound + /-- A resumptive whose movement-vs-base-generation status is unspecified + (pre-@cite{scott-2021} typology). -/ + | unspecified + deriving DecidableEq, Repr + +/-- The resumptive kind of an `NPRelType`, or `none` for non-resumptive + types. Refines the movement-vs-bound contrast; unlike a tri-state + `Option Bool`, it keeps "unspecified resumptive" and "not a resumptive" + as genuinely distinct outcomes. -/ +def NPRelType.resumptiveKind : NPRelType → Option ResumptiveKind + | .resumptiveMovement => some .movementCopy + | .resumptiveBound => some .bound + | .resumptive => some .unspecified + | _ => none /-! ### Relative-clause marker -/ @@ -213,8 +226,8 @@ structure Marker where 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 +instance (m : Marker) (p : AHPosition) : Decidable (m.Covers p) := + inferInstanceAs (Decidable (p ∈ m.positions)) /-! ### Accessibility-Hierarchy contiguity (HC₂) -/ diff --git a/Linglib/Typology/RelativeClause/WALS.lean b/Linglib/Typology/RelativeClause/WALS.lean index 2343640cb..7da9cc872 100644 --- a/Linglib/Typology/RelativeClause/WALS.lean +++ b/Linglib/Typology/RelativeClause/WALS.lean @@ -5,7 +5,7 @@ import Linglib.Data.WALS.Features.F123A /-! # Relative clauses: typological survey (WALS) -@cite{comrie-1989} @cite{keenan-comrie-1977} @cite{comrie-2013} +@cite{comrie-1989} @cite{keenan-comrie-1977} @cite{comrie-kuteva-2013a} @cite{comrie-kuteva-2013b} @cite{dryer-2013-wals} The cross-linguistic WALS-survey facet of the relative clause: the per-language `Profile` summarizing relativization strategies (WALS Chs 122/123/90D), the RC @@ -122,8 +122,8 @@ structure Profile where to `.absent`, since most languages outside East Asia, Mesoamerica, and a few isolates lack this construction. -/ internallyHeaded : InternallyHeadedStrategy := .absent - /-- Free-text notes on the relativization system, including - `@cite{...}` keys for hand-coded values. -/ + /-- Free-text notes on the relativization system, including citation + keys for hand-coded values. -/ notes : String := "" deriving Repr, DecidableEq @@ -165,7 +165,8 @@ def fromWALS90D : Data.WALS.F90D.InternallyHeadedRelativeClauses → /-! ### Distribution theorems WALS-aggregate findings on relative-clause formation strategies -(@cite{comrie-2013}). Ch 122 (subjects): 166 languages; gap dominates, +(@cite{comrie-kuteva-2013a} @cite{comrie-kuteva-2013b} @cite{dryer-2013-wals}). +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 From a7a9d641fe0a8f096dea3e57a746ce4f9ddfec6b Mon Sep 17 00:00:00 2001 From: Robert Hawkins Date: Sat, 30 May 2026 18:12:25 -0700 Subject: [PATCH 2/2] fix(Data/WALS): correct Ch 122/123 relativization cites in generator --- Linglib/Data/WALS/Features/F122A.lean | 2 +- Linglib/Data/WALS/Features/F123A.lean | 2 +- scripts/gen_wals.py | 6 +++--- 3 files changed, 5 insertions(+), 5 deletions(-) diff --git a/Linglib/Data/WALS/Features/F122A.lean b/Linglib/Data/WALS/Features/F122A.lean index 81aaae54f..36fb68568 100644 --- a/Linglib/Data/WALS/Features/F122A.lean +++ b/Linglib/Data/WALS/Features/F122A.lean @@ -2,7 +2,7 @@ import Linglib.Data.WALS.Datapoint /-! # WALS Feature 122A: Relativization on Subjects -@cite{comrie-2013} +@cite{comrie-kuteva-2013a} Auto-generated from WALS v2020.4 CLDF data. **Do not edit by hand** — regenerate with `python3 scripts/gen_wals.py 122A`. diff --git a/Linglib/Data/WALS/Features/F123A.lean b/Linglib/Data/WALS/Features/F123A.lean index 193df16de..6350e985f 100644 --- a/Linglib/Data/WALS/Features/F123A.lean +++ b/Linglib/Data/WALS/Features/F123A.lean @@ -2,7 +2,7 @@ import Linglib.Data.WALS.Datapoint /-! # WALS Feature 123A: Relativization on Obliques -@cite{comrie-2013} +@cite{comrie-kuteva-2013b} Auto-generated from WALS v2020.4 CLDF data. **Do not edit by hand** — regenerate with `python3 scripts/gen_wals.py 123A`. diff --git a/scripts/gen_wals.py b/scripts/gen_wals.py index 50fdf01aa..f0cb1292f 100644 --- a/scripts/gen_wals.py +++ b/scripts/gen_wals.py @@ -241,8 +241,8 @@ def name_to_constructor(name): # ── Comparatives/Relatives (Ch 121–123) ──────────────────────────── "121A": {"enum": "ComparativeType", "author": "stassen-2013"}, - "122A": {"enum": "SubjectRelativization", "author": "comrie-2013"}, - "123A": {"enum": "ObliqueRelativization", "author": "comrie-2013"}, + "122A": {"enum": "SubjectRelativization", "author": "comrie-kuteva-2013a"}, + "123A": {"enum": "ObliqueRelativization", "author": "comrie-kuteva-2013b"}, # ── Morphology (Ch 20–22, 26–27) ────────────────────────────────── "20A": {"enum": "FusionType", "author": "bickel-nichols-2013a"}, @@ -720,7 +720,7 @@ def generate_languages(langs, used_ids): return "\n".join(lines) -REFERENCES_BIB = ROOT / "blog" / "data" / "references.bib" +REFERENCES_BIB = ROOT / "blog" / "references.bib" def load_bib_keys(): """Return the set of bibkeys defined in blog/data/references.bib."""