From ea14b8afed4f061b59053b5a5d3a3e5e36c2aab4 Mon Sep 17 00:00:00 2001 From: Robert Hawkins Date: Thu, 4 Jun 2026 08:20:43 -0700 Subject: [PATCH 1/3] refactor(Core,Features): one UD file; feature types to Features/ --- Linglib.lean | 4 +- Linglib/Core/Tree.lean | 2 +- Linglib/Core/UD/Word.lean | 136 ----- .../Basic.lean => UniversalDependencies.lean} | 49 ++ Linglib/Features/Case.lean | 2 +- Linglib/Features/Gender.lean | 2 +- Linglib/Features/MassCount.lean | 15 + Linglib/Features/Number.lean | 6 +- Linglib/Features/OntologicalCategory.lean | 2 +- Linglib/Features/Person.lean | 30 +- Linglib/Fragments/Dargwa/Agreement.lean | 2 +- Linglib/Fragments/Dutch/Nouns.lean | 2 +- Linglib/Fragments/English/Auxiliaries.lean | 6 +- .../Fragments/English/Complementizers.lean | 2 +- Linglib/Fragments/English/Determiners.lean | 2 +- Linglib/Fragments/English/FunctionWords.lean | 2 +- .../English/Modifiers/Adjectives.lean | 2 +- Linglib/Fragments/English/Nouns.lean | 3 +- .../Fragments/English/NumeralModifiers.lean | 2 +- Linglib/Fragments/English/Pronouns.lean | 2 +- Linglib/Fragments/Farsi/Determiners.lean | 2 +- Linglib/Fragments/French/Determiners.lean | 2 +- Linglib/Fragments/French/Nouns.lean | 2 +- Linglib/Fragments/Ga/Basic.lean | 6 +- Linglib/Fragments/Hungarian/Reciprocals.lean | 3 + Linglib/Fragments/Italian/Nouns.lean | 5 +- Linglib/Fragments/Italian/Pronouns.lean | 2 +- Linglib/Fragments/Japanese/Determiners.lean | 2 +- Linglib/Fragments/Japanese/Nouns.lean | 2 +- .../Fragments/Jarawara/PossessedNouns.lean | 2 +- Linglib/Fragments/Kawapanan/Shawi/Basic.lean | 4 + Linglib/Fragments/Mandarin/Determiners.lean | 2 +- Linglib/Fragments/Mandarin/Nouns.lean | 2 +- Linglib/Fragments/Mandarin/Reciprocals.lean | 2 +- Linglib/Fragments/Mayan/Kiche/Agreement.lean | 2 +- .../Mayan/Mam/ExtractionMorphology.lean | 2 +- Linglib/Fragments/Mayan/Params.lean | 2 +- Linglib/Fragments/Mixtec/SMPM/Basic.lean | 2 +- .../Fragments/NezPerce/ClausalEmbedding.lean | 2 +- Linglib/Fragments/Nungon/MedialVerbs.lean | 2 +- .../Fragments/Slavic/Czech/Determiners.lean | 2 +- Linglib/Fragments/Spanish/Clitics.lean | 2 +- Linglib/Fragments/Wambaya/Reciprocals.lean | 2 +- Linglib/Fragments/Yoruba/FocusParticles.lean | 3 +- Linglib/Morphology/MorphRule.lean | 2 +- Linglib/Paradigms/AcceptabilityJudgment.lean | 2 +- .../Phenomena/Anaphora/DonkeyAnaphora.lean | 2 +- .../Attitudes/ConjunctionDistribution.lean | 2 +- .../Attitudes/IntentionalIdentity.lean | 2 +- .../Phenomena/AuxiliaryVerbs/Selection.lean | 2 +- .../Phenomena/Ellipsis/FragmentAnswers.lean | 2 +- Linglib/Phenomena/Ellipsis/NPEllipsis.lean | 2 +- Linglib/Phenomena/Ellipsis/Sluicing.lean | 2 +- Linglib/Phenomena/Ellipsis/VPEllipsis.lean | 2 +- Linglib/Phenomena/Focus/Basic.lean | 2 +- .../Phenomena/Focus/ProsodicExhaustivity.lean | 2 +- Linglib/Phenomena/NullSubject/Defs.lean | 2 +- Linglib/Phenomena/Politeness/Honorifics.lean | 2 +- Linglib/Phenomena/Questions/Basic.lean | 2 +- Linglib/Pragmatics/Implicature/Basic.lean | 2 +- Linglib/Semantics/ArgumentStructure/Defs.lean | 2 +- Linglib/Semantics/Aspect/Composition.lean | 3 +- Linglib/Semantics/Dynamic/DiscourseRef.lean | 3 +- Linglib/Semantics/Kinds/Anaphora.lean | 539 +++++++++--------- .../Semantics/Kinds/MeaningPreservation.lean | 3 +- .../Kinds/NominalMappingParameter.lean | 3 +- Linglib/Semantics/Mood/ClauseType.lean | 2 +- Linglib/Semantics/Quantification/Lexicon.lean | 2 +- Linglib/Semantics/TypeTheoretic/Basic.lean | 2 +- Linglib/Studies/AissenPolian2025.lean | 1 + Linglib/Studies/AlexeyenkoZeijlstra2025.lean | 2 +- Linglib/Studies/AnandHardtMcCloskey2021.lean | 2 +- Linglib/Studies/Borer2005.lean | 1 + Linglib/Studies/Cacchioli2025.lean | 2 +- Linglib/Studies/FillmoreKayOConnor1988.lean | 2 +- Linglib/Studies/Gibson2025.lean | 3 +- Linglib/Studies/Gotham2017.lean | 2 +- Linglib/Studies/HalpertHammerly2026.lean | 6 +- Linglib/Studies/Harbour2016.lean | 8 +- Linglib/Studies/Haspelmath1997Polarity.lean | 2 +- Linglib/Studies/KehlerRohde2013.lean | 2 +- Linglib/Studies/Krifka2026.lean | 427 +++++++------- Linglib/Studies/OsborneLi2023.lean | 2 +- Linglib/Studies/RomeroHan2004.lean | 2 +- Linglib/Studies/Sauerland2003.lean | 4 +- Linglib/Studies/Smith1997.lean | 1 + Linglib/Studies/TurkHirsch2026.lean | 2 +- Linglib/Studies/Wang2023.lean | 2 +- Linglib/Studies/Zheng2025.lean | 2 +- Linglib/Syntax/Agreement/Paradigm.lean | 2 +- Linglib/Syntax/Binding/Basic.lean | 2 +- .../ArgumentStructure.lean | 2 +- Linglib/Syntax/DependencyGrammar/Basic.lean | 2 +- Linglib/Syntax/DependencyGrammar/Nominal.lean | 2 +- Linglib/Syntax/HPSG/Basic.lean | 2 +- Linglib/Syntax/Minimalist/Basic.lean | 2 +- Linglib/Syntax/Minimalist/Features.lean | 5 +- Linglib/Syntax/Minimalist/Modification.lean | 399 ++++++------- Linglib/Syntax/Pronoun/Basic.lean | 6 +- Linglib/Syntax/Pronoun/Capabilities.lean | 2 +- Linglib/Typology/Adposition.lean | 3 +- Linglib/Typology/AuxiliaryVerbs.lean | 2 +- Linglib/Typology/ClauseChaining.lean | 4 +- Linglib/Typology/WordOrder.lean | 8 + 104 files changed, 912 insertions(+), 929 deletions(-) delete mode 100644 Linglib/Core/UD/Word.lean rename Linglib/Core/{UD/Basic.lean => UniversalDependencies.lean} (90%) create mode 100644 Linglib/Features/MassCount.lean diff --git a/Linglib.lean b/Linglib.lean index 8e26a203b..32f8c66a8 100644 --- a/Linglib.lean +++ b/Linglib.lean @@ -8,7 +8,7 @@ and their interfaces. See README.md for documentation links. import Linglib.Features.Dimension import Linglib.Features.Gender import Linglib.Core.Valence -import Linglib.Core.UD.Word +import Linglib.Core.UniversalDependencies import Linglib.Typology.NegativeConcord import Linglib.Typology.PolarityItem import Linglib.Typology.Negation @@ -38,7 +38,6 @@ import Linglib.Core.Logic.Team.Closure import Linglib.Core.Logic.Team.Definability import Linglib.Features.Acceptability import Linglib.Semantics.Dynamic.ParameterizedUpdate -import Linglib.Core.UD.Basic import Linglib.Core.Tree import Linglib.Features.Coordination import Linglib.Core.Logic.Duality @@ -221,6 +220,7 @@ import Linglib.Features.Evidentiality import Linglib.Features.Mirativity import Linglib.Semantics.Epistemicity import Linglib.Features.Logophoricity +import Linglib.Features.MassCount import Linglib.Core.WorldTimeIndex import Linglib.Core.Time.Interval.Basic import Linglib.Core.Time.Interval.Generalized diff --git a/Linglib/Core/Tree.lean b/Linglib/Core/Tree.lean index 399c17a08..44c089cf4 100644 --- a/Linglib/Core/Tree.lean +++ b/Linglib/Core/Tree.lean @@ -1,6 +1,6 @@ import Mathlib.Data.List.Infix import Mathlib.Algebra.Free -import Linglib.Core.UD.Basic +import Linglib.Core.UniversalDependencies import Linglib.Core.Order.Tree /-! diff --git a/Linglib/Core/UD/Word.lean b/Linglib/Core/UD/Word.lean deleted file mode 100644 index 68cd2a7e4..000000000 --- a/Linglib/Core/UD/Word.lean +++ /dev/null @@ -1,136 +0,0 @@ -import Linglib.Core.UD.Basic - -/-! -# Word -[biberauer-roberts-2014] [dryer-1992] - -The lexical unit and its building blocks: morphological feature types (aliased -to Universal Dependencies) and the `Word` structure. A word's morphology is one -`UD.MorphFeatures` bundle — there is no separate word-level feature record. - -## Provenance - -Lifted from `Core/Lexical/Word.lean` in the cleanup that dissolved -`Core/Lexical/`. Every layer (Fragments, Phenomena, Theories, Features, -Typology) consumes `Word`; the broad consumer base is the strongest case -for keeping it in `Core/`. - -## Universal Dependencies Integration - -Morphological features are aliased to UD types: -- `Number` = `UD.Number` (with compatibility constructors `sg`, `pl`) -- `Person` = `UD.Person` (with compatibility constructors `first`, `second`, `third`) -- `Voice` = `UD.Voice` (with compatibility constructors `active`, `passive`) -- `VForm` = `UD.VerbForm` (with compatibility constructors) - -The grammatical-case substrate lives separately at `Linglib/Features/Case.lean`. - -Syntactic categories use `UD.UPOS` directly (the 17 universal POS tags). - -Types without UD equivalents remain defined here: -- `HeadDirection` (word-order typology) --/ - --- ============================================================================ --- Aliased Types (backed by UD) --- ============================================================================ - -/-- Grammatical number. Aliased to UD.Number; constructors are UD's own -(`.Sing`, `.Plur`, `.Dual`, …) — there are no lowercase value aliases. -/ -abbrev Number := UD.Number - -/-- Grammatical person. Aliased to UD.Person; constructors are UD's own -(`.first`, `.second`, `.third`, `.zero`). -/ -abbrev Person := UD.Person - -/-- Voice. Aliased to UD.Voice; constructors are UD's own (`.Act`, `.Pass`, …). -/ -abbrev Voice := UD.Voice - -/-- Verb form. Aliased to UD.VerbForm; constructors are UD's own -(`.Fin`, `.Inf`, `.Part`, …). -/ -abbrev VForm := UD.VerbForm - -/-- Tense. Aliased to UD.Tense; constructors are UD's own (`.Past`, `.Pres`, `.Fut`, …). -/ -abbrev Tense := UD.Tense - --- ============================================================================ --- Types Without UD Equivalents --- ============================================================================ - -/-- Morphosyntactic mass/count feature. No direct UD equivalent. - - A formal feature parallel to grammatical gender — not an ontological - distinction. Determines kind-anaphor morphology: [MASS] → *it*, - [COUNT] → *they*. Evidence: *pollen*[MASS] → *it* vs - *pollen grains*[COUNT] → *they* for the same referent - ([krifka-2026] §2). -/ -inductive MassCount where - | mass -- mass nouns: *mold*, *pollen*, *milk*, *gold* - | count -- count nouns: *spider*, *pollen grain*, *dog*, *cup* - deriving Repr, DecidableEq, Hashable - -/-- Head direction of a syntactic construction. - Used for word-order typology and - constraints like FOFC. -/ -inductive HeadDirection where - | headInitial -- head precedes complement (VO, preposition, head-initial FocP, ...) - | headFinal -- head follows complement (OV, postposition, head-final FocP, ...) - deriving Repr, DecidableEq - --- ============================================================================ --- Word --- ============================================================================ - -/-- A word: the pure CoNLL-U surface token — surface form, UD category, and UD morphology - (one `UD.MorphFeatures` bundle; there is no separate word-level feature record). - - **Admission rule**: a property belongs on `Word` iff a Fragment-free token-level engine - reads it off the token's *own* data; otherwise it lives on the typed lexical carrier - (`Pronoun`, `NounEntry`, `Verb`, …) or on the consuming framework's own structures - (e.g. DG subcategorization premises live on `DepTree.frames`, not here). Identity - caveat: `BEq` is form + category, so homographs collapse; a CoNLL-U `lemma` field is - the known fix, deferred until a consumer needs it. -/ -structure Word where - form : String - cat : UD.UPOS - features : UD.MorphFeatures := {} - deriving Repr - -/-- Convenience constructor for a featureless word (form + category only). -/ -def Word.mk' (form : String) (cat : UD.UPOS) : Word := { form := form, cat := cat } - -/-- The φ-feature subset (person, number, gender) of a word, as a - `UD.MorphFeatures` bundle. -/ -def Word.phi (w : Word) : UD.MorphFeatures := - { person := w.features.person, number := w.features.number, - gender := w.features.gender } - -/-- φ-agreement between two words: their person/number/gender features are - compatible (an unspecified feature is a wildcard). A reflexive, symmetric - *tolerance* relation on `Word` (not transitive), decided by the shared - `UD.MorphFeatures.compatible`. This is the feature-based agreement primitive - binding and concord consumers share — no surface-form gender lookup. -/ -def Word.Agree (w1 w2 : Word) : Prop := w1.phi.compatible w2.phi - -instance (w1 w2 : Word) : Decidable (Word.Agree w1 w2) := by - unfold Word.Agree; infer_instance - -@[refl] theorem Word.Agree.refl (w : Word) : Word.Agree w w := - UD.MorphFeatures.compatible_self w.phi - - -/-- Derive a passive variant: sets voice to passive. The valence change - (detransitivization) is a frame-level fact carried by the passive analysis on - `DepTree.frames`, not token data. Composes with `VerbEntry.toWordPastPart`. -/ -def Word.asPassive (w : Word) : Word := - { w with features := { w.features with voice := some .Pass } } - -instance : BEq Word where - beq w1 w2 := w1.form == w2.form && w1.cat == w2.cat - -instance : ToString Word where - toString w := w.form - -/-- Convert a word list to a readable string. -/ -def wordsToString (ws : List Word) : String := - " ".intercalate (ws.map (·.form)) diff --git a/Linglib/Core/UD/Basic.lean b/Linglib/Core/UniversalDependencies.lean similarity index 90% rename from Linglib/Core/UD/Basic.lean rename to Linglib/Core/UniversalDependencies.lean index a54bdd3d9..73901d398 100644 --- a/Linglib/Core/UD/Basic.lean +++ b/Linglib/Core/UniversalDependencies.lean @@ -547,3 +547,52 @@ structure DepArc where deriving DecidableEq, Repr end UD + +-- ============================================================================ +-- Word: the CoNLL-U surface token +-- ============================================================================ + +structure Word where + form : String + cat : UD.UPOS + features : UD.MorphFeatures := {} + deriving Repr + +/-- Convenience constructor for a featureless word (form + category only). -/ +def Word.mk' (form : String) (cat : UD.UPOS) : Word := { form := form, cat := cat } + +/-- The φ-feature subset (person, number, gender) of a word, as a + `UD.MorphFeatures` bundle. -/ +def Word.phi (w : Word) : UD.MorphFeatures := + { person := w.features.person, number := w.features.number, + gender := w.features.gender } + +/-- φ-agreement between two words: their person/number/gender features are + compatible (an unspecified feature is a wildcard). A reflexive, symmetric + *tolerance* relation on `Word` (not transitive), decided by the shared + `UD.MorphFeatures.compatible`. This is the feature-based agreement primitive + binding and concord consumers share — no surface-form gender lookup. -/ +def Word.Agree (w1 w2 : Word) : Prop := w1.phi.compatible w2.phi + +instance (w1 w2 : Word) : Decidable (Word.Agree w1 w2) := by + unfold Word.Agree; infer_instance + +@[refl] theorem Word.Agree.refl (w : Word) : Word.Agree w w := + UD.MorphFeatures.compatible_self w.phi + + +/-- Derive a passive variant: sets voice to passive. The valence change + (detransitivization) is a frame-level fact carried by the passive analysis on + `DepTree.frames`, not token data. Composes with `VerbEntry.toWordPastPart`. -/ +def Word.asPassive (w : Word) : Word := + { w with features := { w.features with voice := some .Pass } } + +instance : BEq Word where + beq w1 w2 := w1.form == w2.form && w1.cat == w2.cat + +instance : ToString Word where + toString w := w.form + +/-- Convert a word list to a readable string. -/ +def wordsToString (ws : List Word) : String := + " ".intercalate (ws.map (·.form)) diff --git a/Linglib/Features/Case.lean b/Linglib/Features/Case.lean index 3fef63b1d..d062ce89e 100644 --- a/Linglib/Features/Case.lean +++ b/Linglib/Features/Case.lean @@ -1,7 +1,7 @@ import Mathlib.Data.Finset.Card import Mathlib.Order.Lattice import Mathlib.Tactic.DeriveFintype -import Linglib.Core.UD.Basic +import Linglib.Core.UniversalDependencies /-! # Case — Feature Taxonomy diff --git a/Linglib/Features/Gender.lean b/Linglib/Features/Gender.lean index 6da0d6cd1..6f2eebcf8 100644 --- a/Linglib/Features/Gender.lean +++ b/Linglib/Features/Gender.lean @@ -1,4 +1,4 @@ -import Linglib.Core.UD.Basic +import Linglib.Core.UniversalDependencies import Linglib.Features.PrivativePair /-! diff --git a/Linglib/Features/MassCount.lean b/Linglib/Features/MassCount.lean new file mode 100644 index 000000000..1747df2b1 --- /dev/null +++ b/Linglib/Features/MassCount.lean @@ -0,0 +1,15 @@ +/-! +# Mass/count + +The morphosyntactic mass/count feature ([krifka-2026]). No UD equivalent, so it is a +linglib feature taxonomy rather than a `UD.*` alias. +-/ + +/-- Morphosyntactic mass/count feature. A formal feature parallel to grammatical + gender — not an ontological distinction. Determines kind-anaphor morphology: + [MASS] → *it*, [COUNT] → *they*. Evidence: *pollen*[MASS] → *it* vs + *pollen grains*[COUNT] → *they* for the same referent ([krifka-2026] §2). -/ +inductive MassCount where + | mass -- mass nouns: *mold*, *pollen*, *milk*, *gold* + | count -- count nouns: *spider*, *pollen grain*, *dog*, *cup* + deriving Repr, DecidableEq, Hashable diff --git a/Linglib/Features/Number.lean b/Linglib/Features/Number.lean index 3032f0a68..5f4a1547b 100644 --- a/Linglib/Features/Number.lean +++ b/Linglib/Features/Number.lean @@ -1,4 +1,4 @@ -import Linglib.Core.UD.Basic +import Linglib.Core.UniversalDependencies import Linglib.Features.PrivativePair /-! @@ -42,6 +42,10 @@ hierarchy, language data) remains in -/ +/-- Grammatical number — UD's descriptive vocabulary (`UD.Number`: `.Sing`, `.Plur`, +`.Dual`, …) as the canonical type; the analytical apparatus below is its API. -/ +abbrev Features.Number := UD.Number + namespace Features.Number -- ============================================================================ diff --git a/Linglib/Features/OntologicalCategory.lean b/Linglib/Features/OntologicalCategory.lean index 3f3c5b93b..8a106a0ec 100644 --- a/Linglib/Features/OntologicalCategory.lean +++ b/Linglib/Features/OntologicalCategory.lean @@ -1,4 +1,4 @@ -import Linglib.Core.UD.Basic +import Linglib.Core.UniversalDependencies import Linglib.Features.Prominence /-! diff --git a/Linglib/Features/Person.lean b/Linglib/Features/Person.lean index 08851ab36..fd2927067 100644 --- a/Linglib/Features/Person.lean +++ b/Linglib/Features/Person.lean @@ -1,4 +1,4 @@ -import Linglib.Core.UD.Basic +import Linglib.Core.UniversalDependencies import Linglib.Features.Prominence import Linglib.Features.PrivativePair @@ -42,6 +42,10 @@ language data) remains in `Phenomena/Agreement/PersonMarkingTypology.lean`. -/ +/-- Grammatical person — UD's descriptive vocabulary (`UD.Person`: `.first`, `.second`, +`.third`, `.zero`) as the canonical type; the feature theory below is its API. -/ +abbrev Features.Person := UD.Person + namespace Features.Person -- ============================================================================ @@ -74,13 +78,13 @@ def Features.wellFormed (pf : Features) : Bool := -- ============================================================================ /-- 1st person features: [+participant, +author]. -/ -def first : Features := ⟨true, true⟩ +def firstF : Features := ⟨true, true⟩ /-- 2nd person features: [+participant, −author]. -/ -def second : Features := ⟨true, false⟩ +def secondF : Features := ⟨true, false⟩ /-- 3rd person features: [−participant, −author]. -/ -def third : Features := ⟨false, false⟩ +def thirdF : Features := ⟨false, false⟩ -- ============================================================================ -- § 3: PersonLevel Bridge @@ -92,9 +96,9 @@ namespace Features.Prominence /-- Decompose `PersonLevel` into binary person features. -/ def PersonLevel.toFeatures : PersonLevel → Features.Person.Features - | .first => Features.Person.first - | .second => Features.Person.second - | .third => Features.Person.third + | .first => Features.Person.firstF + | .second => Features.Person.secondF + | .third => Features.Person.thirdF /-- Convert `UD.Person` to `PersonLevel`. The UD `.zero` (impersonal) case has no `PersonLevel` analogue; everything else is direct. -/ @@ -114,9 +118,9 @@ open Features.Prominence -- § 4: Features Verification -- ============================================================================ -@[simp] theorem first_wellFormed : first.wellFormed = true := rfl -@[simp] theorem second_wellFormed : second.wellFormed = true := rfl -@[simp] theorem third_wellFormed : third.wellFormed = true := rfl +@[simp] theorem firstF_wellFormed : firstF.wellFormed = true := rfl +@[simp] theorem secondF_wellFormed : secondF.wellFormed = true := rfl +@[simp] theorem thirdF_wellFormed : thirdF.wellFormed = true := rfl /-- The ill-formed combination [−participant, +author] is the only combination that violates well-formedness. -/ @@ -150,9 +154,9 @@ instance : Features.PhiFeatures Features where roundtrip := fun ⟨_, _⟩ => rfl /-- The three canonical person values map to the three PrivativePair cells. -/ -@[simp] theorem first_is_maximal : PhiFeatures.toPair first = .maximal := rfl -@[simp] theorem second_is_intermediate : PhiFeatures.toPair second = .intermediate := rfl -@[simp] theorem third_is_minimal : PhiFeatures.toPair third = .minimal := rfl +@[simp] theorem firstF_is_maximal : PhiFeatures.toPair firstF = .maximal := rfl +@[simp] theorem secondF_is_intermediate : PhiFeatures.toPair secondF = .intermediate := rfl +@[simp] theorem thirdF_is_minimal : PhiFeatures.toPair thirdF = .minimal := rfl /-- The `[±participant, ±author]` decomposition **is** the privative pair: an equivalence `Features ≃ PrivativePair` ([harbour-2016]'s phi-kernel skeleton as an isomorphism, not a diff --git a/Linglib/Fragments/Dargwa/Agreement.lean b/Linglib/Fragments/Dargwa/Agreement.lean index a7ce9cf6f..b87c3ca6e 100644 --- a/Linglib/Fragments/Dargwa/Agreement.lean +++ b/Linglib/Fragments/Dargwa/Agreement.lean @@ -1,5 +1,5 @@ import Linglib.Features.Prominence -import Linglib.Core.UD.Word +import Linglib.Core.UniversalDependencies import Linglib.Features.Gender /-! diff --git a/Linglib/Fragments/Dutch/Nouns.lean b/Linglib/Fragments/Dutch/Nouns.lean index 570b52f5c..93f41ab1e 100644 --- a/Linglib/Fragments/Dutch/Nouns.lean +++ b/Linglib/Fragments/Dutch/Nouns.lean @@ -1,4 +1,4 @@ -import Linglib.Core.UD.Word +import Linglib.Core.UniversalDependencies import Linglib.Semantics.Kinds.NominalMappingParameter /-! diff --git a/Linglib/Fragments/English/Auxiliaries.lean b/Linglib/Fragments/English/Auxiliaries.lean index efb6b278c..f6ab0460c 100644 --- a/Linglib/Fragments/English/Auxiliaries.lean +++ b/Linglib/Fragments/English/Auxiliaries.lean @@ -1,4 +1,6 @@ -import Linglib.Core.UD.Word +import Linglib.Core.UniversalDependencies +import Linglib.Features.Number +import Linglib.Features.Person import Linglib.Semantics.Modality.ModalTypes import Linglib.Features.Register @@ -47,6 +49,8 @@ To find every claim made about a particular entry, grep for `Theories/`. -/ +open Features (Number Person) + namespace English.Auxiliaries section Modals diff --git a/Linglib/Fragments/English/Complementizers.lean b/Linglib/Fragments/English/Complementizers.lean index 0ed87acb1..8622edcc3 100644 --- a/Linglib/Fragments/English/Complementizers.lean +++ b/Linglib/Fragments/English/Complementizers.lean @@ -1,4 +1,4 @@ -import Linglib.Core.UD.Word +import Linglib.Core.UniversalDependencies /-! # English Complementizers Lexicon Fragment diff --git a/Linglib/Fragments/English/Determiners.lean b/Linglib/Fragments/English/Determiners.lean index bed0e67df..ac4b4f8fb 100644 --- a/Linglib/Fragments/English/Determiners.lean +++ b/Linglib/Fragments/English/Determiners.lean @@ -1,4 +1,4 @@ -import Linglib.Core.UD.Word +import Linglib.Core.UniversalDependencies import Linglib.Semantics.Quantification.Lexicon /-! diff --git a/Linglib/Fragments/English/FunctionWords.lean b/Linglib/Fragments/English/FunctionWords.lean index 76364ac22..b73c6de6a 100644 --- a/Linglib/Fragments/English/FunctionWords.lean +++ b/Linglib/Fragments/English/FunctionWords.lean @@ -1,4 +1,4 @@ -import Linglib.Core.UD.Word +import Linglib.Core.UniversalDependencies /-! # English Miscellaneous Function Words Fragment diff --git a/Linglib/Fragments/English/Modifiers/Adjectives.lean b/Linglib/Fragments/English/Modifiers/Adjectives.lean index 311aaf6b4..8f4de1909 100644 --- a/Linglib/Fragments/English/Modifiers/Adjectives.lean +++ b/Linglib/Fragments/English/Modifiers/Adjectives.lean @@ -18,7 +18,7 @@ Both share scale type and antonym information, but serve different grammatical f -/ -import Linglib.Core.UD.Word +import Linglib.Core.UniversalDependencies import Linglib.Features.PropertyDomain import Linglib.Morphology.Exponence import Linglib.Morphology.DegreeContainment diff --git a/Linglib/Fragments/English/Nouns.lean b/Linglib/Fragments/English/Nouns.lean index cac93999f..aa626f2aa 100644 --- a/Linglib/Fragments/English/Nouns.lean +++ b/Linglib/Fragments/English/Nouns.lean @@ -1,7 +1,8 @@ -import Linglib.Core.UD.Word +import Linglib.Core.UniversalDependencies import Linglib.Features.Gender import Linglib.Morphology.Exponence import Linglib.Semantics.Kinds.NominalMappingParameter +import Linglib.Features.MassCount /-! # English Noun Lexicon Fragment diff --git a/Linglib/Fragments/English/NumeralModifiers.lean b/Linglib/Fragments/English/NumeralModifiers.lean index 963b7990e..894751932 100644 --- a/Linglib/Fragments/English/NumeralModifiers.lean +++ b/Linglib/Fragments/English/NumeralModifiers.lean @@ -18,7 +18,7 @@ from "up to" (positive), predicting divergent framing effects. -/ -import Linglib.Core.UD.Word +import Linglib.Core.UniversalDependencies import Linglib.Features.PropertyDomain import Linglib.Features.Valence import Linglib.Semantics.Numerals.Basic diff --git a/Linglib/Fragments/English/Pronouns.lean b/Linglib/Fragments/English/Pronouns.lean index 8ba729440..1e28c7ae9 100644 --- a/Linglib/Fragments/English/Pronouns.lean +++ b/Linglib/Fragments/English/Pronouns.lean @@ -1,4 +1,4 @@ -import Linglib.Core.UD.Word +import Linglib.Core.UniversalDependencies import Linglib.Features.Case import Linglib.Features.Gender import Linglib.Syntax.Pronoun.Basic diff --git a/Linglib/Fragments/Farsi/Determiners.lean b/Linglib/Fragments/Farsi/Determiners.lean index fa1512013..f4dcb2b4e 100644 --- a/Linglib/Fragments/Farsi/Determiners.lean +++ b/Linglib/Fragments/Farsi/Determiners.lean @@ -1,4 +1,4 @@ -import Linglib.Core.UD.Word +import Linglib.Core.UniversalDependencies import Linglib.Semantics.Quantification.ChoiceFunction import Linglib.Semantics.Modality.ModalTypes import Mathlib.Data.Rat.Defs diff --git a/Linglib/Fragments/French/Determiners.lean b/Linglib/Fragments/French/Determiners.lean index 566321bdd..3d38fb08f 100644 --- a/Linglib/Fragments/French/Determiners.lean +++ b/Linglib/Fragments/French/Determiners.lean @@ -1,4 +1,4 @@ -import Linglib.Core.UD.Word +import Linglib.Core.UniversalDependencies import Linglib.Semantics.Quantification.Lexicon /-! diff --git a/Linglib/Fragments/French/Nouns.lean b/Linglib/Fragments/French/Nouns.lean index aa146939a..fe1335225 100644 --- a/Linglib/Fragments/French/Nouns.lean +++ b/Linglib/Fragments/French/Nouns.lean @@ -1,5 +1,5 @@ import Linglib.Features.Gender -import Linglib.Core.UD.Word +import Linglib.Core.UniversalDependencies import Linglib.Semantics.Kinds.NominalMappingParameter /-! # French Noun Lexicon Fragment diff --git a/Linglib/Fragments/Ga/Basic.lean b/Linglib/Fragments/Ga/Basic.lean index 3b2bc684e..bd8ebf90d 100644 --- a/Linglib/Fragments/Ga/Basic.lean +++ b/Linglib/Fragments/Ga/Basic.lean @@ -1,5 +1,7 @@ import Linglib.Features.Gender -import Linglib.Core.UD.Word +import Linglib.Core.UniversalDependencies +import Linglib.Features.Number +import Linglib.Features.Person /-! # Gã Fragment @@ -37,6 +39,8 @@ diagnostic requires a free Neg head; Gã `-ee` and `-ko` appear suffixal) that is orthogonal to the OC story. -/ +open Features (Number Person) + namespace Ga -- ════════════════════════════════════════════════════════════════ diff --git a/Linglib/Fragments/Hungarian/Reciprocals.lean b/Linglib/Fragments/Hungarian/Reciprocals.lean index 9fa50d926..041273ed4 100644 --- a/Linglib/Fragments/Hungarian/Reciprocals.lean +++ b/Linglib/Fragments/Hungarian/Reciprocals.lean @@ -1,6 +1,7 @@ import Linglib.Syntax.Pronoun.Basic import Linglib.Semantics.Reference.Reciprocals import Linglib.Semantics.Reference.PluralityLicensing +import Linglib.Features.Number /-! # Hungarian Reciprocal Fragment @@ -38,6 +39,8 @@ construction types, while reflexives require morphosyntactic plurality (I-)reading. [dalrymple-haug-2024] §2. -/ +open Features (Number) + namespace Hungarian.Reciprocals open Pronoun diff --git a/Linglib/Fragments/Italian/Nouns.lean b/Linglib/Fragments/Italian/Nouns.lean index 2701c4743..1ace223dd 100644 --- a/Linglib/Fragments/Italian/Nouns.lean +++ b/Linglib/Fragments/Italian/Nouns.lean @@ -1,6 +1,7 @@ import Linglib.Features.Gender -import Linglib.Core.UD.Word +import Linglib.Core.UniversalDependencies import Linglib.Semantics.Kinds.NominalMappingParameter +import Linglib.Features.Number /-! # Italian Noun Lexicon Fragment @@ -23,6 +24,8 @@ The partitive articles (di + definite article) serve as the obligatory indefinite plural — Italian has no bare plural arguments. -/ +open Features (Number) + namespace Italian.Nouns open Semantics.Kinds.NMP (BlockingPrinciple NominalMapping) diff --git a/Linglib/Fragments/Italian/Pronouns.lean b/Linglib/Fragments/Italian/Pronouns.lean index 959e3c14d..d507c0398 100644 --- a/Linglib/Fragments/Italian/Pronouns.lean +++ b/Linglib/Fragments/Italian/Pronouns.lean @@ -1,6 +1,6 @@ import Linglib.Syntax.Pronoun.Basic import Linglib.Syntax.Pronoun.Capabilities -import Linglib.Core.UD.Word +import Linglib.Core.UniversalDependencies /-! # Italian Pronoun and Clitic Fragment diff --git a/Linglib/Fragments/Japanese/Determiners.lean b/Linglib/Fragments/Japanese/Determiners.lean index 84acfd24d..e6eace966 100644 --- a/Linglib/Fragments/Japanese/Determiners.lean +++ b/Linglib/Fragments/Japanese/Determiners.lean @@ -1,4 +1,4 @@ -import Linglib.Core.UD.Word +import Linglib.Core.UniversalDependencies import Linglib.Fragments.English.Determiners /-! # Japanese Quantifier Fragment diff --git a/Linglib/Fragments/Japanese/Nouns.lean b/Linglib/Fragments/Japanese/Nouns.lean index bb6fdd13c..efc2d5043 100644 --- a/Linglib/Fragments/Japanese/Nouns.lean +++ b/Linglib/Fragments/Japanese/Nouns.lean @@ -1,4 +1,4 @@ -import Linglib.Core.UD.Word +import Linglib.Core.UniversalDependencies import Linglib.Typology.ClassifierSystem import Linglib.Fragments.Japanese.Classifier import Linglib.Semantics.Kinds.NominalMappingParameter diff --git a/Linglib/Fragments/Jarawara/PossessedNouns.lean b/Linglib/Fragments/Jarawara/PossessedNouns.lean index d81216877..303b8a083 100644 --- a/Linglib/Fragments/Jarawara/PossessedNouns.lean +++ b/Linglib/Fragments/Jarawara/PossessedNouns.lean @@ -1,6 +1,6 @@ import Linglib.Morphology.DM.NominalStructure import Linglib.Typology.Possession -import Linglib.Core.UD.Word +import Linglib.Core.UniversalDependencies import Linglib.Features.Gender /-! diff --git a/Linglib/Fragments/Kawapanan/Shawi/Basic.lean b/Linglib/Fragments/Kawapanan/Shawi/Basic.lean index 048ed0daf..32284e16b 100644 --- a/Linglib/Fragments/Kawapanan/Shawi/Basic.lean +++ b/Linglib/Fragments/Kawapanan/Shawi/Basic.lean @@ -1,6 +1,8 @@ import Linglib.Features.Case import Linglib.Features.Case import Linglib.Features.Prominence +import Linglib.Features.Number +import Linglib.Features.Person /-! # Shawi Agreement Fragment [clem-deal-2024] @@ -36,6 +38,8 @@ of ergative distribution to a particular Agree configuration — lives in `Studies/ClemDeal2024.lean`. -/ +open Features (Number Person) + namespace Kawapanan.Shawi open Features.Prominence (PersonLevel) diff --git a/Linglib/Fragments/Mandarin/Determiners.lean b/Linglib/Fragments/Mandarin/Determiners.lean index 673bf49ae..41031126e 100644 --- a/Linglib/Fragments/Mandarin/Determiners.lean +++ b/Linglib/Fragments/Mandarin/Determiners.lean @@ -1,4 +1,4 @@ -import Linglib.Core.UD.Word +import Linglib.Core.UniversalDependencies import Linglib.Typology.ClassifierSystem import Linglib.Fragments.English.Determiners import Linglib.Fragments.Mandarin.Classifiers diff --git a/Linglib/Fragments/Mandarin/Nouns.lean b/Linglib/Fragments/Mandarin/Nouns.lean index 9c0976007..fb53c1907 100644 --- a/Linglib/Fragments/Mandarin/Nouns.lean +++ b/Linglib/Fragments/Mandarin/Nouns.lean @@ -1,4 +1,4 @@ -import Linglib.Core.UD.Word +import Linglib.Core.UniversalDependencies import Linglib.Typology.ClassifierSystem import Linglib.Fragments.Mandarin.Classifiers import Linglib.Semantics.Kinds.NominalMappingParameter diff --git a/Linglib/Fragments/Mandarin/Reciprocals.lean b/Linglib/Fragments/Mandarin/Reciprocals.lean index 947e92027..a48dea6d4 100644 --- a/Linglib/Fragments/Mandarin/Reciprocals.lean +++ b/Linglib/Fragments/Mandarin/Reciprocals.lean @@ -1,4 +1,4 @@ -import Linglib.Core.UD.Word +import Linglib.Core.UniversalDependencies /-! # Mandarin Reciprocal Fragment diff --git a/Linglib/Fragments/Mayan/Kiche/Agreement.lean b/Linglib/Fragments/Mayan/Kiche/Agreement.lean index 031071507..41983d392 100644 --- a/Linglib/Fragments/Mayan/Kiche/Agreement.lean +++ b/Linglib/Fragments/Mayan/Kiche/Agreement.lean @@ -1,5 +1,5 @@ import Linglib.Features.Case -import Linglib.Core.UD.Word +import Linglib.Core.UniversalDependencies import Linglib.Features.Prominence import Linglib.Fragments.Mayan.Params import Linglib.Typology.Extraction diff --git a/Linglib/Fragments/Mayan/Mam/ExtractionMorphology.lean b/Linglib/Fragments/Mayan/Mam/ExtractionMorphology.lean index a06a2ce63..3d093253a 100644 --- a/Linglib/Fragments/Mayan/Mam/ExtractionMorphology.lean +++ b/Linglib/Fragments/Mayan/Mam/ExtractionMorphology.lean @@ -1,5 +1,5 @@ import Linglib.Typology.Extraction -import Linglib.Core.UD.Word +import Linglib.Core.UniversalDependencies /-! # Mam Extraction Morphology Fragment [elkins-torrence-brown-2026] diff --git a/Linglib/Fragments/Mayan/Params.lean b/Linglib/Fragments/Mayan/Params.lean index ebc4075d1..c0c6cf356 100644 --- a/Linglib/Fragments/Mayan/Params.lean +++ b/Linglib/Fragments/Mayan/Params.lean @@ -1,5 +1,5 @@ import Linglib.Features.Case -import Linglib.Core.UD.Basic +import Linglib.Core.UniversalDependencies import Linglib.Features.Prominence import Linglib.Syntax.Case.Alignment import Linglib.Syntax.Agreement.Paradigm diff --git a/Linglib/Fragments/Mixtec/SMPM/Basic.lean b/Linglib/Fragments/Mixtec/SMPM/Basic.lean index 44ce4b730..725f9df4d 100644 --- a/Linglib/Fragments/Mixtec/SMPM/Basic.lean +++ b/Linglib/Fragments/Mixtec/SMPM/Basic.lean @@ -1,5 +1,5 @@ import Linglib.Features.Gender -import Linglib.Core.UD.Word +import Linglib.Core.UniversalDependencies import Linglib.Syntax.Pronoun.Basic /-! diff --git a/Linglib/Fragments/NezPerce/ClausalEmbedding.lean b/Linglib/Fragments/NezPerce/ClausalEmbedding.lean index 9f85238b9..c3221d8cb 100644 --- a/Linglib/Fragments/NezPerce/ClausalEmbedding.lean +++ b/Linglib/Fragments/NezPerce/ClausalEmbedding.lean @@ -1,5 +1,5 @@ import Linglib.Typology.Complementation -import Linglib.Core.UD.Basic +import Linglib.Core.UniversalDependencies /-! # Nez Perce Clausal Embedding Inventory diff --git a/Linglib/Fragments/Nungon/MedialVerbs.lean b/Linglib/Fragments/Nungon/MedialVerbs.lean index d732b13f8..feba80b55 100644 --- a/Linglib/Fragments/Nungon/MedialVerbs.lean +++ b/Linglib/Fragments/Nungon/MedialVerbs.lean @@ -1,4 +1,4 @@ -import Linglib.Core.UD.Basic +import Linglib.Core.UniversalDependencies /-! # Nungon Medial Verb Morphology [sarvasy-2017] diff --git a/Linglib/Fragments/Slavic/Czech/Determiners.lean b/Linglib/Fragments/Slavic/Czech/Determiners.lean index 4084affd4..62e06c5bd 100644 --- a/Linglib/Fragments/Slavic/Czech/Determiners.lean +++ b/Linglib/Fragments/Slavic/Czech/Determiners.lean @@ -1,4 +1,4 @@ -import Linglib.Core.UD.Word +import Linglib.Core.UniversalDependencies import Linglib.Semantics.Negation.CzechNegation /-! diff --git a/Linglib/Fragments/Spanish/Clitics.lean b/Linglib/Fragments/Spanish/Clitics.lean index 5af2e1bd2..b6ca409c4 100644 --- a/Linglib/Fragments/Spanish/Clitics.lean +++ b/Linglib/Fragments/Spanish/Clitics.lean @@ -1,4 +1,4 @@ -import Linglib.Core.UD.Word +import Linglib.Core.UniversalDependencies /-! # Spanish Clitic Paradigm diff --git a/Linglib/Fragments/Wambaya/Reciprocals.lean b/Linglib/Fragments/Wambaya/Reciprocals.lean index ffafda363..f6f75ed21 100644 --- a/Linglib/Fragments/Wambaya/Reciprocals.lean +++ b/Linglib/Fragments/Wambaya/Reciprocals.lean @@ -1,4 +1,4 @@ -import Linglib.Core.UD.Word +import Linglib.Core.UniversalDependencies /-! # Wambaya Reciprocal Fragment diff --git a/Linglib/Fragments/Yoruba/FocusParticles.lean b/Linglib/Fragments/Yoruba/FocusParticles.lean index 71030e114..0493493ae 100644 --- a/Linglib/Fragments/Yoruba/FocusParticles.lean +++ b/Linglib/Fragments/Yoruba/FocusParticles.lean @@ -1,4 +1,5 @@ -import Linglib.Core.UD.Word +import Linglib.Core.UniversalDependencies +import Linglib.Typology.WordOrder /-! # Yorùbá Focus Particles [aremu-2026] diff --git a/Linglib/Morphology/MorphRule.lean b/Linglib/Morphology/MorphRule.lean index 07f991de3..de4f52ff3 100644 --- a/Linglib/Morphology/MorphRule.lean +++ b/Linglib/Morphology/MorphRule.lean @@ -1,4 +1,4 @@ -import Linglib.Core.UD.Word +import Linglib.Core.UniversalDependencies import Linglib.Core.Valence import Linglib.Syntax.Agreement.Controller diff --git a/Linglib/Paradigms/AcceptabilityJudgment.lean b/Linglib/Paradigms/AcceptabilityJudgment.lean index 7eb44c62d..a0a61e819 100644 --- a/Linglib/Paradigms/AcceptabilityJudgment.lean +++ b/Linglib/Paradigms/AcceptabilityJudgment.lean @@ -1,7 +1,7 @@ import Mathlib.Data.Rat.Defs import Mathlib.Data.Fintype.Basic import Mathlib.Tactic.NormNum -import Linglib.Core.UD.Word +import Linglib.Core.UniversalDependencies import Linglib.Features.ClauseForm /-! diff --git a/Linglib/Phenomena/Anaphora/DonkeyAnaphora.lean b/Linglib/Phenomena/Anaphora/DonkeyAnaphora.lean index bef44f906..ef503e588 100644 --- a/Linglib/Phenomena/Anaphora/DonkeyAnaphora.lean +++ b/Linglib/Phenomena/Anaphora/DonkeyAnaphora.lean @@ -1,4 +1,4 @@ -import Linglib.Core.UD.Word +import Linglib.Core.UniversalDependencies import Linglib.Features.Definiteness import Linglib.Core.Nominal.Determiner import Linglib.Fragments.German.Definiteness diff --git a/Linglib/Phenomena/Attitudes/ConjunctionDistribution.lean b/Linglib/Phenomena/Attitudes/ConjunctionDistribution.lean index d03350f33..6ea68d872 100644 --- a/Linglib/Phenomena/Attitudes/ConjunctionDistribution.lean +++ b/Linglib/Phenomena/Attitudes/ConjunctionDistribution.lean @@ -1,4 +1,4 @@ -import Linglib.Core.UD.Word +import Linglib.Core.UniversalDependencies /-! # Conjunction Distribution: Empirical Data diff --git a/Linglib/Phenomena/Attitudes/IntentionalIdentity.lean b/Linglib/Phenomena/Attitudes/IntentionalIdentity.lean index c047a037e..e13768ef2 100644 --- a/Linglib/Phenomena/Attitudes/IntentionalIdentity.lean +++ b/Linglib/Phenomena/Attitudes/IntentionalIdentity.lean @@ -1,4 +1,4 @@ -import Linglib.Core.UD.Word +import Linglib.Core.UniversalDependencies /-! # Intentional Identity Data [chatzikyriakidis-etal-2025] diff --git a/Linglib/Phenomena/AuxiliaryVerbs/Selection.lean b/Linglib/Phenomena/AuxiliaryVerbs/Selection.lean index 89715cd96..49385bca4 100644 --- a/Linglib/Phenomena/AuxiliaryVerbs/Selection.lean +++ b/Linglib/Phenomena/AuxiliaryVerbs/Selection.lean @@ -1,4 +1,4 @@ -import Linglib.Core.UD.Word +import Linglib.Core.UniversalDependencies /-! # Be/Have Auxiliary Selection in European Perfects diff --git a/Linglib/Phenomena/Ellipsis/FragmentAnswers.lean b/Linglib/Phenomena/Ellipsis/FragmentAnswers.lean index 1a863eb68..c513c9781 100644 --- a/Linglib/Phenomena/Ellipsis/FragmentAnswers.lean +++ b/Linglib/Phenomena/Ellipsis/FragmentAnswers.lean @@ -27,7 +27,7 @@ Fragment answers differ from sluicing: -/ -import Linglib.Core.UD.Word +import Linglib.Core.UniversalDependencies /-! ## Connection to RSA Theory diff --git a/Linglib/Phenomena/Ellipsis/NPEllipsis.lean b/Linglib/Phenomena/Ellipsis/NPEllipsis.lean index 6eb4b696b..6734bdcc8 100644 --- a/Linglib/Phenomena/Ellipsis/NPEllipsis.lean +++ b/Linglib/Phenomena/Ellipsis/NPEllipsis.lean @@ -1,4 +1,4 @@ -import Linglib.Core.UD.Word +import Linglib.Core.UniversalDependencies import Linglib.Semantics.Quantification.BinominalDefs /-! diff --git a/Linglib/Phenomena/Ellipsis/Sluicing.lean b/Linglib/Phenomena/Ellipsis/Sluicing.lean index 02f517103..b0be9bded 100644 --- a/Linglib/Phenomena/Ellipsis/Sluicing.lean +++ b/Linglib/Phenomena/Ellipsis/Sluicing.lean @@ -47,7 +47,7 @@ Case matching follows from the continuation analysis: -/ -import Linglib.Core.UD.Word +import Linglib.Core.UniversalDependencies namespace Phenomena.Ellipsis.Sluicing diff --git a/Linglib/Phenomena/Ellipsis/VPEllipsis.lean b/Linglib/Phenomena/Ellipsis/VPEllipsis.lean index 11db8ec37..966ae68df 100644 --- a/Linglib/Phenomena/Ellipsis/VPEllipsis.lean +++ b/Linglib/Phenomena/Ellipsis/VPEllipsis.lean @@ -1,4 +1,4 @@ -import Linglib.Core.UD.Word +import Linglib.Core.UniversalDependencies /-! # VP Ellipsis: Empirical Data diff --git a/Linglib/Phenomena/Focus/Basic.lean b/Linglib/Phenomena/Focus/Basic.lean index c3dc40eb3..113d74475 100644 --- a/Linglib/Phenomena/Focus/Basic.lean +++ b/Linglib/Phenomena/Focus/Basic.lean @@ -12,7 +12,7 @@ Empirical data on focus interpretation effects (association with focus, contrast -/ -import Linglib.Core.UD.Word +import Linglib.Core.UniversalDependencies import Linglib.Features.InformationStructure open Features.InformationStructure (FIPApplication) diff --git a/Linglib/Phenomena/Focus/ProsodicExhaustivity.lean b/Linglib/Phenomena/Focus/ProsodicExhaustivity.lean index 6cbe6fa99..6da8a3578 100644 --- a/Linglib/Phenomena/Focus/ProsodicExhaustivity.lean +++ b/Linglib/Phenomena/Focus/ProsodicExhaustivity.lean @@ -32,7 +32,7 @@ This phenomenon relates to mention-all vs mention-some: -/ -import Linglib.Core.UD.Word +import Linglib.Core.UniversalDependencies /-! ## Connection to RSA Theory diff --git a/Linglib/Phenomena/NullSubject/Defs.lean b/Linglib/Phenomena/NullSubject/Defs.lean index 9675a21ce..ec0d21254 100644 --- a/Linglib/Phenomena/NullSubject/Defs.lean +++ b/Linglib/Phenomena/NullSubject/Defs.lean @@ -1,4 +1,4 @@ -import Linglib.Core.UD.Basic +import Linglib.Core.UniversalDependencies /-! # Subject-Context Vocabulary diff --git a/Linglib/Phenomena/Politeness/Honorifics.lean b/Linglib/Phenomena/Politeness/Honorifics.lean index da16c905f..f1f8e5409 100644 --- a/Linglib/Phenomena/Politeness/Honorifics.lean +++ b/Linglib/Phenomena/Politeness/Honorifics.lean @@ -13,7 +13,7 @@ encode addressee features — and the morphosyntactic expression of honorifics. -/ -import Linglib.Core.UD.Word +import Linglib.Core.UniversalDependencies namespace Phenomena.Politeness.Honorifics diff --git a/Linglib/Phenomena/Questions/Basic.lean b/Linglib/Phenomena/Questions/Basic.lean index 10c17202f..0c38f2451 100644 --- a/Linglib/Phenomena/Questions/Basic.lean +++ b/Linglib/Phenomena/Questions/Basic.lean @@ -1,4 +1,4 @@ -import Linglib.Core.UD.Word +import Linglib.Core.UniversalDependencies import Linglib.Features.OntologicalCategory /-! diff --git a/Linglib/Pragmatics/Implicature/Basic.lean b/Linglib/Pragmatics/Implicature/Basic.lean index 9a6b1df14..e45eeab39 100644 --- a/Linglib/Pragmatics/Implicature/Basic.lean +++ b/Linglib/Pragmatics/Implicature/Basic.lean @@ -1,4 +1,4 @@ -import Linglib.Core.UD.Word +import Linglib.Core.UniversalDependencies import Linglib.Semantics.Entailment.Polarity /-! diff --git a/Linglib/Semantics/ArgumentStructure/Defs.lean b/Linglib/Semantics/ArgumentStructure/Defs.lean index baa77b721..1eeed3144 100644 --- a/Linglib/Semantics/ArgumentStructure/Defs.lean +++ b/Linglib/Semantics/ArgumentStructure/Defs.lean @@ -1,5 +1,5 @@ import Linglib.Semantics.Events.Basic -import Linglib.Core.UD.Word +import Linglib.Core.UniversalDependencies import Linglib.Semantics.ArgumentStructure.Linking /-! diff --git a/Linglib/Semantics/Aspect/Composition.lean b/Linglib/Semantics/Aspect/Composition.lean index a70549bf1..0f1b10392 100644 --- a/Linglib/Semantics/Aspect/Composition.lean +++ b/Linglib/Semantics/Aspect/Composition.lean @@ -1,5 +1,6 @@ import Linglib.Features.Aktionsart -import Linglib.Core.UD.Word +import Linglib.Core.UniversalDependencies +import Linglib.Features.MassCount /-! # VP-Level Situation Type Composition diff --git a/Linglib/Semantics/Dynamic/DiscourseRef.lean b/Linglib/Semantics/Dynamic/DiscourseRef.lean index 291fa43d6..d571de82f 100644 --- a/Linglib/Semantics/Dynamic/DiscourseRef.lean +++ b/Linglib/Semantics/Dynamic/DiscourseRef.lean @@ -47,8 +47,9 @@ This separation enables anaphora to indefinites under negation: -/ -import Linglib.Core.UD.Word +import Linglib.Core.UniversalDependencies import Linglib.Semantics.Dynamic.Connectives.CCP +import Linglib.Features.MassCount import Mathlib.Data.Fintype.Basic diff --git a/Linglib/Semantics/Kinds/Anaphora.lean b/Linglib/Semantics/Kinds/Anaphora.lean index 6858a58f2..dcd163271 100644 --- a/Linglib/Semantics/Kinds/Anaphora.lean +++ b/Linglib/Semantics/Kinds/Anaphora.lean @@ -1,269 +1,270 @@ -import Linglib.Semantics.Kinds.NominalMappingParameter -import Linglib.Semantics.Dynamic.DiscourseRef -import Linglib.Semantics.Dynamic.Connectives.Defs -import Linglib.Core.Assignment - -/-! -# Kind Anaphora: Static-Dynamic Bridge -[krifka-2026] - -Bridges the static kind semantics in [chierchia-1998] (∩, ⊔, `IsMass`, -`kindAnaphorMass`, `kindAnaphorCount`) with the dynamic concept discourse -referent types in `DiscourseRef` (`ConceptDRef`, `DRefVal`). - -Both modules share `MassCount` from `Core.Lexical.Word`, which models the -morphosyntactic mass/count feature that determines kind-anaphor pronoun -selection (*it* for [MASS], *they* for [COUNT]). - -## Core insight - -[krifka-2026] proposes that head nouns introduce **concept discourse -referents** — properties annotated with a [MASS]/[COUNT] feature. Kind anaphors -pick up these concept drefs and derive kind individuals via Chierchia's ∩ -operator: - -- *it* picks up [MASS] concepts: ⟦it⟧ = λP[MASS]. ∩P -- *they* picks up [COUNT] concepts: ⟦they⟧ = λP[COUNT]. ∩(⊔P) - -Concept drefs **project past anaphoric islands** (negation, modals, -conditionals) because they are presupposed in the input assignment, -not existentially introduced. This is what licenses: - - *John doesn't own a dog. He is afraid of them.* - -while blocking: - - *John doesn't own a dog. \*It is friendly.* - -## Sections - -1. Kind anaphor selection by mass/count feature -2. Concept dref projection past anaphoric islands --/ - -namespace Semantics.Kinds.Anaphora - -open Semantics.Kinds.NMP (Kind Property IsMass - kindAnaphorMass kindAnaphorCount kindAnaphorCount_mass) -open Semantics.Dynamic.Core (ConceptDRef DRefVal) - --- ════════════════════════════════════════════════════ --- § 1. Kind Anaphor Selection --- ════════════════════════════════════════════════════ - -/-- Select the kind-anaphor operator based on the morphosyntactic mass/count feature. - - [krifka-2026] (17a,b): - - ⟦it⟧ = λP[MASS]. λi. ∩P(i) → `kindAnaphorMass` - - ⟦they⟧ = λP[COUNT]. λi. ∩(⊔P)(i) → `kindAnaphorCount` - - The [MASS]/[COUNT] feature determines the pronoun form and whether - plural closure (⊔) applies before nominalization (∩). -/ -def selectKindAnaphor (World Atom : Type) (feature : MassCount) - (P : Property World Atom) : Kind World Atom := - match feature with - | .mass => kindAnaphorMass World Atom P - | .count => kindAnaphorCount World Atom P - -/-- For mass properties, both anaphor paths yield the same kind. - - [krifka-2026] (16): ⊔⊔S = ⊔S for cumulative S (absorption rule). - Since mass nouns are cumulative, plural closure is a no-op, so - `kindAnaphorCount P = kindAnaphorMass P` when P is mass. - - This means the [MASS]/[COUNT] feature's only role is selecting - pronoun morphology — the semantic content of the kind anaphor - is identical for mass properties. -/ -theorem selectKindAnaphor_mass_absorb {World Atom : Type} - (P : Property World Atom) (hMass : IsMass World Atom P) : - selectKindAnaphor World Atom .count P = - selectKindAnaphor World Atom .mass P := - kindAnaphorCount_mass World Atom P hMass - - --- ════════════════════════════════════════════════════ --- § 2. Concept DRef Projection past Anaphoric Islands --- ════════════════════════════════════════════════════ - -section Projection - -variable {W E : Type*} - -/-- Heterogeneous assignment: maps indices to discourse referent values. - - Following [krifka-2026] §4: assignments are partial functions - from ℕ to a heterogeneous universe including entities, concepts - (properties with mass/count features), and world-time indices. Partiality - is modeled by `DRefVal.undef`, so this is `Core.Assignment (DRefVal W E)` - rather than `Core.PartialAssign (DRefVal W E)`. -/ -abbrev HAssign (W E : Type*) := Core.Assignment (DRefVal W E) - -/-- Dynamic sentence meaning: relation between input and output assignments. - - [krifka-2026] §4: meanings of type **aast** map input assignment g - to output assignment h relative to a world-time index i. We omit the - index parameter for the projection theorems since it is orthogonal - to the island-escaping behavior. -/ -def DSent (W E : Type*) := HAssign W E → HAssign W E → Prop - -/-- DPL-style negation: test (output = input) plus denial of body. - - [krifka-2026] (34): ⟦NEG⟧ = λp.λghi[g=h, ¬∃k[g≤k, p(gki)]] - - Negation is a *test*: it preserves the input assignment (g = h) and - checks that no extension of g satisfies the body. This is why - entity drefs introduced under negation are inaccessible — they - exist only in the existentially bound extension k. -/ -def dNeg (φ : DSent W E) : DSent W E := - λ g h => g = h ∧ ¬∃ k, φ g k - -/-- Existential introduction of an entity dref at index n. - - Models the indexed determiner *a*₃ in [krifka-2026] (40c,e): - the determiner introduces a new entity dref (index 3) that falls - under the concept property (index 2). -/ -def entityIntro (n : Nat) (body : DSent W E) : DSent W E := - λ g h => ∃ e : E, body (λ m => if m = n then .entity e else g m) h - -/-- Concept presupposition: the input assignment must already contain - a concept dref at index n. - - Models how head nouns introduce concept drefs *presuppositionally* - in [krifka-2026] §4 — they behave like names. The indexed - head noun *dog*₂ in (40d) is interpreted as a dynamic predicate - of type **eaast** that *presupposes* dref 2 is anchored to the - property 'dog'. Unlike entity drefs (existentially introduced by - the determiner), concept drefs are conditions on the INPUT - assignment, making them globally accessible. -/ -def conceptPresup (n : Nat) (c : ConceptDRef W E) (body : DSent W E) : - DSent W E := - λ g h => g n = .concept c ∧ body g h - -/-- After negation, every index in the output has the same value as - in the input. This is the fundamental property of negation-as-test. -/ -theorem dNeg_preserves (φ : DSent W E) {g h : HAssign W E} - (hNeg : dNeg φ g h) (n : Nat) : - h n = g n := - congr_fun hNeg.1.symm n - -/-- **Concept drefs survive negation.** - - If a concept dref was presupposed in the input, it remains accessible - in the output of a negated sentence. - - [krifka-2026] §3, §4: - *John doesn't own a dog.* introduces concept dref x₂ for 'dog' - in the main box / input assignment. After negation, x₂ persists, - licensing continuations like *He is afraid of them₂.* - - Proof: negation forces h = g (test), so h(n) = g(n) = .concept c. -/ -theorem concept_survives_negation {n : Nat} {c : ConceptDRef W E} - {body : DSent W E} {g h : HAssign W E} - (hPresup : g n = .concept c) - (hNeg : dNeg body g h) : - h n = .concept c := - (dNeg_preserves body hNeg n).trans hPresup - -/-- **Entity drefs die under negation.** - - Entity drefs introduced by indefinites under negation are inaccessible - in the output: the existentially introduced entity exists only in the - local extension k, which is bound under ¬∃. - - [krifka-2026] §4: after *John doesn't own [a₃ dog₂]*, - index 3 (the entity dref for the dog John might own) is NOT in the - output assignment, because it was introduced by ∃k (the determiner) - under ¬ (the negation operator). - - Formally: negation forces h = g, and since the entity was NEWLY - introduced at n (novelty: g(n) = .undef), the output h(n) = .undef. -/ -theorem entity_trapped_by_negation {n : Nat} - {body : DSent W E} {g h : HAssign W E} - (hNeg : dNeg (entityIntro n body) g h) - (hNovel : g n = .undef) : - h n = .undef := - (dNeg_preserves (entityIntro n body) hNeg n).trans hNovel - -/-- The asymmetry between concept and entity drefs under negation. - - In the same sentence *John₁ doesn't own [a₃ dog₂]*, the concept - dref at index 2 survives while the entity dref at index 3 does not. - - This theorem combines the two projection results. -/ -theorem concept_entity_asymmetry - {nConcept nEntity : Nat} - {c : ConceptDRef W E} - {φ : DSent W E} {g h : HAssign W E} - (hPresup : g nConcept = .concept c) - (hNovel : g nEntity = .undef) - (hNeg : dNeg φ g h) : - h nConcept = .concept c ∧ h nEntity = .undef := - ⟨concept_survives_negation hPresup hNeg, - (dNeg_preserves φ hNeg nEntity).trans hNovel⟩ - -end Projection - - --- ════════════════════════════════════════════════════ --- § 3. DPL Bridge --- ════════════════════════════════════════════════════ - -section DPLBridge - -open Semantics.Dynamic.Core.DynProp (Update dneg test) -open _root_.Core (Assignment) - -variable {W E : Type*} - -/-- Embed a homogeneous DPL-style assignment (`Assignment E = Nat → E`, - [groenendijk-stokhof-1991]) into a heterogeneous Krifka-style - assignment (`Nat → DRefVal W E`) by wrapping every value in `.entity`. -/ -def embedAssign (g : Assignment E) : HAssign W E := - λ n => .entity (g n) - -/-- Lift a DPL-style relation (`Update (Assignment E)`) to operate on - heterogeneous assignments via the entity embedding. -/ -def liftDPL (φ : Update (Assignment E)) : DSent W E := - λ g h => ∃ g' h' : Assignment E, embedAssign g' = g ∧ embedAssign h' = h ∧ φ g' h' - -/-- `dNeg` and `test (dneg φ)` (the substrate form of [groenendijk-stokhof-1991]'s - DPL negation) have identical structure. - - Both are: `λ g h => g = h ∧ ¬∃ k, φ g k`. - [krifka-2026]'s negation (34) generalizes DPL negation from homogeneous - (`Nat → E`) to heterogeneous (`Nat → DRefVal W E`) assignments. The structure - is preserved because the projection mechanism depends only on `g = h`. -/ -theorem dNeg_structure (φ : DSent W E) (g h : HAssign W E) : - dNeg φ g h ↔ (g = h ∧ ¬∃ k, φ g k) := - Iff.rfl - -theorem dplNeg_structure (φ : Update (Assignment E)) (g h : Assignment E) : - test (dneg φ) g h ↔ (g = h ∧ ¬∃ k, φ g k) := by - simp only [test, dneg] - exact ⟨fun ⟨heq, hneg⟩ => ⟨heq, heq ▸ hneg⟩, - fun ⟨heq, hneg⟩ => ⟨heq, heq ▸ hneg⟩⟩ - -/-- Negation commutes with the DPL→heterogeneous embedding. - - Lifting a DPL-style negation produces the same result as negating the - lifted relation, modulo the entity-only constraint on assignments. -/ -theorem liftDPL_neg (φ : Update (Assignment E)) (g h : HAssign W E) : - liftDPL (W := W) (test (dneg φ)) g h → - dNeg (liftDPL (W := W) φ) g h := by - intro ⟨g', h', hg, hh, hEq, hNex⟩ - -- hEq : g' = h' (test's first conjunct) - -- hNex : ¬∃ k, φ h' k (test (dneg φ) puts the dneg-condition at the second arg) - refine ⟨?_, ?_⟩ - · rw [← hg, ← hh]; exact congrArg embedAssign hEq - · intro ⟨k, g'', h'', hg'', hk, hφ⟩ - rw [← hg] at hg'' - have hgeq : g' = g'' := by - have := congrFun hg''.symm - funext n; have := this n; simp [embedAssign] at this; exact this - -- h' = g' (hEq.symm) = g'' (hgeq), so hφ : φ g'' h'' ↦ φ h' h'' - have hh'eq : h' = g'' := hEq.symm.trans hgeq - exact hNex ⟨h'', hh'eq ▸ hφ⟩ - -end DPLBridge - -end Semantics.Kinds.Anaphora +import Linglib.Semantics.Kinds.NominalMappingParameter +import Linglib.Semantics.Dynamic.DiscourseRef +import Linglib.Semantics.Dynamic.Connectives.Defs +import Linglib.Core.Assignment +import Linglib.Features.MassCount + +/-! +# Kind Anaphora: Static-Dynamic Bridge +[krifka-2026] + +Bridges the static kind semantics in [chierchia-1998] (∩, ⊔, `IsMass`, +`kindAnaphorMass`, `kindAnaphorCount`) with the dynamic concept discourse +referent types in `DiscourseRef` (`ConceptDRef`, `DRefVal`). + +Both modules share `MassCount` from `Core.Lexical.Word`, which models the +morphosyntactic mass/count feature that determines kind-anaphor pronoun +selection (*it* for [MASS], *they* for [COUNT]). + +## Core insight + +[krifka-2026] proposes that head nouns introduce **concept discourse +referents** — properties annotated with a [MASS]/[COUNT] feature. Kind anaphors +pick up these concept drefs and derive kind individuals via Chierchia's ∩ +operator: + +- *it* picks up [MASS] concepts: ⟦it⟧ = λP[MASS]. ∩P +- *they* picks up [COUNT] concepts: ⟦they⟧ = λP[COUNT]. ∩(⊔P) + +Concept drefs **project past anaphoric islands** (negation, modals, +conditionals) because they are presupposed in the input assignment, +not existentially introduced. This is what licenses: + + *John doesn't own a dog. He is afraid of them.* + +while blocking: + + *John doesn't own a dog. \*It is friendly.* + +## Sections + +1. Kind anaphor selection by mass/count feature +2. Concept dref projection past anaphoric islands +-/ + +namespace Semantics.Kinds.Anaphora + +open Semantics.Kinds.NMP (Kind Property IsMass + kindAnaphorMass kindAnaphorCount kindAnaphorCount_mass) +open Semantics.Dynamic.Core (ConceptDRef DRefVal) + +-- ════════════════════════════════════════════════════ +-- § 1. Kind Anaphor Selection +-- ════════════════════════════════════════════════════ + +/-- Select the kind-anaphor operator based on the morphosyntactic mass/count feature. + + [krifka-2026] (17a,b): + - ⟦it⟧ = λP[MASS]. λi. ∩P(i) → `kindAnaphorMass` + - ⟦they⟧ = λP[COUNT]. λi. ∩(⊔P)(i) → `kindAnaphorCount` + + The [MASS]/[COUNT] feature determines the pronoun form and whether + plural closure (⊔) applies before nominalization (∩). -/ +def selectKindAnaphor (World Atom : Type) (feature : MassCount) + (P : Property World Atom) : Kind World Atom := + match feature with + | .mass => kindAnaphorMass World Atom P + | .count => kindAnaphorCount World Atom P + +/-- For mass properties, both anaphor paths yield the same kind. + + [krifka-2026] (16): ⊔⊔S = ⊔S for cumulative S (absorption rule). + Since mass nouns are cumulative, plural closure is a no-op, so + `kindAnaphorCount P = kindAnaphorMass P` when P is mass. + + This means the [MASS]/[COUNT] feature's only role is selecting + pronoun morphology — the semantic content of the kind anaphor + is identical for mass properties. -/ +theorem selectKindAnaphor_mass_absorb {World Atom : Type} + (P : Property World Atom) (hMass : IsMass World Atom P) : + selectKindAnaphor World Atom .count P = + selectKindAnaphor World Atom .mass P := + kindAnaphorCount_mass World Atom P hMass + + +-- ════════════════════════════════════════════════════ +-- § 2. Concept DRef Projection past Anaphoric Islands +-- ════════════════════════════════════════════════════ + +section Projection + +variable {W E : Type*} + +/-- Heterogeneous assignment: maps indices to discourse referent values. + + Following [krifka-2026] §4: assignments are partial functions + from ℕ to a heterogeneous universe including entities, concepts + (properties with mass/count features), and world-time indices. Partiality + is modeled by `DRefVal.undef`, so this is `Core.Assignment (DRefVal W E)` + rather than `Core.PartialAssign (DRefVal W E)`. -/ +abbrev HAssign (W E : Type*) := Core.Assignment (DRefVal W E) + +/-- Dynamic sentence meaning: relation between input and output assignments. + + [krifka-2026] §4: meanings of type **aast** map input assignment g + to output assignment h relative to a world-time index i. We omit the + index parameter for the projection theorems since it is orthogonal + to the island-escaping behavior. -/ +def DSent (W E : Type*) := HAssign W E → HAssign W E → Prop + +/-- DPL-style negation: test (output = input) plus denial of body. + + [krifka-2026] (34): ⟦NEG⟧ = λp.λghi[g=h, ¬∃k[g≤k, p(gki)]] + + Negation is a *test*: it preserves the input assignment (g = h) and + checks that no extension of g satisfies the body. This is why + entity drefs introduced under negation are inaccessible — they + exist only in the existentially bound extension k. -/ +def dNeg (φ : DSent W E) : DSent W E := + λ g h => g = h ∧ ¬∃ k, φ g k + +/-- Existential introduction of an entity dref at index n. + + Models the indexed determiner *a*₃ in [krifka-2026] (40c,e): + the determiner introduces a new entity dref (index 3) that falls + under the concept property (index 2). -/ +def entityIntro (n : Nat) (body : DSent W E) : DSent W E := + λ g h => ∃ e : E, body (λ m => if m = n then .entity e else g m) h + +/-- Concept presupposition: the input assignment must already contain + a concept dref at index n. + + Models how head nouns introduce concept drefs *presuppositionally* + in [krifka-2026] §4 — they behave like names. The indexed + head noun *dog*₂ in (40d) is interpreted as a dynamic predicate + of type **eaast** that *presupposes* dref 2 is anchored to the + property 'dog'. Unlike entity drefs (existentially introduced by + the determiner), concept drefs are conditions on the INPUT + assignment, making them globally accessible. -/ +def conceptPresup (n : Nat) (c : ConceptDRef W E) (body : DSent W E) : + DSent W E := + λ g h => g n = .concept c ∧ body g h + +/-- After negation, every index in the output has the same value as + in the input. This is the fundamental property of negation-as-test. -/ +theorem dNeg_preserves (φ : DSent W E) {g h : HAssign W E} + (hNeg : dNeg φ g h) (n : Nat) : + h n = g n := + congr_fun hNeg.1.symm n + +/-- **Concept drefs survive negation.** + + If a concept dref was presupposed in the input, it remains accessible + in the output of a negated sentence. + + [krifka-2026] §3, §4: + *John doesn't own a dog.* introduces concept dref x₂ for 'dog' + in the main box / input assignment. After negation, x₂ persists, + licensing continuations like *He is afraid of them₂.* + + Proof: negation forces h = g (test), so h(n) = g(n) = .concept c. -/ +theorem concept_survives_negation {n : Nat} {c : ConceptDRef W E} + {body : DSent W E} {g h : HAssign W E} + (hPresup : g n = .concept c) + (hNeg : dNeg body g h) : + h n = .concept c := + (dNeg_preserves body hNeg n).trans hPresup + +/-- **Entity drefs die under negation.** + + Entity drefs introduced by indefinites under negation are inaccessible + in the output: the existentially introduced entity exists only in the + local extension k, which is bound under ¬∃. + + [krifka-2026] §4: after *John doesn't own [a₃ dog₂]*, + index 3 (the entity dref for the dog John might own) is NOT in the + output assignment, because it was introduced by ∃k (the determiner) + under ¬ (the negation operator). + + Formally: negation forces h = g, and since the entity was NEWLY + introduced at n (novelty: g(n) = .undef), the output h(n) = .undef. -/ +theorem entity_trapped_by_negation {n : Nat} + {body : DSent W E} {g h : HAssign W E} + (hNeg : dNeg (entityIntro n body) g h) + (hNovel : g n = .undef) : + h n = .undef := + (dNeg_preserves (entityIntro n body) hNeg n).trans hNovel + +/-- The asymmetry between concept and entity drefs under negation. + + In the same sentence *John₁ doesn't own [a₃ dog₂]*, the concept + dref at index 2 survives while the entity dref at index 3 does not. + + This theorem combines the two projection results. -/ +theorem concept_entity_asymmetry + {nConcept nEntity : Nat} + {c : ConceptDRef W E} + {φ : DSent W E} {g h : HAssign W E} + (hPresup : g nConcept = .concept c) + (hNovel : g nEntity = .undef) + (hNeg : dNeg φ g h) : + h nConcept = .concept c ∧ h nEntity = .undef := + ⟨concept_survives_negation hPresup hNeg, + (dNeg_preserves φ hNeg nEntity).trans hNovel⟩ + +end Projection + + +-- ════════════════════════════════════════════════════ +-- § 3. DPL Bridge +-- ════════════════════════════════════════════════════ + +section DPLBridge + +open Semantics.Dynamic.Core.DynProp (Update dneg test) +open _root_.Core (Assignment) + +variable {W E : Type*} + +/-- Embed a homogeneous DPL-style assignment (`Assignment E = Nat → E`, + [groenendijk-stokhof-1991]) into a heterogeneous Krifka-style + assignment (`Nat → DRefVal W E`) by wrapping every value in `.entity`. -/ +def embedAssign (g : Assignment E) : HAssign W E := + λ n => .entity (g n) + +/-- Lift a DPL-style relation (`Update (Assignment E)`) to operate on + heterogeneous assignments via the entity embedding. -/ +def liftDPL (φ : Update (Assignment E)) : DSent W E := + λ g h => ∃ g' h' : Assignment E, embedAssign g' = g ∧ embedAssign h' = h ∧ φ g' h' + +/-- `dNeg` and `test (dneg φ)` (the substrate form of [groenendijk-stokhof-1991]'s + DPL negation) have identical structure. + + Both are: `λ g h => g = h ∧ ¬∃ k, φ g k`. + [krifka-2026]'s negation (34) generalizes DPL negation from homogeneous + (`Nat → E`) to heterogeneous (`Nat → DRefVal W E`) assignments. The structure + is preserved because the projection mechanism depends only on `g = h`. -/ +theorem dNeg_structure (φ : DSent W E) (g h : HAssign W E) : + dNeg φ g h ↔ (g = h ∧ ¬∃ k, φ g k) := + Iff.rfl + +theorem dplNeg_structure (φ : Update (Assignment E)) (g h : Assignment E) : + test (dneg φ) g h ↔ (g = h ∧ ¬∃ k, φ g k) := by + simp only [test, dneg] + exact ⟨fun ⟨heq, hneg⟩ => ⟨heq, heq ▸ hneg⟩, + fun ⟨heq, hneg⟩ => ⟨heq, heq ▸ hneg⟩⟩ + +/-- Negation commutes with the DPL→heterogeneous embedding. + + Lifting a DPL-style negation produces the same result as negating the + lifted relation, modulo the entity-only constraint on assignments. -/ +theorem liftDPL_neg (φ : Update (Assignment E)) (g h : HAssign W E) : + liftDPL (W := W) (test (dneg φ)) g h → + dNeg (liftDPL (W := W) φ) g h := by + intro ⟨g', h', hg, hh, hEq, hNex⟩ + -- hEq : g' = h' (test's first conjunct) + -- hNex : ¬∃ k, φ h' k (test (dneg φ) puts the dneg-condition at the second arg) + refine ⟨?_, ?_⟩ + · rw [← hg, ← hh]; exact congrArg embedAssign hEq + · intro ⟨k, g'', h'', hg'', hk, hφ⟩ + rw [← hg] at hg'' + have hgeq : g' = g'' := by + have := congrFun hg''.symm + funext n; have := this n; simp [embedAssign] at this; exact this + -- h' = g' (hEq.symm) = g'' (hgeq), so hφ : φ g'' h'' ↦ φ h' h'' + have hh'eq : h' = g'' := hEq.symm.trans hgeq + exact hNex ⟨h'', hh'eq ▸ hφ⟩ + +end DPLBridge + +end Semantics.Kinds.Anaphora diff --git a/Linglib/Semantics/Kinds/MeaningPreservation.lean b/Linglib/Semantics/Kinds/MeaningPreservation.lean index 271b16602..e1c04f176 100644 --- a/Linglib/Semantics/Kinds/MeaningPreservation.lean +++ b/Linglib/Semantics/Kinds/MeaningPreservation.lean @@ -1,3 +1,5 @@ +import Linglib.Semantics.Kinds.NominalMappingParameter +import Linglib.Features.MassCount /- # Kind Reference and Number Marking @@ -42,7 +44,6 @@ partition are disjoint) is derived there. -/ -import Linglib.Semantics.Kinds.NominalMappingParameter namespace Semantics.Kinds.MeaningPreservation diff --git a/Linglib/Semantics/Kinds/NominalMappingParameter.lean b/Linglib/Semantics/Kinds/NominalMappingParameter.lean index 19cc63bbe..246a9c654 100644 --- a/Linglib/Semantics/Kinds/NominalMappingParameter.lean +++ b/Linglib/Semantics/Kinds/NominalMappingParameter.lean @@ -32,10 +32,11 @@ come from Mathlib for free, giving us Link's semilattice directly. -/ +import Linglib.Features.MassCount import Mathlib.Data.Set.Basic import Mathlib.Data.Fintype.Basic import Mathlib.Order.UpperLower.Basic -import Linglib.Core.UD.Word +import Linglib.Core.UniversalDependencies import Linglib.Core.Mereology import Linglib.Core.Logic.Intensional.Rigidity diff --git a/Linglib/Semantics/Mood/ClauseType.lean b/Linglib/Semantics/Mood/ClauseType.lean index 187f9a95f..31ee2d4a3 100644 --- a/Linglib/Semantics/Mood/ClauseType.lean +++ b/Linglib/Semantics/Mood/ClauseType.lean @@ -1,7 +1,7 @@ import Linglib.Semantics.Mood.Basic import Linglib.Semantics.Mood.IllocutionaryMood import Linglib.Discourse.Roles -import Linglib.Core.UD.Basic +import Linglib.Core.UniversalDependencies /-! # Clause Type: Force × Mood diff --git a/Linglib/Semantics/Quantification/Lexicon.lean b/Linglib/Semantics/Quantification/Lexicon.lean index 3c1c96131..3cb598a17 100644 --- a/Linglib/Semantics/Quantification/Lexicon.lean +++ b/Linglib/Semantics/Quantification/Lexicon.lean @@ -1,4 +1,4 @@ -import Linglib.Core.UD.Word +import Linglib.Core.UniversalDependencies /-! # Quantifier lexicon — shared structure diff --git a/Linglib/Semantics/TypeTheoretic/Basic.lean b/Linglib/Semantics/TypeTheoretic/Basic.lean index c539c10e7..8ff4bbdb6 100644 --- a/Linglib/Semantics/TypeTheoretic/Basic.lean +++ b/Linglib/Semantics/TypeTheoretic/Basic.lean @@ -2,7 +2,7 @@ import Mathlib.Data.Set.Basic import Linglib.Core.Logic.Intensional.Rigidity import Linglib.Discourse.CommonGround import Linglib.Semantics.Presupposition.Basic -import Linglib.Core.UD.Basic +import Linglib.Core.UniversalDependencies /-! # Type Theory with Records — Core Foundations diff --git a/Linglib/Studies/AissenPolian2025.lean b/Linglib/Studies/AissenPolian2025.lean index 8a3d7cb0e..144887d12 100644 --- a/Linglib/Studies/AissenPolian2025.lean +++ b/Linglib/Studies/AissenPolian2025.lean @@ -3,6 +3,7 @@ import Linglib.Morphology.DM.NominalStructure import Linglib.Syntax.Minimalist.Agree import Linglib.Syntax.Binding.SpecificityCondition import Linglib.Features.InformationStructure +import Linglib.Typology.WordOrder /-! # Aissen & Polian 2025: Possessor Extraction and Categorical Subject in Tseltalan diff --git a/Linglib/Studies/AlexeyenkoZeijlstra2025.lean b/Linglib/Studies/AlexeyenkoZeijlstra2025.lean index 133c0fd3c..6fcb17b9f 100644 --- a/Linglib/Studies/AlexeyenkoZeijlstra2025.lean +++ b/Linglib/Studies/AlexeyenkoZeijlstra2025.lean @@ -1,4 +1,4 @@ -import Linglib.Core.UD.Word +import Linglib.Core.UniversalDependencies import Linglib.Data.WALS.Features.F87A import Linglib.Syntax.Minimalist.Modification import Linglib.Fragments.Greek.StandardModern.AdjAgreement diff --git a/Linglib/Studies/AnandHardtMcCloskey2021.lean b/Linglib/Studies/AnandHardtMcCloskey2021.lean index 65baa7de2..383acc3b4 100644 --- a/Linglib/Studies/AnandHardtMcCloskey2021.lean +++ b/Linglib/Studies/AnandHardtMcCloskey2021.lean @@ -1,4 +1,4 @@ -import Linglib.Core.UD.Word +import Linglib.Core.UniversalDependencies import Linglib.Phenomena.Ellipsis.Sluicing import Linglib.Syntax.Minimalist.Ellipsis.FormalMatching import Linglib.Syntax.Minimalist.Ellipsis.DeletionDomain diff --git a/Linglib/Studies/Borer2005.lean b/Linglib/Studies/Borer2005.lean index 0c40dbecb..0598540a1 100644 --- a/Linglib/Studies/Borer2005.lean +++ b/Linglib/Studies/Borer2005.lean @@ -1,6 +1,7 @@ import Linglib.Core.Mereology import Linglib.Typology.ClassifierSystem import Linglib.Syntax.Minimalist.ExtendedProjection.Basic +import Linglib.Features.MassCount /-! # Nominal Syntax-Semantics Mapping diff --git a/Linglib/Studies/Cacchioli2025.lean b/Linglib/Studies/Cacchioli2025.lean index be182d0a5..0de9a74c3 100644 --- a/Linglib/Studies/Cacchioli2025.lean +++ b/Linglib/Studies/Cacchioli2025.lean @@ -1,4 +1,4 @@ -import Linglib.Core.UD.Word +import Linglib.Core.UniversalDependencies import Linglib.Syntax.Minimalist.Agree import Linglib.Typology.Complementation import Linglib.Fragments.Tigrinya.ClausePrefixes diff --git a/Linglib/Studies/FillmoreKayOConnor1988.lean b/Linglib/Studies/FillmoreKayOConnor1988.lean index 17bfbe8cc..dc107e285 100644 --- a/Linglib/Studies/FillmoreKayOConnor1988.lean +++ b/Linglib/Studies/FillmoreKayOConnor1988.lean @@ -1,4 +1,4 @@ -import Linglib.Core.UD.Word +import Linglib.Core.UniversalDependencies import Linglib.Features.Acceptability import Linglib.Syntax.ConstructionGrammar.Studies.FillmoreKayOConnor1988 import Linglib.Typology.PolarityItem diff --git a/Linglib/Studies/Gibson2025.lean b/Linglib/Studies/Gibson2025.lean index 9d4829352..7f5b30a2e 100644 --- a/Linglib/Studies/Gibson2025.lean +++ b/Linglib/Studies/Gibson2025.lean @@ -1,6 +1,7 @@ import Linglib.Syntax.DependencyGrammar.Formal.HarmonicOrder import Linglib.Data.WALS.Features.F95A -import Linglib.Core.UD.Word +import Linglib.Core.UniversalDependencies +import Linglib.Typology.WordOrder /-! # Gibson 2025: DLM and the Head-Direction Generalization diff --git a/Linglib/Studies/Gotham2017.lean b/Linglib/Studies/Gotham2017.lean index fd93b9900..fe9b8fe97 100644 --- a/Linglib/Studies/Gotham2017.lean +++ b/Linglib/Studies/Gotham2017.lean @@ -1,4 +1,4 @@ -import Linglib.Core.UD.Word +import Linglib.Core.UniversalDependencies /-! # Copredication: [gotham-2017]'s account + bridge data diff --git a/Linglib/Studies/HalpertHammerly2026.lean b/Linglib/Studies/HalpertHammerly2026.lean index 217418830..ffaf6691c 100644 --- a/Linglib/Studies/HalpertHammerly2026.lean +++ b/Linglib/Studies/HalpertHammerly2026.lean @@ -135,7 +135,7 @@ theorem participant_implies_animate (pf : ProminenceFeatures) | false => simp [ProminenceFeatures.wellFormed] at hw /-- First person is necessarily human and animate. -/ -theorem first_person_is_human_animate : +theorem firstF_person_is_human_animate : ∀ pf : ProminenceFeatures, pf.wellFormed = true → pf.hasAuthor = true → pf.isHuman = true ∧ pf.isAnimate = true := by @@ -153,9 +153,9 @@ theorem first_person_is_human_animate : This is not a coincidence: they are fragments of the same containment hierarchy ([hammerly-2023]). -/ theorem person_animacy_same_structure : - (Features.PhiFeatures.toPair Features.Person.first).wellFormed = true ∧ + (Features.PhiFeatures.toPair Features.Person.firstF).wellFormed = true ∧ (Features.PhiFeatures.toPair AnimacyFeatures.human).wellFormed = true ∧ - (Features.PhiFeatures.toPair Features.Person.third).wellFormed = true ∧ + (Features.PhiFeatures.toPair Features.Person.thirdF).wellFormed = true ∧ (Features.PhiFeatures.toPair AnimacyFeatures.inanimate).wellFormed = true := ⟨rfl, rfl, rfl, rfl⟩ diff --git a/Linglib/Studies/Harbour2016.lean b/Linglib/Studies/Harbour2016.lean index e3220660c..ef4952297 100644 --- a/Linglib/Studies/Harbour2016.lean +++ b/Linglib/Studies/Harbour2016.lean @@ -240,10 +240,10 @@ open Features.Number (singularF dualF pluralF) hierarchy in [bejar-rezac-2009]'s Cyclic Agree and [preminger-2014]'s relativized probing. -/ theorem person_hierarchy_is_spec_ordering : - PhiFeatures.specLevel Features.Person.first > - PhiFeatures.specLevel Features.Person.second ∧ - PhiFeatures.specLevel Features.Person.second > - PhiFeatures.specLevel Features.Person.third := + PhiFeatures.specLevel Features.Person.firstF > + PhiFeatures.specLevel Features.Person.secondF ∧ + PhiFeatures.specLevel Features.Person.secondF > + PhiFeatures.specLevel Features.Person.thirdF := PhiFeatures.specLevel_strict_order Features.Person.first_is_maximal Features.Person.second_is_intermediate Features.Person.third_is_minimal diff --git a/Linglib/Studies/Haspelmath1997Polarity.lean b/Linglib/Studies/Haspelmath1997Polarity.lean index 8b47ccd7d..502b77aa5 100644 --- a/Linglib/Studies/Haspelmath1997Polarity.lean +++ b/Linglib/Studies/Haspelmath1997Polarity.lean @@ -1,4 +1,4 @@ -import Linglib.Core.UD.Word +import Linglib.Core.UniversalDependencies import Linglib.Data.WALS.Aggregation import Linglib.Data.WALS.Features.F46A import Linglib.Typology.PolarityItem diff --git a/Linglib/Studies/KehlerRohde2013.lean b/Linglib/Studies/KehlerRohde2013.lean index 5970ec0e8..7060aef20 100644 --- a/Linglib/Studies/KehlerRohde2013.lean +++ b/Linglib/Studies/KehlerRohde2013.lean @@ -1,5 +1,5 @@ import Linglib.Discourse.Coherence -import Linglib.Core.UD.Basic +import Linglib.Core.UniversalDependencies import Linglib.Discourse.Centering.Rule1 import Linglib.Discourse.Centering.Instances.GrammaticalRole diff --git a/Linglib/Studies/Krifka2026.lean b/Linglib/Studies/Krifka2026.lean index 5b3dfecc3..68509b029 100644 --- a/Linglib/Studies/Krifka2026.lean +++ b/Linglib/Studies/Krifka2026.lean @@ -1,213 +1,214 @@ -import Linglib.Semantics.Kinds.Anaphora - -/-! -# Anaphora for Concepts, Kinds, and Parts -[krifka-2026] - -Empirical data and verification theorems for [krifka-2026]'s theory -of concept discourse referents. Three types of anaphora are distinguished: - -| Type | Pronoun | Picks up | Example | -|------|---------|----------|---------| -| Entity | *he/she/it* | individual dref | *A dog₃ came in. It₃ barked.* | -| Concept | *one*, empty NP | concept dref | *John has a big dog₂. Mary has a small one₂.* | -| Kind | *it*[MASS], *they*[COUNT] | concept dref → kind | *John owns a dog₂. They₂ are loyal.* | - -## Key empirical claims - -1. **Concept drefs project past anaphoric islands** — negation, modals, - conditionals cannot trap concept drefs (unlike entity drefs) -2. **Mass/count feature determines kind pronoun** — *it* for [MASS], - *they* for [COUNT], independent of ontology -3. **Kind anaphora ≠ concept anaphora** — kind anaphors derive kind - individuals via ∩ (and ⊔ for count), concept anaphors reuse the property - -## End-to-End Example - -Section 3 constructs a concrete model of examples (44)–(45): - -``` -John₁ doesn't own [DP a₃ [NP dog]₂]. - → concept dref x₂ ('dog'[COUNT]) persists in output - → entity dref x₃ (the dog) is trapped under ¬∃ -He₁ is afraid of them₂,₄. - → kind anaphor picks up concept x₂ (accessible!) - → derives kind individual via ∩(⊔⟦dog⟧) -``` --/ - -namespace Krifka2026 - -open Semantics.Dynamic.Core (ConceptDRef DRefVal) -open Semantics.Kinds.Anaphora - --- ════════════════════════════════════════════════════ --- § 1. Kind Pronoun Selection --- ════════════════════════════════════════════════════ - -/-- Kind-anaphoric pronouns, selected by the [MASS]/[COUNT] feature. -/ -inductive KindPronoun where - | it -- singular, selects [MASS] concepts - | they -- plural, selects [COUNT] concepts - deriving DecidableEq, Repr - -/-- Select kind-anaphoric pronoun from the count feature. - - [krifka-2026] (17a,b): - - ⟦it⟧ = λP[MASS] λi.∩P(i) - - ⟦they⟧ = λP[COUNT] λi.∩⊔P(i) -/ -def selectPronoun : MassCount → KindPronoun - | .mass => .it - | .count => .they - -/-- Example (7a): count noun antecedent → plural kind anaphor *them*. - *John noticed a spider in the bathroom. He has a phobia against them / \*it.* -/ -theorem ex7a_count_them : selectPronoun .count = .they := rfl - -/-- Example (7b): mass noun antecedent → singular kind anaphor *it*. - *John noticed mold in the bathroom. He is allergic against it / \*them.* -/ -theorem ex7b_mass_it : selectPronoun .mass = .it := rfl - -/-- Examples (8a,b): the same individuals (*pollen*[MASS] vs *pollen grains*[COUNT]) - select different pronouns based purely on the morphosyntactic feature. - (8a) *There is a lot of pollen in the air. I am allergic against it / \*them.* - (8b) *There are a lot of pollen grains in the air. I am allergic against them / ??it.* -/ -theorem ex8_feature_determines_pronoun : - selectPronoun .mass ≠ selectPronoun .count := by decide - - --- ════════════════════════════════════════════════════ --- § 2. Concept DRef Projection: Island Escaping --- ════════════════════════════════════════════════════ - -section IslandEscaping - -variable {W E : Type*} - -/-- Examples (5a,c), (25), (44–45): Concept drefs project past negation. - - (5a) *John doesn't own a dog. He is afraid of them. But Mary owns one.* - (5c) *John doesn't own a dog. \*It is friendly.* - - In the DRT representation (25) and dynamic semantics (44–45), the concept - dref x₂ for 'dog' is in the main box / presupposed in the input. After - negation, x₂ persists (licensing *them₂*, *one₂*), but the entity dref - x₃ is trapped under ¬∃ (blocking *\*it₃*). -/ -theorem dog_concept_survives_negation - {dogConcept : ConceptDRef W E} - {φ : DSent W E} - {g h : HAssign W E} - (hDog : g 2 = .concept dogConcept) - (hNovel : g 3 = .undef) - (hNeg : dNeg φ g h) : - h 2 = .concept dogConcept ∧ h 3 = .undef := - concept_entity_asymmetry hDog hNovel hNeg - -end IslandEscaping - - --- ════════════════════════════════════════════════════ --- § 3. End-to-End: "John doesn't own a dog" (44–45) --- ════════════════════════════════════════════════════ - -section EndToEnd - -/-- Concrete entity type for the worked example. -/ -inductive Ent where | john | mary - deriving DecidableEq, Repr - -/-- Concrete world type. A world where John doesn't own a dog. -/ -inductive Wld where | w₀ - deriving DecidableEq, Repr - -/-- The concept 'dog' as a concept dref with [COUNT] feature. - In this model, no entity satisfies the dog predicate (John doesn't own one). -/ -def dogConcept : ConceptDRef Wld Ent where - property := λ _ _ => false -- no dogs in this model - feature := .count - -/-- Initial assignment for (44e): g₁=F(John), g₂=F(dog), F(C)(g₂). - Following [krifka-2026] (40g)/(44e): John's name presupposes - dref 1 is anchored to John; the head noun *dog*₂ presupposes dref 2 - is anchored to the 'dog' concept with [COUNT] feature. -/ -def g₀ : HAssign Wld Ent := λ n => - match n with - | 1 => .entity .john - | 2 => .concept dogConcept - | _ => .undef - -/-- Sentence meaning for "own [DP a₃ [NP dog]₂]": introduces entity dref - at index 3, constrained to satisfy the concept property at index 2. -/ -def ownADog : DSent Wld Ent := entityIntro 3 (λ g h => - g = h ∧ (g 2).liftConceptPred (λ c => c.property .w₀ (match g 3 with - | .entity e => e | _ => .john)) = true) - -/-- "John₁ doesn't own [DP a₃ [NP dog]₂]" as the negation of ownADog. -/ -def doesntOwnADog : DSent Wld Ent := dNeg ownADog - -/-- The negation is satisfiable in this model (no dogs exist). - Output: g₀ = h (test), confirming no entity dref was introduced. -/ -theorem negation_satisfiable : - doesntOwnADog g₀ g₀ := by - refine ⟨rfl, ?_⟩ - intro ⟨k, e, hBody⟩ - simp only [g₀, dogConcept, DRefVal.liftConceptPred] at hBody - obtain ⟨hEq, hProp⟩ := hBody - -- After update, g(2) = g₀(2) = .concept dogConcept, g(3) = .entity e - -- The concept property returns false for all entities - simp at hProp - -/-- **Main result**: after "John doesn't own a dog", the concept dref - for 'dog' at index 2 is accessible while the entity dref at index 3 - remains undefined. This is the concrete instantiation of the asymmetry - predicted by [krifka-2026] §4. -/ -theorem concrete_concept_entity_asymmetry : - ∀ h : HAssign Wld Ent, - doesntOwnADog g₀ h → - h 2 = .concept dogConcept ∧ h 3 = .undef := - λ _ hNeg => concept_entity_asymmetry rfl rfl hNeg - -/-- The kind anaphor *them* selects [COUNT] for dogs, as expected. -/ -theorem dog_kind_pronoun : selectPronoun dogConcept.feature = .they := rfl - -end EndToEnd - - --- ════════════════════════════════════════════════════ --- § 4. Concept vs Kind Anaphora (19a,b) --- ════════════════════════════════════════════════════ - -/-- Anaphoric constructions that pick up concept drefs. - - [krifka-2026] §3 distinguishes concept anaphors (which reuse the - property directly) from kind anaphors (which derive kind individuals - via ∩). Both pick up concept drefs, but they do different things. - - The distinction is testable via examples like (19a,b): - (19a) *John didn't get a dog from the animal shelter downtown. - He is afraid of them.* — kind anaphora (OK: dogs-as-kind) - (19b) *John didn't get a dog from the animal shelter downtown. - But Mary got one.* — concept anaphora (OK: a dog-from-the-shelter) -/ -inductive AnaphoricConstruction where - | emptyNP -- *one*, empty NP: picks up concept property directly - | emptyPP -- partitive *of them*: picks up concept for part-whole - | kindPron -- *it*[MASS], *they*[COUNT]: derives kind via ∩(⊔)P - deriving DecidableEq, Repr - -/-- Whether a construction derives a kind individual or reuses the property. -/ -def derivesKind : AnaphoricConstruction → Bool - | .kindPron => true - | .emptyNP => false - | .emptyPP => false - -/-- Kind pronouns derive kinds; concept anaphors (*one*, empty NP/PP) don't. - This distinction explains (19a) vs (19b): "dogs from the animal shelter" - doesn't name a kind (cf. [carlson-1977]), so kind anaphora yields the - general dog-kind, while concept anaphora preserves the full NP property. -/ -theorem kind_vs_concept_distinction : - derivesKind .kindPron = true ∧ - derivesKind .emptyNP = false ∧ - derivesKind .emptyPP = false := - ⟨rfl, rfl, rfl⟩ - -end Krifka2026 +import Linglib.Semantics.Kinds.Anaphora +import Linglib.Features.MassCount + +/-! +# Anaphora for Concepts, Kinds, and Parts +[krifka-2026] + +Empirical data and verification theorems for [krifka-2026]'s theory +of concept discourse referents. Three types of anaphora are distinguished: + +| Type | Pronoun | Picks up | Example | +|------|---------|----------|---------| +| Entity | *he/she/it* | individual dref | *A dog₃ came in. It₃ barked.* | +| Concept | *one*, empty NP | concept dref | *John has a big dog₂. Mary has a small one₂.* | +| Kind | *it*[MASS], *they*[COUNT] | concept dref → kind | *John owns a dog₂. They₂ are loyal.* | + +## Key empirical claims + +1. **Concept drefs project past anaphoric islands** — negation, modals, + conditionals cannot trap concept drefs (unlike entity drefs) +2. **Mass/count feature determines kind pronoun** — *it* for [MASS], + *they* for [COUNT], independent of ontology +3. **Kind anaphora ≠ concept anaphora** — kind anaphors derive kind + individuals via ∩ (and ⊔ for count), concept anaphors reuse the property + +## End-to-End Example + +Section 3 constructs a concrete model of examples (44)–(45): + +``` +John₁ doesn't own [DP a₃ [NP dog]₂]. + → concept dref x₂ ('dog'[COUNT]) persists in output + → entity dref x₃ (the dog) is trapped under ¬∃ +He₁ is afraid of them₂,₄. + → kind anaphor picks up concept x₂ (accessible!) + → derives kind individual via ∩(⊔⟦dog⟧) +``` +-/ + +namespace Krifka2026 + +open Semantics.Dynamic.Core (ConceptDRef DRefVal) +open Semantics.Kinds.Anaphora + +-- ════════════════════════════════════════════════════ +-- § 1. Kind Pronoun Selection +-- ════════════════════════════════════════════════════ + +/-- Kind-anaphoric pronouns, selected by the [MASS]/[COUNT] feature. -/ +inductive KindPronoun where + | it -- singular, selects [MASS] concepts + | they -- plural, selects [COUNT] concepts + deriving DecidableEq, Repr + +/-- Select kind-anaphoric pronoun from the count feature. + + [krifka-2026] (17a,b): + - ⟦it⟧ = λP[MASS] λi.∩P(i) + - ⟦they⟧ = λP[COUNT] λi.∩⊔P(i) -/ +def selectPronoun : MassCount → KindPronoun + | .mass => .it + | .count => .they + +/-- Example (7a): count noun antecedent → plural kind anaphor *them*. + *John noticed a spider in the bathroom. He has a phobia against them / \*it.* -/ +theorem ex7a_count_them : selectPronoun .count = .they := rfl + +/-- Example (7b): mass noun antecedent → singular kind anaphor *it*. + *John noticed mold in the bathroom. He is allergic against it / \*them.* -/ +theorem ex7b_mass_it : selectPronoun .mass = .it := rfl + +/-- Examples (8a,b): the same individuals (*pollen*[MASS] vs *pollen grains*[COUNT]) + select different pronouns based purely on the morphosyntactic feature. + (8a) *There is a lot of pollen in the air. I am allergic against it / \*them.* + (8b) *There are a lot of pollen grains in the air. I am allergic against them / ??it.* -/ +theorem ex8_feature_determines_pronoun : + selectPronoun .mass ≠ selectPronoun .count := by decide + + +-- ════════════════════════════════════════════════════ +-- § 2. Concept DRef Projection: Island Escaping +-- ════════════════════════════════════════════════════ + +section IslandEscaping + +variable {W E : Type*} + +/-- Examples (5a,c), (25), (44–45): Concept drefs project past negation. + + (5a) *John doesn't own a dog. He is afraid of them. But Mary owns one.* + (5c) *John doesn't own a dog. \*It is friendly.* + + In the DRT representation (25) and dynamic semantics (44–45), the concept + dref x₂ for 'dog' is in the main box / presupposed in the input. After + negation, x₂ persists (licensing *them₂*, *one₂*), but the entity dref + x₃ is trapped under ¬∃ (blocking *\*it₃*). -/ +theorem dog_concept_survives_negation + {dogConcept : ConceptDRef W E} + {φ : DSent W E} + {g h : HAssign W E} + (hDog : g 2 = .concept dogConcept) + (hNovel : g 3 = .undef) + (hNeg : dNeg φ g h) : + h 2 = .concept dogConcept ∧ h 3 = .undef := + concept_entity_asymmetry hDog hNovel hNeg + +end IslandEscaping + + +-- ════════════════════════════════════════════════════ +-- § 3. End-to-End: "John doesn't own a dog" (44–45) +-- ════════════════════════════════════════════════════ + +section EndToEnd + +/-- Concrete entity type for the worked example. -/ +inductive Ent where | john | mary + deriving DecidableEq, Repr + +/-- Concrete world type. A world where John doesn't own a dog. -/ +inductive Wld where | w₀ + deriving DecidableEq, Repr + +/-- The concept 'dog' as a concept dref with [COUNT] feature. + In this model, no entity satisfies the dog predicate (John doesn't own one). -/ +def dogConcept : ConceptDRef Wld Ent where + property := λ _ _ => false -- no dogs in this model + feature := .count + +/-- Initial assignment for (44e): g₁=F(John), g₂=F(dog), F(C)(g₂). + Following [krifka-2026] (40g)/(44e): John's name presupposes + dref 1 is anchored to John; the head noun *dog*₂ presupposes dref 2 + is anchored to the 'dog' concept with [COUNT] feature. -/ +def g₀ : HAssign Wld Ent := λ n => + match n with + | 1 => .entity .john + | 2 => .concept dogConcept + | _ => .undef + +/-- Sentence meaning for "own [DP a₃ [NP dog]₂]": introduces entity dref + at index 3, constrained to satisfy the concept property at index 2. -/ +def ownADog : DSent Wld Ent := entityIntro 3 (λ g h => + g = h ∧ (g 2).liftConceptPred (λ c => c.property .w₀ (match g 3 with + | .entity e => e | _ => .john)) = true) + +/-- "John₁ doesn't own [DP a₃ [NP dog]₂]" as the negation of ownADog. -/ +def doesntOwnADog : DSent Wld Ent := dNeg ownADog + +/-- The negation is satisfiable in this model (no dogs exist). + Output: g₀ = h (test), confirming no entity dref was introduced. -/ +theorem negation_satisfiable : + doesntOwnADog g₀ g₀ := by + refine ⟨rfl, ?_⟩ + intro ⟨k, e, hBody⟩ + simp only [g₀, dogConcept, DRefVal.liftConceptPred] at hBody + obtain ⟨hEq, hProp⟩ := hBody + -- After update, g(2) = g₀(2) = .concept dogConcept, g(3) = .entity e + -- The concept property returns false for all entities + simp at hProp + +/-- **Main result**: after "John doesn't own a dog", the concept dref + for 'dog' at index 2 is accessible while the entity dref at index 3 + remains undefined. This is the concrete instantiation of the asymmetry + predicted by [krifka-2026] §4. -/ +theorem concrete_concept_entity_asymmetry : + ∀ h : HAssign Wld Ent, + doesntOwnADog g₀ h → + h 2 = .concept dogConcept ∧ h 3 = .undef := + λ _ hNeg => concept_entity_asymmetry rfl rfl hNeg + +/-- The kind anaphor *them* selects [COUNT] for dogs, as expected. -/ +theorem dog_kind_pronoun : selectPronoun dogConcept.feature = .they := rfl + +end EndToEnd + + +-- ════════════════════════════════════════════════════ +-- § 4. Concept vs Kind Anaphora (19a,b) +-- ════════════════════════════════════════════════════ + +/-- Anaphoric constructions that pick up concept drefs. + + [krifka-2026] §3 distinguishes concept anaphors (which reuse the + property directly) from kind anaphors (which derive kind individuals + via ∩). Both pick up concept drefs, but they do different things. + + The distinction is testable via examples like (19a,b): + (19a) *John didn't get a dog from the animal shelter downtown. + He is afraid of them.* — kind anaphora (OK: dogs-as-kind) + (19b) *John didn't get a dog from the animal shelter downtown. + But Mary got one.* — concept anaphora (OK: a dog-from-the-shelter) -/ +inductive AnaphoricConstruction where + | emptyNP -- *one*, empty NP: picks up concept property directly + | emptyPP -- partitive *of them*: picks up concept for part-whole + | kindPron -- *it*[MASS], *they*[COUNT]: derives kind via ∩(⊔)P + deriving DecidableEq, Repr + +/-- Whether a construction derives a kind individual or reuses the property. -/ +def derivesKind : AnaphoricConstruction → Bool + | .kindPron => true + | .emptyNP => false + | .emptyPP => false + +/-- Kind pronouns derive kinds; concept anaphors (*one*, empty NP/PP) don't. + This distinction explains (19a) vs (19b): "dogs from the animal shelter" + doesn't name a kind (cf. [carlson-1977]), so kind anaphora yields the + general dog-kind, while concept anaphora preserves the full NP property. -/ +theorem kind_vs_concept_distinction : + derivesKind .kindPron = true ∧ + derivesKind .emptyNP = false ∧ + derivesKind .emptyPP = false := + ⟨rfl, rfl, rfl⟩ + +end Krifka2026 diff --git a/Linglib/Studies/OsborneLi2023.lean b/Linglib/Studies/OsborneLi2023.lean index 4140b39a4..2bd144dbf 100644 --- a/Linglib/Studies/OsborneLi2023.lean +++ b/Linglib/Studies/OsborneLi2023.lean @@ -1,5 +1,5 @@ import Linglib.Syntax.DependencyGrammar.Basic -import Linglib.Core.UD.Word +import Linglib.Core.UniversalDependencies import Linglib.Data.Examples.Schema import Linglib.Syntax.DependencyGrammar.Coordination diff --git a/Linglib/Studies/RomeroHan2004.lean b/Linglib/Studies/RomeroHan2004.lean index dc8b7249b..33955aab5 100644 --- a/Linglib/Studies/RomeroHan2004.lean +++ b/Linglib/Studies/RomeroHan2004.lean @@ -1,5 +1,5 @@ import Linglib.Discourse.CommonGround -import Linglib.Core.UD.Word +import Linglib.Core.UniversalDependencies /-! # Romero & Han (2004): Negative Yes/No Questions and Epistemic Bias diff --git a/Linglib/Studies/Sauerland2003.lean b/Linglib/Studies/Sauerland2003.lean index 6773db358..bddc15038 100644 --- a/Linglib/Studies/Sauerland2003.lean +++ b/Linglib/Studies/Sauerland2003.lean @@ -694,7 +694,7 @@ theorem politeness_uses_unmarked : -- Plural (number) isSemanticUnmarked (PhiFeatures.toPair Features.Number.pluralF) = true ∧ -- 3rd person - isSemanticUnmarked (PhiFeatures.toPair Features.Person.third) = true ∧ + isSemanticUnmarked (PhiFeatures.toPair Features.Person.thirdF) = true ∧ -- Masculine (gender) isSemanticUnmarked (PhiFeatures.toPair Features.Gender.masculineF) = true := ⟨rfl, rfl, rfl⟩ @@ -704,7 +704,7 @@ theorem politeness_uses_unmarked : restrictions on the addressee. -/ theorem marked_not_polite : isSemanticMarked (PhiFeatures.toPair Features.Number.singularF) = true ∧ - isSemanticMarked (PhiFeatures.toPair Features.Person.first) = true ∧ + isSemanticMarked (PhiFeatures.toPair Features.Person.firstF) = true ∧ isSemanticMarked (PhiFeatures.toPair Features.Gender.neuterF) = true := ⟨rfl, rfl, rfl⟩ diff --git a/Linglib/Studies/Smith1997.lean b/Linglib/Studies/Smith1997.lean index e38a5bda4..d5b532128 100644 --- a/Linglib/Studies/Smith1997.lean +++ b/Linglib/Studies/Smith1997.lean @@ -5,6 +5,7 @@ import Linglib.Phenomena.TenseAspect.Diagnostics import Linglib.Fragments.English.TenseAspect import Linglib.Fragments.French.TenseAspect import Linglib.Fragments.Mandarin.TenseAspect +import Linglib.Features.MassCount /-! # The Parameter of Aspect (2nd ed.) diff --git a/Linglib/Studies/TurkHirsch2026.lean b/Linglib/Studies/TurkHirsch2026.lean index 282ffad92..ad918c0f7 100644 --- a/Linglib/Studies/TurkHirsch2026.lean +++ b/Linglib/Studies/TurkHirsch2026.lean @@ -1,6 +1,6 @@ import Linglib.Features.InformationStructure import Linglib.Core.Logic.Intensional.Premise -import Linglib.Core.UD.Basic +import Linglib.Core.UniversalDependencies import Linglib.Semantics.Alternatives.AltMeaning import Linglib.Semantics.Polarity.Operator import Linglib.Semantics.Focus.Interpretation diff --git a/Linglib/Studies/Wang2023.lean b/Linglib/Studies/Wang2023.lean index 7e87241f2..b84dd73b6 100644 --- a/Linglib/Studies/Wang2023.lean +++ b/Linglib/Studies/Wang2023.lean @@ -437,7 +437,7 @@ theorem plural_strategy_is_plSem : /-- The 3rd-person strategy targets the minimal PERSON cell, which is `thirdSem` — the PrProp with vacuous presupposition. -/ theorem thirdPerson_strategy_is_third : - honStrategyCell .thirdPerson = PhiFeatures.toPair Features.Person.third := + honStrategyCell .thirdPerson = PhiFeatures.toPair Features.Person.thirdF := rfl /-- Both strategies target cells whose presuppositional denotations diff --git a/Linglib/Studies/Zheng2025.lean b/Linglib/Studies/Zheng2025.lean index ad4a317d8..ad27015e2 100644 --- a/Linglib/Studies/Zheng2025.lean +++ b/Linglib/Studies/Zheng2025.lean @@ -1,4 +1,4 @@ -import Linglib.Core.UD.Word +import Linglib.Core.UniversalDependencies import Linglib.Fragments.Mandarin.QuestionParticles import Linglib.Semantics.Modality.Kernel import Linglib.Features.QParticleLayer diff --git a/Linglib/Syntax/Agreement/Paradigm.lean b/Linglib/Syntax/Agreement/Paradigm.lean index 6c6c5e0e9..fdd2e3b6c 100644 --- a/Linglib/Syntax/Agreement/Paradigm.lean +++ b/Linglib/Syntax/Agreement/Paradigm.lean @@ -1,4 +1,4 @@ -import Linglib.Core.UD.Word +import Linglib.Core.UniversalDependencies import Linglib.Features.Prominence /-! diff --git a/Linglib/Syntax/Binding/Basic.lean b/Linglib/Syntax/Binding/Basic.lean index c90cd0af8..0a250d475 100644 --- a/Linglib/Syntax/Binding/Basic.lean +++ b/Linglib/Syntax/Binding/Basic.lean @@ -1,4 +1,4 @@ -import Linglib.Core.UD.Word +import Linglib.Core.UniversalDependencies import Linglib.Features.CoreferenceStatus /-! diff --git a/Linglib/Syntax/ConstructionGrammar/ArgumentStructure.lean b/Linglib/Syntax/ConstructionGrammar/ArgumentStructure.lean index 1947ce8e0..61b872c40 100644 --- a/Linglib/Syntax/ConstructionGrammar/ArgumentStructure.lean +++ b/Linglib/Syntax/ConstructionGrammar/ArgumentStructure.lean @@ -3,7 +3,7 @@ import Linglib.Syntax.ConstructionGrammar.Studies.GoldbergShirtz2025 import Linglib.Syntax.ConstructionGrammar.Studies.FillmoreKayOConnor1988 import Linglib.Core.CombinationKind import Linglib.Semantics.ArgumentStructure.DiathesisAlternation -import Linglib.Core.UD.Basic +import Linglib.Core.UniversalDependencies /-! # Argument Structure Constructions diff --git a/Linglib/Syntax/DependencyGrammar/Basic.lean b/Linglib/Syntax/DependencyGrammar/Basic.lean index 56330df99..41a8ddb6f 100644 --- a/Linglib/Syntax/DependencyGrammar/Basic.lean +++ b/Linglib/Syntax/DependencyGrammar/Basic.lean @@ -1,5 +1,5 @@ import Mathlib.Data.List.Basic -import Linglib.Core.UD.Word +import Linglib.Core.UniversalDependencies import Linglib.Core.Valence /-! diff --git a/Linglib/Syntax/DependencyGrammar/Nominal.lean b/Linglib/Syntax/DependencyGrammar/Nominal.lean index b60cc9525..bf93a854d 100644 --- a/Linglib/Syntax/DependencyGrammar/Nominal.lean +++ b/Linglib/Syntax/DependencyGrammar/Nominal.lean @@ -1,4 +1,4 @@ -import Linglib.Core.UD.Word +import Linglib.Core.UniversalDependencies import Linglib.Features.CoreferenceStatus import Linglib.Fragments.English.Nouns import Linglib.Fragments.English.Pronouns diff --git a/Linglib/Syntax/HPSG/Basic.lean b/Linglib/Syntax/HPSG/Basic.lean index 882c10584..9d7a149e6 100644 --- a/Linglib/Syntax/HPSG/Basic.lean +++ b/Linglib/Syntax/HPSG/Basic.lean @@ -3,7 +3,7 @@ HPSG formalization: typed feature structures, signs, and phrase structure schema [pollard-sag-1994], [sag-wasow-bender-2003], [ginzburg-sag-2000]. -/ -import Linglib.Core.UD.Word +import Linglib.Core.UniversalDependencies namespace HPSG diff --git a/Linglib/Syntax/Minimalist/Basic.lean b/Linglib/Syntax/Minimalist/Basic.lean index 0d069b16b..9a3e59560 100644 --- a/Linglib/Syntax/Minimalist/Basic.lean +++ b/Linglib/Syntax/Minimalist/Basic.lean @@ -1,7 +1,7 @@ import Mathlib.Data.Set.Basic import Mathlib.Data.Multiset.Basic import Mathlib.Algebra.Free -import Linglib.Core.UD.Basic +import Linglib.Core.UniversalDependencies import Linglib.Core.Combinatorics.RootedTree.Decorated /-! diff --git a/Linglib/Syntax/Minimalist/Features.lean b/Linglib/Syntax/Minimalist/Features.lean index 4d1d8b466..2b9f1f41f 100644 --- a/Linglib/Syntax/Minimalist/Features.lean +++ b/Linglib/Syntax/Minimalist/Features.lean @@ -1,6 +1,7 @@ import Linglib.Features.Case -import Linglib.Core.UD.Word +import Linglib.Core.UniversalDependencies import Linglib.Features.Prominence +import Linglib.Features.Number /-! # Feature Infrastructure for Minimalist Agree @@ -46,6 +47,8 @@ for probes. -/ +open Features (Number) + namespace Minimalist open Features.Prominence diff --git a/Linglib/Syntax/Minimalist/Modification.lean b/Linglib/Syntax/Minimalist/Modification.lean index fbf477a01..6dabf925b 100644 --- a/Linglib/Syntax/Minimalist/Modification.lean +++ b/Linglib/Syntax/Minimalist/Modification.lean @@ -1,199 +1,200 @@ -import Linglib.Syntax.Minimalist.Features -import Linglib.Morphology.MorphRule - -/-! -# Syntactic Modification via Feature Composition -[alexeyenko-zeijlstra-2025] - -Nominal modification as a species of complementation: adjectives and nouns -cannot directly merge because neither c-selects the other. Resolution comes -either from the adjective lexically carrying `[N, uN]` (in φ/κ-complete -languages like Greek) or from an **Attr head** that mediates the feature -conversion. - -## Core Claims - -1. **Modification = complementation**: both are driven by c-selection features - (`[uF]` checked under sisterhood with `[F]`). An adjective `[A]` and a - noun `[N]` can merge only if one bears the other's uninterpretable - categorial feature. - -2. **Two feature compositions** (§5.1): - - **Direct**: adjective enters as `[N, uN]`, selects and merges with `[N]` - directly. Available only when pred & attr adjectives have identical - φ/κ-specification. Corresponds semantically to predicate modification. - - **Attr-mediated**: an Attr head converts `[A] → [N, uN]` (part of xAP) - or `[N] → [N, uA]` (part of xNP). Required when adjectives lack full - φ/κ-specification. - -3. **Attr status determines linearization** (§5.2): the morphophonological - realization of Attr (affix / clitic / free word / null) determines - whether it must be linearly adjacent to its host, via the Input - Correspondence Principle ([ackema-neeleman-2004]). - -## Types Exported - -- `AttrStatus` — morphophonological status of the attributivizer -- `AdjMorphProfile` — per-language adjective morphosyntactic profile -- `ModificationRoute` — direct (no Attr) vs Attr-mediated modification -- `morphStatusToAttrStatus` — bridge from `Core.Lexical.MorphRule.MorphStatus` --/ - -namespace Minimalist.Modification - -open Morphology (MorphStatus) - --- ============================================================================ --- § 1: Attributivizer Status --- ============================================================================ - -/-- Morphophonological status of the attributivizer (Attr head, §5.2). - Determines whether Attr imposes linear adjacency with the adjective. -/ -inductive AttrStatus where - | affix -- must be adjacent to host per ICP: German -er, Dutch -e, Basque - | clitic -- morphophonologically independent: Mandarin 的, Farsi ezafe - | freeWord -- independent word form - | null -- covert but syntactically present: English, Hungarian - deriving DecidableEq, Repr - -/-- Position of attributive adjectives relative to the modified noun. -/ -inductive AdjPosition where - | prenominal -- A–N: English, German, Russian, Greek - | postnominal -- N–A: Basque, Farsi, Eastern Oromo - | both -- both orders productive: Latin, Tagalog - deriving DecidableEq, Repr - --- ============================================================================ --- § 2: Adjective Morphosyntactic Profile --- ============================================================================ - -/-- Morphosyntactic profile of adjectives in a language. - - The MAG (34) is determined by two independent factors: - - **Morphosyntactic** (§5.1): agreement identity between predicative and - attributive forms, and completeness of that agreement for all φ/κ-features - - **Morphophonological** (§5.2): status of the attributivizer -/ -structure AdjMorphProfile where - /-- Primary position of attributive adjectives relative to N -/ - adjPosition : AdjPosition - /-- Internal head direction of the AP -/ - apDirection : HeadDirection - /-- MAG (34a), clause 1: the agreement marker on attr adjectives is - also present on predicative adjectives (pred = attr featurally). -/ - predAttrSameAgreement : Bool - /-- MAG (34a), clause 2: the agreement marker is specified for ALL - φ/κ-features available in the DP. Per fn 17, κ (case) is always - a DP feature whether morphologically realized or not. -/ - agreementPhiKappaComplete : Bool - /-- MAG (34b): morphophonological status of the attributivizer -/ - attrStatus : AttrStatus - deriving DecidableEq, Repr - --- ============================================================================ --- § 3: Modification Routes (§5.1) --- ============================================================================ - -/-- The two routes to nominal modification (§5.1.2 vs §5.1.3). - - - **direct**: adjective lexically carries `[N, uN]`, merges directly - with the noun. No Attr head needed. Only available in φ/κ-complete - languages (Greek, Russian, Latin, Kalaallisut). - - **attrMediated**: an Attr functional head mediates the feature - conversion. Required when adjectives lack full φ/κ-specification. - Attr may be part of the extended adjectival projection (xAP) or - the extended nominal projection (xNP). -/ -inductive ModificationRoute where - | direct -- [N, uN] + [N] → no Attr needed (§5.1.2) - | attrMediated -- Attr converts [A] → [N, uN] or [N] → [N, uA] (§5.1.3) - deriving DecidableEq, Repr - -/-- Determine the modification route from the adjective morphosyntactic - profile. φ/κ-complete languages use direct modification; all others - require an Attr head. -/ -def modificationRoute (prof : AdjMorphProfile) : ModificationRoute := - if prof.predAttrSameAgreement && prof.agreementPhiKappaComplete then - .direct - else - .attrMediated - -/-- φ/κ-complete languages use direct modification. -/ -theorem phiKappaComplete_implies_direct (prof : AdjMorphProfile) - (hSame : prof.predAttrSameAgreement = true) - (hComplete : prof.agreementPhiKappaComplete = true) : - modificationRoute prof = .direct := by - simp [modificationRoute, hSame, hComplete] - -/-- Languages with pred ≠ attr require Attr. -/ -theorem predNeAttr_implies_attrMediated (prof : AdjMorphProfile) - (h : prof.predAttrSameAgreement = false) : - modificationRoute prof = .attrMediated := by - simp [modificationRoute, h] - -/-- Languages with incomplete φ/κ require Attr. -/ -theorem incomplete_implies_attrMediated (prof : AdjMorphProfile) - (h : prof.agreementPhiKappaComplete = false) : - modificationRoute prof = .attrMediated := by - simp [modificationRoute, h] - --- ============================================================================ --- § 4: Bridge from MorphStatus to AttrStatus --- ============================================================================ - -/-- Map the framework-agnostic `MorphStatus` (from Zwicky & Pullum's - clitic-affix cline) to the MAG's `AttrStatus`. Both inflectional - and derivational affixes impose adjacency per the ICP. Both simple - and special clitics are morphophonologically independent. -/ -def morphStatusToAttrStatus : MorphStatus → AttrStatus - | .freeWord => .freeWord - | .simpleClitic => .clitic - | .specialClitic => .clitic - | .inflAffix => .affix - | .derivAffix => .affix - -/-- Affixes impose adjacency. -/ -theorem affix_maps_to_affix : - morphStatusToAttrStatus .inflAffix = .affix := rfl - -/-- Clitics are morphophonologically independent. -/ -theorem clitic_maps_to_clitic : - morphStatusToAttrStatus .simpleClitic = .clitic := rfl - -/-- Free words map to free words. -/ -theorem freeWord_maps_to_freeWord : - morphStatusToAttrStatus .freeWord = .freeWord := rfl - --- ============================================================================ --- § 5: MAG Feature Types (bridge to Minimalist features) --- ============================================================================ - -/-- The feature types that MAG condition (a) requires agreement for. - φ-features map to `Minimalist.PhiFeature`, κ-features to `Features.Case`. -/ -inductive MAGFeatureType where - | phi : Minimalist.PhiFeature → MAGFeatureType - | kappa : Features.Case → MAGFeatureType - deriving DecidableEq, Repr - -/-- An adjective agreement entry: which features are morphologically - realized on adjectives in each syntactic position. -/ -structure AdjAgreementEntry where - /-- Features realized on predicative adjectives. -/ - predFeatures : List MAGFeatureType - /-- Features realized on attributive adjectives. -/ - attrFeatures : List MAGFeatureType - /-- All φ/κ-features available in the DP of this language. -/ - dpFeatures : List MAGFeatureType - deriving Repr - -/-- Derive `predAttrSameAgreement` from an agreement entry: - true iff the attr feature list is a subset of the pred features and - vice versa (same set). Simplified to list equality for decidability. -/ -def AdjAgreementEntry.sameAgreement (e : AdjAgreementEntry) : Bool := - e.predFeatures.length == e.attrFeatures.length && - e.attrFeatures.all (e.predFeatures.contains ·) - -/-- Derive `agreementPhiKappaComplete` from an agreement entry: - true iff every DP feature appears on the attributive adjective. -/ -def AdjAgreementEntry.phiKappaComplete (e : AdjAgreementEntry) : Bool := - e.dpFeatures.all (e.attrFeatures.contains ·) - -end Minimalist.Modification +import Linglib.Syntax.Minimalist.Features +import Linglib.Morphology.MorphRule +import Linglib.Typology.WordOrder + +/-! +# Syntactic Modification via Feature Composition +[alexeyenko-zeijlstra-2025] + +Nominal modification as a species of complementation: adjectives and nouns +cannot directly merge because neither c-selects the other. Resolution comes +either from the adjective lexically carrying `[N, uN]` (in φ/κ-complete +languages like Greek) or from an **Attr head** that mediates the feature +conversion. + +## Core Claims + +1. **Modification = complementation**: both are driven by c-selection features + (`[uF]` checked under sisterhood with `[F]`). An adjective `[A]` and a + noun `[N]` can merge only if one bears the other's uninterpretable + categorial feature. + +2. **Two feature compositions** (§5.1): + - **Direct**: adjective enters as `[N, uN]`, selects and merges with `[N]` + directly. Available only when pred & attr adjectives have identical + φ/κ-specification. Corresponds semantically to predicate modification. + - **Attr-mediated**: an Attr head converts `[A] → [N, uN]` (part of xAP) + or `[N] → [N, uA]` (part of xNP). Required when adjectives lack full + φ/κ-specification. + +3. **Attr status determines linearization** (§5.2): the morphophonological + realization of Attr (affix / clitic / free word / null) determines + whether it must be linearly adjacent to its host, via the Input + Correspondence Principle ([ackema-neeleman-2004]). + +## Types Exported + +- `AttrStatus` — morphophonological status of the attributivizer +- `AdjMorphProfile` — per-language adjective morphosyntactic profile +- `ModificationRoute` — direct (no Attr) vs Attr-mediated modification +- `morphStatusToAttrStatus` — bridge from `Core.Lexical.MorphRule.MorphStatus` +-/ + +namespace Minimalist.Modification + +open Morphology (MorphStatus) + +-- ============================================================================ +-- § 1: Attributivizer Status +-- ============================================================================ + +/-- Morphophonological status of the attributivizer (Attr head, §5.2). + Determines whether Attr imposes linear adjacency with the adjective. -/ +inductive AttrStatus where + | affix -- must be adjacent to host per ICP: German -er, Dutch -e, Basque + | clitic -- morphophonologically independent: Mandarin 的, Farsi ezafe + | freeWord -- independent word form + | null -- covert but syntactically present: English, Hungarian + deriving DecidableEq, Repr + +/-- Position of attributive adjectives relative to the modified noun. -/ +inductive AdjPosition where + | prenominal -- A–N: English, German, Russian, Greek + | postnominal -- N–A: Basque, Farsi, Eastern Oromo + | both -- both orders productive: Latin, Tagalog + deriving DecidableEq, Repr + +-- ============================================================================ +-- § 2: Adjective Morphosyntactic Profile +-- ============================================================================ + +/-- Morphosyntactic profile of adjectives in a language. + + The MAG (34) is determined by two independent factors: + - **Morphosyntactic** (§5.1): agreement identity between predicative and + attributive forms, and completeness of that agreement for all φ/κ-features + - **Morphophonological** (§5.2): status of the attributivizer -/ +structure AdjMorphProfile where + /-- Primary position of attributive adjectives relative to N -/ + adjPosition : AdjPosition + /-- Internal head direction of the AP -/ + apDirection : HeadDirection + /-- MAG (34a), clause 1: the agreement marker on attr adjectives is + also present on predicative adjectives (pred = attr featurally). -/ + predAttrSameAgreement : Bool + /-- MAG (34a), clause 2: the agreement marker is specified for ALL + φ/κ-features available in the DP. Per fn 17, κ (case) is always + a DP feature whether morphologically realized or not. -/ + agreementPhiKappaComplete : Bool + /-- MAG (34b): morphophonological status of the attributivizer -/ + attrStatus : AttrStatus + deriving DecidableEq, Repr + +-- ============================================================================ +-- § 3: Modification Routes (§5.1) +-- ============================================================================ + +/-- The two routes to nominal modification (§5.1.2 vs §5.1.3). + + - **direct**: adjective lexically carries `[N, uN]`, merges directly + with the noun. No Attr head needed. Only available in φ/κ-complete + languages (Greek, Russian, Latin, Kalaallisut). + - **attrMediated**: an Attr functional head mediates the feature + conversion. Required when adjectives lack full φ/κ-specification. + Attr may be part of the extended adjectival projection (xAP) or + the extended nominal projection (xNP). -/ +inductive ModificationRoute where + | direct -- [N, uN] + [N] → no Attr needed (§5.1.2) + | attrMediated -- Attr converts [A] → [N, uN] or [N] → [N, uA] (§5.1.3) + deriving DecidableEq, Repr + +/-- Determine the modification route from the adjective morphosyntactic + profile. φ/κ-complete languages use direct modification; all others + require an Attr head. -/ +def modificationRoute (prof : AdjMorphProfile) : ModificationRoute := + if prof.predAttrSameAgreement && prof.agreementPhiKappaComplete then + .direct + else + .attrMediated + +/-- φ/κ-complete languages use direct modification. -/ +theorem phiKappaComplete_implies_direct (prof : AdjMorphProfile) + (hSame : prof.predAttrSameAgreement = true) + (hComplete : prof.agreementPhiKappaComplete = true) : + modificationRoute prof = .direct := by + simp [modificationRoute, hSame, hComplete] + +/-- Languages with pred ≠ attr require Attr. -/ +theorem predNeAttr_implies_attrMediated (prof : AdjMorphProfile) + (h : prof.predAttrSameAgreement = false) : + modificationRoute prof = .attrMediated := by + simp [modificationRoute, h] + +/-- Languages with incomplete φ/κ require Attr. -/ +theorem incomplete_implies_attrMediated (prof : AdjMorphProfile) + (h : prof.agreementPhiKappaComplete = false) : + modificationRoute prof = .attrMediated := by + simp [modificationRoute, h] + +-- ============================================================================ +-- § 4: Bridge from MorphStatus to AttrStatus +-- ============================================================================ + +/-- Map the framework-agnostic `MorphStatus` (from Zwicky & Pullum's + clitic-affix cline) to the MAG's `AttrStatus`. Both inflectional + and derivational affixes impose adjacency per the ICP. Both simple + and special clitics are morphophonologically independent. -/ +def morphStatusToAttrStatus : MorphStatus → AttrStatus + | .freeWord => .freeWord + | .simpleClitic => .clitic + | .specialClitic => .clitic + | .inflAffix => .affix + | .derivAffix => .affix + +/-- Affixes impose adjacency. -/ +theorem affix_maps_to_affix : + morphStatusToAttrStatus .inflAffix = .affix := rfl + +/-- Clitics are morphophonologically independent. -/ +theorem clitic_maps_to_clitic : + morphStatusToAttrStatus .simpleClitic = .clitic := rfl + +/-- Free words map to free words. -/ +theorem freeWord_maps_to_freeWord : + morphStatusToAttrStatus .freeWord = .freeWord := rfl + +-- ============================================================================ +-- § 5: MAG Feature Types (bridge to Minimalist features) +-- ============================================================================ + +/-- The feature types that MAG condition (a) requires agreement for. + φ-features map to `Minimalist.PhiFeature`, κ-features to `Features.Case`. -/ +inductive MAGFeatureType where + | phi : Minimalist.PhiFeature → MAGFeatureType + | kappa : Features.Case → MAGFeatureType + deriving DecidableEq, Repr + +/-- An adjective agreement entry: which features are morphologically + realized on adjectives in each syntactic position. -/ +structure AdjAgreementEntry where + /-- Features realized on predicative adjectives. -/ + predFeatures : List MAGFeatureType + /-- Features realized on attributive adjectives. -/ + attrFeatures : List MAGFeatureType + /-- All φ/κ-features available in the DP of this language. -/ + dpFeatures : List MAGFeatureType + deriving Repr + +/-- Derive `predAttrSameAgreement` from an agreement entry: + true iff the attr feature list is a subset of the pred features and + vice versa (same set). Simplified to list equality for decidability. -/ +def AdjAgreementEntry.sameAgreement (e : AdjAgreementEntry) : Bool := + e.predFeatures.length == e.attrFeatures.length && + e.attrFeatures.all (e.predFeatures.contains ·) + +/-- Derive `agreementPhiKappaComplete` from an agreement entry: + true iff every DP feature appears on the attributive adjective. -/ +def AdjAgreementEntry.phiKappaComplete (e : AdjAgreementEntry) : Bool := + e.dpFeatures.all (e.attrFeatures.contains ·) + +end Minimalist.Modification diff --git a/Linglib/Syntax/Pronoun/Basic.lean b/Linglib/Syntax/Pronoun/Basic.lean index 5fae89b63..65e28a32a 100644 --- a/Linglib/Syntax/Pronoun/Basic.lean +++ b/Linglib/Syntax/Pronoun/Basic.lean @@ -1,10 +1,12 @@ -import Linglib.Core.UD.Word +import Linglib.Core.UniversalDependencies import Linglib.Features.Case import Linglib.Features.Register import Linglib.Features.Prominence import Linglib.Features.Gender import Linglib.Features.Clusivity import Linglib.Features.CoreferenceStatus +import Linglib.Features.Number +import Linglib.Features.Person /-! # Pronoun @@ -33,6 +35,8 @@ in as fields of the general `Pronoun`. * `Pronoun.AllocutiveEntry` — speaker–addressee (allocutive) markers. -/ +open Features (Number Person) + set_option autoImplicit false /-- The general pronoun object: the morphosyntactic core shared by every pronoun diff --git a/Linglib/Syntax/Pronoun/Capabilities.lean b/Linglib/Syntax/Pronoun/Capabilities.lean index c5a51c168..7b252f35c 100644 --- a/Linglib/Syntax/Pronoun/Capabilities.lean +++ b/Linglib/Syntax/Pronoun/Capabilities.lean @@ -1,4 +1,4 @@ -import Linglib.Core.UD.Word +import Linglib.Core.UniversalDependencies import Linglib.Features.CoreferenceStatus import Linglib.Features.Register import Linglib.Features.Prominence diff --git a/Linglib/Typology/Adposition.lean b/Linglib/Typology/Adposition.lean index 86e5515ed..6b14d7679 100644 --- a/Linglib/Typology/Adposition.lean +++ b/Linglib/Typology/Adposition.lean @@ -1,5 +1,6 @@ import Linglib.Data.WALS.Features.F85A -import Linglib.Core.UD.Word +import Linglib.Core.UniversalDependencies +import Linglib.Typology.WordOrder /-! # Adposition typology: shared substrate type diff --git a/Linglib/Typology/AuxiliaryVerbs.lean b/Linglib/Typology/AuxiliaryVerbs.lean index fac3d9995..392c58ad1 100644 --- a/Linglib/Typology/AuxiliaryVerbs.lean +++ b/Linglib/Typology/AuxiliaryVerbs.lean @@ -1,4 +1,4 @@ -import Linglib.Core.UD.Basic +import Linglib.Core.UniversalDependencies import Linglib.Morphology.MorphRule /-! diff --git a/Linglib/Typology/ClauseChaining.lean b/Linglib/Typology/ClauseChaining.lean index d7c681f27..5652990ca 100644 --- a/Linglib/Typology/ClauseChaining.lean +++ b/Linglib/Typology/ClauseChaining.lean @@ -1,5 +1,5 @@ -import Linglib.Core.UD.Basic -import Linglib.Core.UD.Word +import Linglib.Core.UniversalDependencies +import Linglib.Typology.WordOrder /-! # Clause Chaining Typology [sarvasy-aikhenvald-2025] [foley-r-d-van-valin-1984] [longacre-2007] diff --git a/Linglib/Typology/WordOrder.lean b/Linglib/Typology/WordOrder.lean index 90ffce53e..1ff5c1e15 100644 --- a/Linglib/Typology/WordOrder.lean +++ b/Linglib/Typology/WordOrder.lean @@ -53,6 +53,14 @@ in their consuming Studies file (`Studies/ Gibson2025.lean`) until a second framework consumer materialises. -/ +/-- Head direction of a syntactic construction: head-initial (VO, prepositions, +head-initial FocP, …) vs head-final. Used for word-order typology and constraints +like FOFC. Root-named (consumed across Fragments, Studies, Syntax). -/ +inductive HeadDirection where + | headInitial + | headFinal + deriving Repr, DecidableEq + namespace Typology.WordOrder -- ============================================================================ From 74cea80e54831148e95d87e03942152432fdd3c9 Mon Sep 17 00:00:00 2001 From: Robert Hawkins Date: Thu, 4 Jun 2026 08:25:27 -0700 Subject: [PATCH 2/3] fix(Fragments): capitalize remaining UD Number values after alias drop --- Linglib/Fragments/Dargwa/Agreement.lean | 507 ++++++++-------- Linglib/Fragments/French/Nouns.lean | 19 +- Linglib/Fragments/German/AdjAgreement.lean | 2 +- .../Greek/StandardModern/AdjAgreement.lean | 2 +- Linglib/Fragments/Italian/AdjAgreement.lean | 2 +- Linglib/Fragments/Italian/Nouns.lean | 12 +- .../Fragments/Jarawara/PossessedNouns.lean | 539 +++++++++--------- .../Slavic/Russian/AdjAgreement.lean | 2 +- Linglib/Syntax/Minimalist/Agree.lean | 8 +- 9 files changed, 551 insertions(+), 542 deletions(-) diff --git a/Linglib/Fragments/Dargwa/Agreement.lean b/Linglib/Fragments/Dargwa/Agreement.lean index b87c3ca6e..0cecba51f 100644 --- a/Linglib/Fragments/Dargwa/Agreement.lean +++ b/Linglib/Fragments/Dargwa/Agreement.lean @@ -1,252 +1,255 @@ -import Linglib.Features.Prominence -import Linglib.Core.UniversalDependencies -import Linglib.Features.Gender - -/-! -# Dargwa (Tanti) Agreement [sumbatova-2021] - -Dargwa is among the few Nakh-Dagestanian languages with both **gender -agreement** and **person agreement** ([sumbatova-2021] §4.5.8, §4.7.6). - -## Gender Agreement - -Three genders in the singular (masculine, feminine, neuter) and three -in the plural (1st/2nd person, human, non-human). Gender is almost -entirely semantic: masculine = male humans, feminine = female humans, -neuter = everything else. Gender agreement targets include verb roots, -preverbs, copulas, and some adjective roots. - -Gender agreement is controlled by the **absolutive argument** in clauses. -In copular clauses with two absolutives, the predicate controls agreement. - -## Person Agreement ("Dargic Type") - -Person agreement follows the hierarchy **1, 2 > 3** and -**absolutive > ergative**. The agreement paradigm configuration is the -"Dargic type" ([cysouw-2003]): a typologically rare opposition of -2SG versus {1SG, 1PL, 2PL}, where the 3rd person is usually unmarked. - -Three person-marker sets distribute across TAM paradigms: -1. **Clitic set**: present, preterite, perfect, propositive -2. **Irrealis set**: past habitual, future, conditional -3. **Optative set**: optative - -The 2SG marker is identical across the clitic set (*=de*) and past -tense (*=de*), creating a homophony that is typologically unusual. --/ - -namespace Dargwa.Agreement - -open Features.Prominence (PersonLevel) - --- ============================================================================ --- § 1: Gender System --- ============================================================================ - -/-- Singular gender values. -/ -inductive SgGender where - | masculine -- w- (or ∅, realized as -j after vowels) - | feminine -- r- - | neuter -- b- (non-human, inanimate) - deriving DecidableEq, Repr - -/-- Plural gender values. These differ from singular genders. -/ -inductive PlGender where - | sapHuman -- d-: 1st/2nd person NPs - | human -- b-: 3rd person human plurals - | nonHuman -- d-: non-human plurals - deriving DecidableEq, Repr - -/-- Bridge to cross-linguistic surface gender. -/ -def SgGender.toSurfaceGender : SgGender → Features.SurfaceGender - | .masculine => .masculine - | .feminine => .feminine - | .neuter => .neuter - -/-- Gender agreement prefix on the verb stem. - The prefix immediately precedes the root in simplex verbs and - attaches to the light verb, preverb, or lexical stem in complex verbs - ([sumbatova-2021] §4.5.2.3, Table 4.12). -/ -def sgGenderPrefix : SgGender → String - | .masculine => "w-" - | .feminine => "r-" - | .neuter => "b-" - -def plGenderPrefix : PlGender → String - | .sapHuman => "d-" - | .human => "b-" - | .nonHuman => "d-" - -/-- Gender assignment is semantically transparent: masculine = male - humans, feminine = female humans, neuter = everything else - ([sumbatova-2021] §4.4.1). A small set of nouns have a - *variable* gender morpheme determined by the referent's actual - gender (if human) or the possessor's gender: e.g., *w-eˁ.ʔ* - 'proprietor (M)' / *r-eˁ.ʔ* 'proprietor (F)'. -/ -theorem gender_semantically_transparent : True := trivial - --- ============================================================================ --- § 2: Person Agreement --- ============================================================================ - -/-- The three person-marker paradigm sets. -/ -inductive MarkerSet where - | clitic -- present, preterite, perfect, propositive - | irrealis -- past habitual, future, conditional - | optative -- optative - deriving DecidableEq, Repr - -/-- Person clitic/suffix forms (Table 4.20, 4.21 of [sumbatova-2021]). - Returns `none` when the person is unmarked. - - **Clitic set** ("Dargic type"): =da covers 1SG, 1PL, and 2PL - (ex. 34a: "I, we, you(PL) am, are doing"); =de is 2SG only. - Table 4.21 confirms: "person clitics: 2SG =de, 1SG/PL, 2PL =da". -/ -def personMarker : MarkerSet → PersonLevel → Number → Option String - -- Clitic set: =da for {1SG, 1PL, 2PL}, =de for {2SG}, none for {3} - | .clitic, .first, _ => some "=da" - | .clitic, .second, .sg => some "=de" - | .clitic, .second, _ => some "=da" -- 2PL patterns with 1st person - | .clitic, .third, _ => none -- 3rd unmarked - -- Irrealis set - | .irrealis, .first, .sg => some "-d" - | .irrealis, .first, _ => some "-haˁ" -- (> -he) - | .irrealis, .second, .sg => some "-t:" -- (> -t) - | .irrealis, .second, _ => some "-t:-a" - | .irrealis, .third, _ => none - -- Optative set - | .optative, .first, _ => some "-a" - | .optative, .second, .sg => some "-e" - | .optative, .second, _ => some "-a" -- + -ja allocutive - | .optative, .third, _ => none - -/-- 3rd person is unmarked in all paradigm sets. -/ -theorem third_unmarked : - personMarker .clitic .third .sg = none ∧ - personMarker .clitic .third .pl = none ∧ - personMarker .irrealis .third .sg = none ∧ - personMarker .irrealis .third .pl = none ∧ - personMarker .optative .third .sg = none ∧ - personMarker .optative .third .pl = none := ⟨rfl, rfl, rfl, rfl, rfl, rfl⟩ - --- ============================================================================ --- § 3: Agreement Control --- ============================================================================ - -/-- Gender agreement controller: the absolutive argument. - In intransitive clauses: S (always absolutive). - In transitive clauses: P (absolutive), not A (ergative). - In copular clauses with two absolutives: the predicate. -/ -inductive GenderController where - | absolutive -- default: the absolutive NP - | predicate -- copular clause: predicate NP - | ergOrDat -- Tanti allows ergative/dative control optionally - deriving DecidableEq, Repr - -/-- Person agreement hierarchy: person (1, 2 > 3) and case - (absolutive > ergative). - - If one core argument is a SAP and the other is not, the verb - agrees with the SAP regardless of case. If both are SAPs, - agreement is with the absolutive. -/ -def personAgreementController (aPerson pPerson : PersonLevel) : PersonLevel := - match aPerson, pPerson with - | .first, .third => .first -- SAP wins - | .second, .third => .second -- SAP wins - | .third, .first => .first -- SAP wins - | .third, .second => .second -- SAP wins - | _, p => p -- both SAP → absolutive (P) wins - --- ============================================================================ --- § 4: Thematic Suffixes (Table 4.10 of [sumbatova-2021]) --- ============================================================================ - -/-- Thematic suffix for transitive verbs, determined by the person features - of A and P arguments (Table 4.10, §4.5.2.5 of [sumbatova-2021]). - - *-i* when A is SAP (1st/2nd) and P is 3rd — the configuration where - A outranks P in the person hierarchy (1, 2 > 3). - *-u* otherwise (both SAP, or A is 3rd). -/ -def thematicSuffix (aPerson pPerson : PersonLevel) : String := - if aPerson.isSAP && !pPerson.isSAP then "-i" else "-u" - -/-- Intransitive thematic suffix: *-u* for SAP subjects, - *-ar* / *-an* for 3rd person subjects. -/ -def intransitiveThematicSuffix (sPerson : PersonLevel) : String := - if sPerson.isSAP then "-u" else "-ar" - -/-- The thematic suffix *-i* marks the same configuration that the - person agreement hierarchy resolves to the A-argument: SAP acting - on 3rd person. The suffix is a morphological reflex of hierarchy. -/ -theorem thematic_i_iff_sap_on_third : - thematicSuffix .first .third = "-i" ∧ - thematicSuffix .second .third = "-i" ∧ - thematicSuffix .third .third = "-u" ∧ - thematicSuffix .first .second = "-u" ∧ - thematicSuffix .third .first = "-u" := ⟨rfl, rfl, rfl, rfl, rfl⟩ - -/-- When thematic suffix is *-i* (A = SAP, P = 3), person agreement - controller selects A — the same argument that triggers *-i*. - When thematic suffix is *-u* (A = 3, P = SAP), person agreement - controller selects P. The suffix and the agreement controller - always pick the highest-ranked argument. -/ -theorem thematic_suffix_tracks_controller : - -- -i cases: controller picks A (= SAP), suffix marks SAP > 3 - personAgreementController .first .third = .first ∧ - thematicSuffix .first .third = "-i" ∧ - personAgreementController .second .third = .second ∧ - thematicSuffix .second .third = "-i" ∧ - -- -u cases: controller picks P (= SAP), suffix marks non-dominant A - personAgreementController .third .first = .first ∧ - thematicSuffix .third .first = "-u" ∧ - personAgreementController .third .second = .second ∧ - thematicSuffix .third .second = "-u" := - ⟨rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl⟩ - --- ============================================================================ --- § 5: Verification --- ============================================================================ - -/-- "Dargic type" ([cysouw-2003]): in the clitic set, 1SG, 1PL, - and 2PL all receive the same marker (=da), while 2SG alone gets a - distinct marker (=de). This is the typologically rare opposition - described in the abstract: "2SG versus {1SG, 1PL, 2PL}". -/ -theorem dargic_type_clitic : - personMarker .clitic .first .sg = personMarker .clitic .first .pl ∧ - personMarker .clitic .first .pl = personMarker .clitic .second .pl ∧ - personMarker .clitic .second .sg ≠ personMarker .clitic .first .sg := by - refine ⟨rfl, rfl, ?_⟩; decide - -/-- SAP always wins over 3rd person. -/ -theorem sap_wins : - personAgreementController .first .third = .first ∧ - personAgreementController .third .first = .first ∧ - personAgreementController .second .third = .second ∧ - personAgreementController .third .second = .second := ⟨rfl, rfl, rfl, rfl⟩ - -/-- When both arguments are SAPs, the absolutive (P) controls. -/ -theorem both_sap_absolutive_wins : - personAgreementController .first .second = .second ∧ - personAgreementController .second .first = .first := ⟨rfl, rfl⟩ - -/-- The "SAP wins" rule directly reflects the person prominence hierarchy: - SAP (1st/2nd) > 3rd. This is the same hierarchy formalized in - `Features.Prominence.PersonLevel`. -/ -theorem sap_hierarchy_from_prominence : - PersonLevel.first.isSAP = true ∧ - PersonLevel.second.isSAP = true ∧ - PersonLevel.third.isSAP = false := ⟨rfl, rfl, rfl⟩ - -/-- Masculine and feminine prefixes are distinct. -/ -theorem gender_prefixes_distinct : - sgGenderPrefix .masculine ≠ sgGenderPrefix .feminine ∧ - sgGenderPrefix .masculine ≠ sgGenderPrefix .neuter ∧ - sgGenderPrefix .feminine ≠ sgGenderPrefix .neuter := by - refine ⟨?_, ?_, ?_⟩ <;> decide - -/-- Plural SAP-human and non-human prefixes are homophonous (both d-). - This is a typologically notable syncretism. -/ -theorem plural_syncretism : - plGenderPrefix .sapHuman = plGenderPrefix .nonHuman := rfl - -end Dargwa.Agreement +import Linglib.Features.Prominence +import Linglib.Core.UniversalDependencies +import Linglib.Features.Gender +import Linglib.Features.Number + +/-! +# Dargwa (Tanti) Agreement [sumbatova-2021] + +Dargwa is among the few Nakh-Dagestanian languages with both **gender +agreement** and **person agreement** ([sumbatova-2021] §4.5.8, §4.7.6). + +## Gender Agreement + +Three genders in the singular (masculine, feminine, neuter) and three +in the plural (1st/2nd person, human, non-human). Gender is almost +entirely semantic: masculine = male humans, feminine = female humans, +neuter = everything else. Gender agreement targets include verb roots, +preverbs, copulas, and some adjective roots. + +Gender agreement is controlled by the **absolutive argument** in clauses. +In copular clauses with two absolutives, the predicate controls agreement. + +## Person Agreement ("Dargic Type") + +Person agreement follows the hierarchy **1, 2 > 3** and +**absolutive > ergative**. The agreement paradigm configuration is the +"Dargic type" ([cysouw-2003]): a typologically rare opposition of +2SG versus {1SG, 1PL, 2PL}, where the 3rd person is usually unmarked. + +Three person-marker sets distribute across TAM paradigms: +1. **Clitic set**: present, preterite, perfect, propositive +2. **Irrealis set**: past habitual, future, conditional +3. **Optative set**: optative + +The 2SG marker is identical across the clitic set (*=de*) and past +tense (*=de*), creating a homophony that is typologically unusual. +-/ + +open Features (Number) + +namespace Dargwa.Agreement + +open Features.Prominence (PersonLevel) + +-- ============================================================================ +-- § 1: Gender System +-- ============================================================================ + +/-- Singular gender values. -/ +inductive SgGender where + | masculine -- w- (or ∅, realized as -j after vowels) + | feminine -- r- + | neuter -- b- (non-human, inanimate) + deriving DecidableEq, Repr + +/-- Plural gender values. These differ from singular genders. -/ +inductive PlGender where + | sapHuman -- d-: 1st/2nd person NPs + | human -- b-: 3rd person human plurals + | nonHuman -- d-: non-human plurals + deriving DecidableEq, Repr + +/-- Bridge to cross-linguistic surface gender. -/ +def SgGender.toSurfaceGender : SgGender → Features.SurfaceGender + | .masculine => .masculine + | .feminine => .feminine + | .neuter => .neuter + +/-- Gender agreement prefix on the verb stem. + The prefix immediately precedes the root in simplex verbs and + attaches to the light verb, preverb, or lexical stem in complex verbs + ([sumbatova-2021] §4.5.2.3, Table 4.12). -/ +def sgGenderPrefix : SgGender → String + | .masculine => "w-" + | .feminine => "r-" + | .neuter => "b-" + +def plGenderPrefix : PlGender → String + | .sapHuman => "d-" + | .human => "b-" + | .nonHuman => "d-" + +/-- Gender assignment is semantically transparent: masculine = male + humans, feminine = female humans, neuter = everything else + ([sumbatova-2021] §4.4.1). A small set of nouns have a + *variable* gender morpheme determined by the referent's actual + gender (if human) or the possessor's gender: e.g., *w-eˁ.ʔ* + 'proprietor (M)' / *r-eˁ.ʔ* 'proprietor (F)'. -/ +theorem gender_semantically_transparent : True := trivial + +-- ============================================================================ +-- § 2: Person Agreement +-- ============================================================================ + +/-- The three person-marker paradigm sets. -/ +inductive MarkerSet where + | clitic -- present, preterite, perfect, propositive + | irrealis -- past habitual, future, conditional + | optative -- optative + deriving DecidableEq, Repr + +/-- Person clitic/suffix forms (Table 4.20, 4.21 of [sumbatova-2021]). + Returns `none` when the person is unmarked. + + **Clitic set** ("Dargic type"): =da covers 1SG, 1PL, and 2PL + (ex. 34a: "I, we, you(PL) am, are doing"); =de is 2SG only. + Table 4.21 confirms: "person clitics: 2SG =de, 1SG/PL, 2PL =da". -/ +def personMarker : MarkerSet → PersonLevel → Number → Option String + -- Clitic set: =da for {1SG, 1PL, 2PL}, =de for {2SG}, none for {3} + | .clitic, .first, _ => some "=da" + | .clitic, .second, .Sing => some "=de" + | .clitic, .second, _ => some "=da" -- 2PL patterns with 1st person + | .clitic, .third, _ => none -- 3rd unmarked + -- Irrealis set + | .irrealis, .first, .Sing => some "-d" + | .irrealis, .first, _ => some "-haˁ" -- (> -he) + | .irrealis, .second, .Sing => some "-t:" -- (> -t) + | .irrealis, .second, _ => some "-t:-a" + | .irrealis, .third, _ => none + -- Optative set + | .optative, .first, _ => some "-a" + | .optative, .second, .Sing => some "-e" + | .optative, .second, _ => some "-a" -- + -ja allocutive + | .optative, .third, _ => none + +/-- 3rd person is unmarked in all paradigm sets. -/ +theorem third_unmarked : + personMarker .clitic .third .Sing = none ∧ + personMarker .clitic .third .Plur = none ∧ + personMarker .irrealis .third .Sing = none ∧ + personMarker .irrealis .third .Plur = none ∧ + personMarker .optative .third .Sing = none ∧ + personMarker .optative .third .Plur = none := ⟨rfl, rfl, rfl, rfl, rfl, rfl⟩ + +-- ============================================================================ +-- § 3: Agreement Control +-- ============================================================================ + +/-- Gender agreement controller: the absolutive argument. + In intransitive clauses: S (always absolutive). + In transitive clauses: P (absolutive), not A (ergative). + In copular clauses with two absolutives: the predicate. -/ +inductive GenderController where + | absolutive -- default: the absolutive NP + | predicate -- copular clause: predicate NP + | ergOrDat -- Tanti allows ergative/dative control optionally + deriving DecidableEq, Repr + +/-- Person agreement hierarchy: person (1, 2 > 3) and case + (absolutive > ergative). + + If one core argument is a SAP and the other is not, the verb + agrees with the SAP regardless of case. If both are SAPs, + agreement is with the absolutive. -/ +def personAgreementController (aPerson pPerson : PersonLevel) : PersonLevel := + match aPerson, pPerson with + | .first, .third => .first -- SAP wins + | .second, .third => .second -- SAP wins + | .third, .first => .first -- SAP wins + | .third, .second => .second -- SAP wins + | _, p => p -- both SAP → absolutive (P) wins + +-- ============================================================================ +-- § 4: Thematic Suffixes (Table 4.10 of [sumbatova-2021]) +-- ============================================================================ + +/-- Thematic suffix for transitive verbs, determined by the person features + of A and P arguments (Table 4.10, §4.5.2.5 of [sumbatova-2021]). + + *-i* when A is SAP (1st/2nd) and P is 3rd — the configuration where + A outranks P in the person hierarchy (1, 2 > 3). + *-u* otherwise (both SAP, or A is 3rd). -/ +def thematicSuffix (aPerson pPerson : PersonLevel) : String := + if aPerson.isSAP && !pPerson.isSAP then "-i" else "-u" + +/-- Intransitive thematic suffix: *-u* for SAP subjects, + *-ar* / *-an* for 3rd person subjects. -/ +def intransitiveThematicSuffix (sPerson : PersonLevel) : String := + if sPerson.isSAP then "-u" else "-ar" + +/-- The thematic suffix *-i* marks the same configuration that the + person agreement hierarchy resolves to the A-argument: SAP acting + on 3rd person. The suffix is a morphological reflex of hierarchy. -/ +theorem thematic_i_iff_sap_on_third : + thematicSuffix .first .third = "-i" ∧ + thematicSuffix .second .third = "-i" ∧ + thematicSuffix .third .third = "-u" ∧ + thematicSuffix .first .second = "-u" ∧ + thematicSuffix .third .first = "-u" := ⟨rfl, rfl, rfl, rfl, rfl⟩ + +/-- When thematic suffix is *-i* (A = SAP, P = 3), person agreement + controller selects A — the same argument that triggers *-i*. + When thematic suffix is *-u* (A = 3, P = SAP), person agreement + controller selects P. The suffix and the agreement controller + always pick the highest-ranked argument. -/ +theorem thematic_suffix_tracks_controller : + -- -i cases: controller picks A (= SAP), suffix marks SAP > 3 + personAgreementController .first .third = .first ∧ + thematicSuffix .first .third = "-i" ∧ + personAgreementController .second .third = .second ∧ + thematicSuffix .second .third = "-i" ∧ + -- -u cases: controller picks P (= SAP), suffix marks non-dominant A + personAgreementController .third .first = .first ∧ + thematicSuffix .third .first = "-u" ∧ + personAgreementController .third .second = .second ∧ + thematicSuffix .third .second = "-u" := + ⟨rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl⟩ + +-- ============================================================================ +-- § 5: Verification +-- ============================================================================ + +/-- "Dargic type" ([cysouw-2003]): in the clitic set, 1SG, 1PL, + and 2PL all receive the same marker (=da), while 2SG alone gets a + distinct marker (=de). This is the typologically rare opposition + described in the abstract: "2SG versus {1SG, 1PL, 2PL}". -/ +theorem dargic_type_clitic : + personMarker .clitic .first .Sing = personMarker .clitic .first .Plur ∧ + personMarker .clitic .first .Plur = personMarker .clitic .second .Plur ∧ + personMarker .clitic .second .Sing ≠ personMarker .clitic .first .Sing := by + refine ⟨rfl, rfl, ?_⟩; decide + +/-- SAP always wins over 3rd person. -/ +theorem sap_wins : + personAgreementController .first .third = .first ∧ + personAgreementController .third .first = .first ∧ + personAgreementController .second .third = .second ∧ + personAgreementController .third .second = .second := ⟨rfl, rfl, rfl, rfl⟩ + +/-- When both arguments are SAPs, the absolutive (P) controls. -/ +theorem both_sap_absolutive_wins : + personAgreementController .first .second = .second ∧ + personAgreementController .second .first = .first := ⟨rfl, rfl⟩ + +/-- The "SAP wins" rule directly reflects the person prominence hierarchy: + SAP (1st/2nd) > 3rd. This is the same hierarchy formalized in + `Features.Prominence.PersonLevel`. -/ +theorem sap_hierarchy_from_prominence : + PersonLevel.first.isSAP = true ∧ + PersonLevel.second.isSAP = true ∧ + PersonLevel.third.isSAP = false := ⟨rfl, rfl, rfl⟩ + +/-- Masculine and feminine prefixes are distinct. -/ +theorem gender_prefixes_distinct : + sgGenderPrefix .masculine ≠ sgGenderPrefix .feminine ∧ + sgGenderPrefix .masculine ≠ sgGenderPrefix .neuter ∧ + sgGenderPrefix .feminine ≠ sgGenderPrefix .neuter := by + refine ⟨?_, ?_, ?_⟩ <;> decide + +/-- Plural SAP-human and non-human prefixes are homophonous (both d-). + This is a typologically notable syncretism. -/ +theorem plural_syncretism : + plGenderPrefix .sapHuman = plGenderPrefix .nonHuman := rfl + +end Dargwa.Agreement diff --git a/Linglib/Fragments/French/Nouns.lean b/Linglib/Fragments/French/Nouns.lean index fe1335225..ce6d11b69 100644 --- a/Linglib/Fragments/French/Nouns.lean +++ b/Linglib/Fragments/French/Nouns.lean @@ -1,12 +1,15 @@ import Linglib.Features.Gender import Linglib.Core.UniversalDependencies import Linglib.Semantics.Kinds.NominalMappingParameter +import Linglib.Features.Number /-! # French Noun Lexicon Fragment French NP structure with gender. Bare arguments restricted ([chierchia-1998] [-arg, +pred]). -/ +open Features (Number) + namespace French.Nouns open Semantics.Kinds.NMP (BlockingPrinciple NominalMapping) @@ -69,10 +72,10 @@ def frenchMapping : NominalMapping := .predOnly /-- Create a definite NP (le/la/les) -/ -def defNP (n : NounEntry) (num : Number := .sg) : NP := +def defNP (n : NounEntry) (num : Number := .Sing) : NP := let det := match num, n.gender with - | .sg, .masculine => Determiner.le - | .sg, .feminine => Determiner.la + | .Sing, .masculine => Determiner.le + | .Sing, .feminine => Determiner.la | _, _ => Determiner.les -- plural (and fallback for non-binary number) { noun := n, number := num, isBare := false, determiner := some det } @@ -81,21 +84,21 @@ def indefNP (n : NounEntry) : NP := let det := match n.gender with | .feminine => Determiner.une | _ => Determiner.un -- masculine is default - { noun := n, number := .sg, isBare := false, determiner := some det } + { noun := n, number := .Sing, isBare := false, determiner := some det } /-- Create an indefinite plural NP (des) -/ def desNP (n : NounEntry) : NP := - { noun := n, number := .pl, isBare := false, determiner := some .des } + { noun := n, number := .Plur, isBare := false, determiner := some .des } /-- Create a partitive NP (du/de la) for mass nouns -/ def partNP (n : NounEntry) : NP := let det := match n.gender with | .feminine => Determiner.dela | _ => Determiner.du -- masculine is default - { noun := n, number := .sg, isBare := false, determiner := some det } + { noun := n, number := .Sing, isBare := false, determiner := some det } /-- Create a bare NP (restricted in French) -/ -def bareNP (n : NounEntry) (num : Number := .sg) : NP := +def bareNP (n : NounEntry) (num : Number := .Sing) : NP := { noun := n, number := num, isBare := true } @@ -152,7 +155,7 @@ example : bareSingularLicensed = false := rfl def leChien : NP := defNP chien /-- "les chiens" (the dogs) -/ -def lesChiens : NP := defNP chien .pl +def lesChiens : NP := defNP chien .Plur /-- "un chien" (a dog) -/ def unChien : NP := indefNP chien diff --git a/Linglib/Fragments/German/AdjAgreement.lean b/Linglib/Fragments/German/AdjAgreement.lean index 0718cf810..1c8a62da2 100644 --- a/Linglib/Fragments/German/AdjAgreement.lean +++ b/Linglib/Fragments/German/AdjAgreement.lean @@ -24,7 +24,7 @@ def predFeatures : List MAGFeatureType := [] /-- German attributive adjectives carry φ + κ (strong endings). -/ def attrFeatures : List MAGFeatureType := - [ .phi (.number .pl), .phi (.number .sg) + [ .phi (.number .Plur), .phi (.number .Sing) , .phi (.gender 0), .phi (.gender 1), .phi (.gender 2) , .kappa .nom, .kappa .acc, .kappa .dat, .kappa .gen ] diff --git a/Linglib/Fragments/Greek/StandardModern/AdjAgreement.lean b/Linglib/Fragments/Greek/StandardModern/AdjAgreement.lean index 382a7277f..a7975ef19 100644 --- a/Linglib/Fragments/Greek/StandardModern/AdjAgreement.lean +++ b/Linglib/Fragments/Greek/StandardModern/AdjAgreement.lean @@ -21,7 +21,7 @@ open Minimalist.Modification /-- φ-features realized on Greek adjectives: number and gender. -/ private def phiFeatures : List MAGFeatureType := - [ .phi (.number .pl), .phi (.number .sg) + [ .phi (.number .Plur), .phi (.number .Sing) , .phi (.gender 0), .phi (.gender 1), .phi (.gender 2) ] /-- κ-features realized on Greek adjectives: full 3-case system diff --git a/Linglib/Fragments/Italian/AdjAgreement.lean b/Linglib/Fragments/Italian/AdjAgreement.lean index 27f33aa6b..7a1733343 100644 --- a/Linglib/Fragments/Italian/AdjAgreement.lean +++ b/Linglib/Fragments/Italian/AdjAgreement.lean @@ -21,7 +21,7 @@ open Minimalist.Modification /-- Italian adjective φ-features: number and gender only. -/ def phiFeatures : List MAGFeatureType := - [ .phi (.number .pl), .phi (.number .sg) + [ .phi (.number .Plur), .phi (.number .Sing) , .phi (.gender 0), .phi (.gender 1) ] /-- Italian DP features include κ (case is always a DP feature per fn 17, diff --git a/Linglib/Fragments/Italian/Nouns.lean b/Linglib/Fragments/Italian/Nouns.lean index 1ace223dd..6f8d84736 100644 --- a/Linglib/Fragments/Italian/Nouns.lean +++ b/Linglib/Fragments/Italian/Nouns.lean @@ -107,9 +107,9 @@ structure NP where modeled here). -/ def defNP (n : NounEntry) (num : Number := .sg) : NP := let det := match num, n.gender with - | .sg, .feminine => Determiner.la - | .sg, _ => Determiner.il -- masculine is default - | .pl, .feminine => Determiner.le + | .Sing, .feminine => Determiner.la + | .Sing, _ => Determiner.il -- masculine is default + | .Plur, .feminine => Determiner.le | _, _ => Determiner.i { noun := n, number := num, isBare := false, determiner := some det } @@ -123,9 +123,9 @@ def indefNP (n : NounEntry) : NP := /-- Create a partitive NP (del/della for mass, dei/delle for plural). -/ def partNP (n : NounEntry) (num : Number := .sg) : NP := let det := match num, n.gender with - | .sg, .feminine => Determiner.della - | .sg, _ => Determiner.del -- masculine is default - | .pl, .feminine => Determiner.delle + | .Sing, .feminine => Determiner.della + | .Sing, _ => Determiner.del -- masculine is default + | .Plur, .feminine => Determiner.delle | _, _ => Determiner.dei { noun := n, number := num, isBare := false, determiner := some det } diff --git a/Linglib/Fragments/Jarawara/PossessedNouns.lean b/Linglib/Fragments/Jarawara/PossessedNouns.lean index 303b8a083..7a5fba631 100644 --- a/Linglib/Fragments/Jarawara/PossessedNouns.lean +++ b/Linglib/Fragments/Jarawara/PossessedNouns.lean @@ -1,268 +1,271 @@ -import Linglib.Morphology.DM.NominalStructure -import Linglib.Typology.Possession -import Linglib.Core.UniversalDependencies -import Linglib.Features.Gender - -/-! -# Jarawara Possessed Nouns [adamson-2024] [dixon-2004] - -Inalienably possessed noun classes and the *mano* 'arm' paradigm -in Jarawara (Arawan), drawn from [adamson-2024] §3.2 and -[dixon-2004]. - -## Key facts - -- Jarawara has two genders: masculine (marked, [+MASC] on n) and - feminine (unmarked, plain n) -- All ~175 iPossessable nouns are feminine when used "free" (without - a possessor), consistent with being licensed by plain n -- iPossession is expressed by direct juxtaposition; aPossession uses - the marker *kaa* -- The "masculine"/"feminine" alternations on possessed nouns reflect - φ-agreement with the iPossessor, not gender assignment - -## Semantic Classification ([dixon-2004] p. 311) - -The iPossessable class maps onto the upper portion of the -cross-linguistic inalienability hierarchy from `Possession.Typology`. --/ - -namespace Jarawara - -open Typology.Possession - --- ============================================================================ --- § 1: Semantic Classes of iPossessable Nouns (Table 3) --- ============================================================================ - -/-- Semantic classification of Jarawara iPossessable nouns - ([dixon-2004] p. 311; [adamson-2024] Table 3). -/ -structure PossessedNounClass where - label : String - memberCount : Nat - examples : List (String × String) -- (Jarawara form, English gloss) - /-- Nearest match on the cross-linguistic inalienability hierarchy. -/ - inalienabilityRank : InalienabilityRank - deriving Repr - -def orientation : PossessedNounClass := - { label := "Orientation" - , memberCount := 17 - , examples := [("mese/mese", "top surface of"), - ("tori/toro", "inside of")] - , inalienabilityRank := .spatialRelation } - -def wholeAndPart : PossessedNounClass := - { label := "Whole and part" - , memberCount := 14 - , examples := [("boni/bono", "whole thing"), - ("kote/kote", "piece")] - , inalienabilityRank := .partWhole } - -def bodyParts : PossessedNounClass := - { label := "Body parts" - , memberCount := 62 - , examples := [("noki/noko", "eye/face"), - ("tame/teme", "foot"), - ("jifori/jifori", "tail")] - , inalienabilityRank := .bodyPart } - -def partsOfPlants : PossessedNounClass := - { label := "Parts of plants" - , memberCount := 19 - , examples := [("mowe/mowe", "flower"), - ("mati/matone", "cord, rope")] - , inalienabilityRank := .partWhole } - -def physicalCharacteristics : PossessedNounClass := - { label := "Physical characteristics/properties" - , memberCount := 18 - , examples := [("kakitiri/kakitiri", "itch"), - ("mahi/maho", "smell")] - , inalienabilityRank := .culturalItem } - -def noiseAndLanguage : PossessedNounClass := - { label := "Noise and language" - , memberCount := 4 - , examples := [("moni/moni", "noise"), - ("ini/ino", "name")] - , inalienabilityRank := .culturalItem } - -def imageAndDream : PossessedNounClass := - { label := "Image and dream" - , memberCount := 5 - , examples := [("hani/hano", "design/picture"), - ("watari/watari(ne)", "dream")] - , inalienabilityRank := .culturalItem } - -def association : PossessedNounClass := - { label := "Association" - , memberCount := 9 - , examples := [("tehe/tehene", "something mixed with"), - ("tase/tesene", "companion of")] - , inalienabilityRank := .culturalItem } - -def containers : PossessedNounClass := - { label := "Containers and other artefacts" - , memberCount := 7 - , examples := [("wije/wijene", "vessel, container"), - ("atori/atori", "ornament")] - , inalienabilityRank := .culturalItem } - -def waterFireLight : PossessedNounClass := - { label := "Water, fire, and light" - , memberCount := 11 - , examples := [("jiji/jifone", "fire, firewood"), - ("fehe/fehene", "liquid, juice, sap, water")] - , inalienabilityRank := .culturalItem } - -def food : PossessedNounClass := - { label := "Food" - , memberCount := 3 - , examples := [("tafe/tefe", "food"), - ("saharine/saharine", "broth, mush")] - , inalienabilityRank := .culturalItem } - -def place : PossessedNounClass := - { label := "Place" - , memberCount := 6 - , examples := [("hawi/hawine", "path"), - ("tame/temene", "grave")] - , inalienabilityRank := .spatialRelation } - -/-- All 12 semantic classes of iPossessable nouns. -/ -def allClasses : List PossessedNounClass := - [orientation, wholeAndPart, bodyParts, partsOfPlants, - physicalCharacteristics, noiseAndLanguage, imageAndDream, - association, containers, waterFireLight, food, place] - -/-- Total iPossessable nouns: ~175 ([dixon-2004] p. 310). -/ -theorem total_ipossessable : - (allClasses.map (·.memberCount)).foldl (· + ·) 0 = 175 := by native_decide - --- ============================================================================ --- § 2: *mano* 'arm' Paradigm (Table 5; [dixon-2004] p. 315) --- ============================================================================ - -/-- Person–number features of a Jarawara possessor. -/ -inductive Person where | first | second | third deriving DecidableEq, Repr -inductive PossGender where | masc | fem deriving DecidableEq, Repr - -/-- Bridge to cross-linguistic surface gender. -/ -def PossGender.toSurfaceGender : PossGender → Features.SurfaceGender - | .masc => .masculine - | .fem => .feminine - -/-- A possessor with full φ-features. Third person distinguishes gender; - first and second person can be singular or plural, with clusivity - for first person plural. -/ -structure Possessor where - person : Person - number : Number - gender : Option PossGender := none -- only for 3rd person - deriving DecidableEq, Repr - -/-- Possessed noun form: "masculine" (mano) or "feminine" (mani). - These labels follow [dixon-2004]'s terminology; they reflect - φ-agreement with the possessor, not the noun's own gender - (which is always feminine). -/ -inductive PossessedForm where | mascForm | femForm - deriving DecidableEq, Repr - -/-! ### Derived mano paradigm ([adamson-2024] Appendix B) - -The mano/mani alternation is derived from three components: - -1. **MARKED features**: [PARTICIPANT] (1st/2nd person) and [MASC] - (masculine possessor gender) are both MARKED. -2. **Impoverishment** (ex. 63): [MASC] → ∅ / [PL] and - [MASC] → ∅ / [PARTICIPANT]. Impoverishment deletes [MASC] when - [PL] or [PARTICIPANT] is present. -3. **VI** (A7): √MANV ↔ *mano* / [MARKED]; √MANV ↔ *mani* (elsewhere). - -The derivation: -- 1st/2nd (any number): [PARTICIPANT] is MARKED → *mano* -- 3.M.SG: [MASC] survives (no [PL], no [PARTICIPANT]) → *mano* -- 3.F.SG: no MARKED feature → *mani* -- 3.M.PL: [MASC] deleted by impoverishment / [PL]; no [PARTICIPANT] → *mani* -- 3.F.PL / 3.PL: no MARKED feature → *mani* --/ - -/-- Whether the possessor is a speech act participant ([PARTICIPANT]). -/ -def Possessor.isParticipant (p : Possessor) : Bool := - p.person != .third - -/-- Whether the possessor has [MASC] that survives impoverishment. - [MASC] is deleted when [PL] or [PARTICIPANT] is present. -/ -def Possessor.mascSurvivesImpoverishment (p : Possessor) : Bool := - match p.gender with - | some .masc => !p.isParticipant && p.number == .sg - | _ => false - -/-- Whether any MARKED feature remains after impoverishment. - MARKED = [PARTICIPANT] or [MASC] (if it survives). -/ -def Possessor.hasMarkedFeature (p : Possessor) : Bool := - p.isParticipant || p.mascSurvivesImpoverishment - -/-- The possessed form of *mano* 'arm', derived from MARKED features, - impoverishment, and VI (A7). -/ -def manoForm (p : Possessor) : PossessedForm := - if p.hasMarkedFeature then .mascForm else .femForm - -/-- Table 5/6 verification: each possessor combination. -/ -theorem mano_1sg : manoForm ⟨.first, .sg, none⟩ = .mascForm := rfl -theorem mano_2sg : manoForm ⟨.second, .sg, none⟩ = .mascForm := rfl -theorem mano_1pl : manoForm ⟨.first, .pl, none⟩ = .mascForm := rfl -theorem mano_2pl : manoForm ⟨.second, .pl, none⟩ = .mascForm := rfl -theorem mano_3m_sg : manoForm ⟨.third, .sg, some .masc⟩ = .mascForm := rfl -theorem mano_3f_sg : manoForm ⟨.third, .sg, some .fem⟩ = .femForm := rfl -theorem mano_3pl : manoForm ⟨.third, .pl, none⟩ = .femForm := rfl -/-- 3.M.PL: [MASC] is deleted by impoverishment in context of [PL], - and 3rd person is not [PARTICIPANT], so no MARKED feature remains. -/ -theorem mano_3m_pl : manoForm ⟨.third, .pl, some .masc⟩ = .femForm := rfl -/-- 3.F.PL: no [MASC], 3rd person not [PARTICIPANT] → elsewhere. -/ -theorem mano_3f_pl : manoForm ⟨.third, .pl, some .fem⟩ = .femForm := rfl - --- ============================================================================ --- § 3: Free vs Possessed Forms (Table 4; [dixon-2004] p. 312) --- ============================================================================ - -/-- A subset of nouns with attested free and iPossessed forms. - Free forms are all feminine ([dixon-2004] pp. 80, 285). -/ -structure FreeVsPossessed where - free : String - iPossessed : String - gloss : String - deriving DecidableEq, Repr - -def freeVsPossessedForms : List FreeVsPossessed := - [ ⟨"faha", "fehe/fehe-ne", "water / liquid, juice, sap, water"⟩ - , ⟨"mato", "mati/mato-ne", "cord, rope, vine / cord, rope"⟩ - , ⟨"hawi", "hawi/hawi-ne", "path / path"⟩ - , ⟨"tona", "tone/tone", "bone / bone"⟩ - , ⟨"neme", "neme/neme", "sky / top part of"⟩ - , ⟨"bofe", "bofe/bofe", "ground / bottom part of"⟩ - , ⟨"tama", "tame/teme-ne", "grave/hole / grave/hole for"⟩ ] - --- ============================================================================ --- § 4: Bridge to Inalienability Hierarchy --- ============================================================================ - -/-- All Jarawara iPossessable classes fall at or above `culturalItem` on - the cross-linguistic inalienability hierarchy. The three highest-ranked - categories (body parts, spatial relations, part-whole) account for - 112/175 = 64% of all iPossessable nouns. -/ -theorem all_classes_inalienable : - allClasses.all (·.inalienabilityRank.toNat ≥ InalienabilityRank.culturalItem.toNat) - = true := by native_decide - -/-- The four highest-ranked inalienable categories (body parts, spatial - relations, part-whole, and kinship-adjacent) account for the majority: - 62 (body parts) + 17 (orientation) + 14 (whole/part) + 19 (plant parts) - + 6 (place) = 118 / 175. -/ -theorem core_inalienable_majority : - let core := allClasses.filter (·.inalienabilityRank.toNat ≥ - InalienabilityRank.partWhole.toNat) - (core.map (·.memberCount)).foldl (· + ·) 0 = 118 := by native_decide - -end Jarawara +import Linglib.Morphology.DM.NominalStructure +import Linglib.Typology.Possession +import Linglib.Core.UniversalDependencies +import Linglib.Features.Gender +import Linglib.Features.Number + +/-! +# Jarawara Possessed Nouns [adamson-2024] [dixon-2004] + +Inalienably possessed noun classes and the *mano* 'arm' paradigm +in Jarawara (Arawan), drawn from [adamson-2024] §3.2 and +[dixon-2004]. + +## Key facts + +- Jarawara has two genders: masculine (marked, [+MASC] on n) and + feminine (unmarked, plain n) +- All ~175 iPossessable nouns are feminine when used "free" (without + a possessor), consistent with being licensed by plain n +- iPossession is expressed by direct juxtaposition; aPossession uses + the marker *kaa* +- The "masculine"/"feminine" alternations on possessed nouns reflect + φ-agreement with the iPossessor, not gender assignment + +## Semantic Classification ([dixon-2004] p. 311) + +The iPossessable class maps onto the upper portion of the +cross-linguistic inalienability hierarchy from `Possession.Typology`. +-/ + +open Features (Number) + +namespace Jarawara + +open Typology.Possession + +-- ============================================================================ +-- § 1: Semantic Classes of iPossessable Nouns (Table 3) +-- ============================================================================ + +/-- Semantic classification of Jarawara iPossessable nouns + ([dixon-2004] p. 311; [adamson-2024] Table 3). -/ +structure PossessedNounClass where + label : String + memberCount : Nat + examples : List (String × String) -- (Jarawara form, English gloss) + /-- Nearest match on the cross-linguistic inalienability hierarchy. -/ + inalienabilityRank : InalienabilityRank + deriving Repr + +def orientation : PossessedNounClass := + { label := "Orientation" + , memberCount := 17 + , examples := [("mese/mese", "top surface of"), + ("tori/toro", "inside of")] + , inalienabilityRank := .spatialRelation } + +def wholeAndPart : PossessedNounClass := + { label := "Whole and part" + , memberCount := 14 + , examples := [("boni/bono", "whole thing"), + ("kote/kote", "piece")] + , inalienabilityRank := .partWhole } + +def bodyParts : PossessedNounClass := + { label := "Body parts" + , memberCount := 62 + , examples := [("noki/noko", "eye/face"), + ("tame/teme", "foot"), + ("jifori/jifori", "tail")] + , inalienabilityRank := .bodyPart } + +def partsOfPlants : PossessedNounClass := + { label := "Parts of plants" + , memberCount := 19 + , examples := [("mowe/mowe", "flower"), + ("mati/matone", "cord, rope")] + , inalienabilityRank := .partWhole } + +def physicalCharacteristics : PossessedNounClass := + { label := "Physical characteristics/properties" + , memberCount := 18 + , examples := [("kakitiri/kakitiri", "itch"), + ("mahi/maho", "smell")] + , inalienabilityRank := .culturalItem } + +def noiseAndLanguage : PossessedNounClass := + { label := "Noise and language" + , memberCount := 4 + , examples := [("moni/moni", "noise"), + ("ini/ino", "name")] + , inalienabilityRank := .culturalItem } + +def imageAndDream : PossessedNounClass := + { label := "Image and dream" + , memberCount := 5 + , examples := [("hani/hano", "design/picture"), + ("watari/watari(ne)", "dream")] + , inalienabilityRank := .culturalItem } + +def association : PossessedNounClass := + { label := "Association" + , memberCount := 9 + , examples := [("tehe/tehene", "something mixed with"), + ("tase/tesene", "companion of")] + , inalienabilityRank := .culturalItem } + +def containers : PossessedNounClass := + { label := "Containers and other artefacts" + , memberCount := 7 + , examples := [("wije/wijene", "vessel, container"), + ("atori/atori", "ornament")] + , inalienabilityRank := .culturalItem } + +def waterFireLight : PossessedNounClass := + { label := "Water, fire, and light" + , memberCount := 11 + , examples := [("jiji/jifone", "fire, firewood"), + ("fehe/fehene", "liquid, juice, sap, water")] + , inalienabilityRank := .culturalItem } + +def food : PossessedNounClass := + { label := "Food" + , memberCount := 3 + , examples := [("tafe/tefe", "food"), + ("saharine/saharine", "broth, mush")] + , inalienabilityRank := .culturalItem } + +def place : PossessedNounClass := + { label := "Place" + , memberCount := 6 + , examples := [("hawi/hawine", "path"), + ("tame/temene", "grave")] + , inalienabilityRank := .spatialRelation } + +/-- All 12 semantic classes of iPossessable nouns. -/ +def allClasses : List PossessedNounClass := + [orientation, wholeAndPart, bodyParts, partsOfPlants, + physicalCharacteristics, noiseAndLanguage, imageAndDream, + association, containers, waterFireLight, food, place] + +/-- Total iPossessable nouns: ~175 ([dixon-2004] p. 310). -/ +theorem total_ipossessable : + (allClasses.map (·.memberCount)).foldl (· + ·) 0 = 175 := by native_decide + +-- ============================================================================ +-- § 2: *mano* 'arm' Paradigm (Table 5; [dixon-2004] p. 315) +-- ============================================================================ + +/-- Person–number features of a Jarawara possessor. -/ +inductive Person where | first | second | third deriving DecidableEq, Repr +inductive PossGender where | masc | fem deriving DecidableEq, Repr + +/-- Bridge to cross-linguistic surface gender. -/ +def PossGender.toSurfaceGender : PossGender → Features.SurfaceGender + | .masc => .masculine + | .fem => .feminine + +/-- A possessor with full φ-features. Third person distinguishes gender; + first and second person can be singular or plural, with clusivity + for first person plural. -/ +structure Possessor where + person : Person + number : Number + gender : Option PossGender := none -- only for 3rd person + deriving DecidableEq, Repr + +/-- Possessed noun form: "masculine" (mano) or "feminine" (mani). + These labels follow [dixon-2004]'s terminology; they reflect + φ-agreement with the possessor, not the noun's own gender + (which is always feminine). -/ +inductive PossessedForm where | mascForm | femForm + deriving DecidableEq, Repr + +/-! ### Derived mano paradigm ([adamson-2024] Appendix B) + +The mano/mani alternation is derived from three components: + +1. **MARKED features**: [PARTICIPANT] (1st/2nd person) and [MASC] + (masculine possessor gender) are both MARKED. +2. **Impoverishment** (ex. 63): [MASC] → ∅ / [PL] and + [MASC] → ∅ / [PARTICIPANT]. Impoverishment deletes [MASC] when + [PL] or [PARTICIPANT] is present. +3. **VI** (A7): √MANV ↔ *mano* / [MARKED]; √MANV ↔ *mani* (elsewhere). + +The derivation: +- 1st/2nd (any number): [PARTICIPANT] is MARKED → *mano* +- 3.M.SG: [MASC] survives (no [PL], no [PARTICIPANT]) → *mano* +- 3.F.SG: no MARKED feature → *mani* +- 3.M.PL: [MASC] deleted by impoverishment / [PL]; no [PARTICIPANT] → *mani* +- 3.F.PL / 3.PL: no MARKED feature → *mani* +-/ + +/-- Whether the possessor is a speech act participant ([PARTICIPANT]). -/ +def Possessor.isParticipant (p : Possessor) : Bool := + p.person != .third + +/-- Whether the possessor has [MASC] that survives impoverishment. + [MASC] is deleted when [PL] or [PARTICIPANT] is present. -/ +def Possessor.mascSurvivesImpoverishment (p : Possessor) : Bool := + match p.gender with + | some .masc => !p.isParticipant && p.number == .sg + | _ => false + +/-- Whether any MARKED feature remains after impoverishment. + MARKED = [PARTICIPANT] or [MASC] (if it survives). -/ +def Possessor.hasMarkedFeature (p : Possessor) : Bool := + p.isParticipant || p.mascSurvivesImpoverishment + +/-- The possessed form of *mano* 'arm', derived from MARKED features, + impoverishment, and VI (A7). -/ +def manoForm (p : Possessor) : PossessedForm := + if p.hasMarkedFeature then .mascForm else .femForm + +/-- Table 5/6 verification: each possessor combination. -/ +theorem mano_1sg : manoForm ⟨.first, .sg, none⟩ = .mascForm := rfl +theorem mano_2sg : manoForm ⟨.second, .sg, none⟩ = .mascForm := rfl +theorem mano_1pl : manoForm ⟨.first, .pl, none⟩ = .mascForm := rfl +theorem mano_2pl : manoForm ⟨.second, .pl, none⟩ = .mascForm := rfl +theorem mano_3m_sg : manoForm ⟨.third, .sg, some .masc⟩ = .mascForm := rfl +theorem mano_3f_sg : manoForm ⟨.third, .sg, some .fem⟩ = .femForm := rfl +theorem mano_3pl : manoForm ⟨.third, .pl, none⟩ = .femForm := rfl +/-- 3.M.PL: [MASC] is deleted by impoverishment in context of [PL], + and 3rd person is not [PARTICIPANT], so no MARKED feature remains. -/ +theorem mano_3m_pl : manoForm ⟨.third, .pl, some .masc⟩ = .femForm := rfl +/-- 3.F.PL: no [MASC], 3rd person not [PARTICIPANT] → elsewhere. -/ +theorem mano_3f_pl : manoForm ⟨.third, .pl, some .fem⟩ = .femForm := rfl + +-- ============================================================================ +-- § 3: Free vs Possessed Forms (Table 4; [dixon-2004] p. 312) +-- ============================================================================ + +/-- A subset of nouns with attested free and iPossessed forms. + Free forms are all feminine ([dixon-2004] pp. 80, 285). -/ +structure FreeVsPossessed where + free : String + iPossessed : String + gloss : String + deriving DecidableEq, Repr + +def freeVsPossessedForms : List FreeVsPossessed := + [ ⟨"faha", "fehe/fehe-ne", "water / liquid, juice, sap, water"⟩ + , ⟨"mato", "mati/mato-ne", "cord, rope, vine / cord, rope"⟩ + , ⟨"hawi", "hawi/hawi-ne", "path / path"⟩ + , ⟨"tona", "tone/tone", "bone / bone"⟩ + , ⟨"neme", "neme/neme", "sky / top part of"⟩ + , ⟨"bofe", "bofe/bofe", "ground / bottom part of"⟩ + , ⟨"tama", "tame/teme-ne", "grave/hole / grave/hole for"⟩ ] + +-- ============================================================================ +-- § 4: Bridge to Inalienability Hierarchy +-- ============================================================================ + +/-- All Jarawara iPossessable classes fall at or above `culturalItem` on + the cross-linguistic inalienability hierarchy. The three highest-ranked + categories (body parts, spatial relations, part-whole) account for + 112/175 = 64% of all iPossessable nouns. -/ +theorem all_classes_inalienable : + allClasses.all (·.inalienabilityRank.toNat ≥ InalienabilityRank.culturalItem.toNat) + = true := by native_decide + +/-- The four highest-ranked inalienable categories (body parts, spatial + relations, part-whole, and kinship-adjacent) account for the majority: + 62 (body parts) + 17 (orientation) + 14 (whole/part) + 19 (plant parts) + + 6 (place) = 118 / 175. -/ +theorem core_inalienable_majority : + let core := allClasses.filter (·.inalienabilityRank.toNat ≥ + InalienabilityRank.partWhole.toNat) + (core.map (·.memberCount)).foldl (· + ·) 0 = 118 := by native_decide + +end Jarawara diff --git a/Linglib/Fragments/Slavic/Russian/AdjAgreement.lean b/Linglib/Fragments/Slavic/Russian/AdjAgreement.lean index 63385a04e..071b34aeb 100644 --- a/Linglib/Fragments/Slavic/Russian/AdjAgreement.lean +++ b/Linglib/Fragments/Slavic/Russian/AdjAgreement.lean @@ -21,7 +21,7 @@ open Minimalist.Modification /-- Russian long-form features: φ (number, gender) + κ (6-case). -/ def longFormFeatures : List MAGFeatureType := - [ .phi (.number .pl), .phi (.number .sg) + [ .phi (.number .Plur), .phi (.number .Sing) , .phi (.gender 0), .phi (.gender 1), .phi (.gender 2) , .kappa .nom, .kappa .acc, .kappa .dat , .kappa .gen, .kappa .abl ] diff --git a/Linglib/Syntax/Minimalist/Agree.lean b/Linglib/Syntax/Minimalist/Agree.lean index 8328604bd..a0bd37f7e 100644 --- a/Linglib/Syntax/Minimalist/Agree.lean +++ b/Linglib/Syntax/Minimalist/Agree.lean @@ -265,10 +265,10 @@ structure TAgree where subjFeatures : FeatureBundle -- T has unvalued phi t_has_uphi : hasUnvaluedFeature tFeatures (.phi (.person .third)) = true ∨ - hasUnvaluedFeature tFeatures (.phi (.number .sg)) = true + hasUnvaluedFeature tFeatures (.phi (.number .Sing)) = true -- Subject has valued phi subj_has_phi : hasValuedFeature subjFeatures (.phi (.person .third)) = true ∨ - hasValuedFeature subjFeatures (.phi (.number .sg)) = true + hasValuedFeature subjFeatures (.phi (.number .Sing)) = true /-- C-Agree: C probes for [Q] feature @@ -606,7 +606,7 @@ def mamInflSatisfaction : SatisfactionCond := (no Voice_TR in the way). Feature match is satisfied → real agreement. -/ theorem mam_intransitive_satisfied : mamInflSatisfaction.isSatisfied - [.valued (.phi (.person .first)), .valued (.phi (.number .sg))] + [.valued (.phi (.person .first)), .valued (.phi (.number .Sing))] none = true := by rfl /-- Transitive environment: the probe encounters Voice_TR (category.v). @@ -621,7 +621,7 @@ theorem mam_transitive_no_copy : /-- In the intransitive case, features ARE copied — yielding real agreement. -/ theorem mam_intransitive_copies : mamInflSatisfaction.copiedFeatures - [.valued (.phi (.person .first)), .valued (.phi (.number .sg))] + [.valued (.phi (.person .first)), .valued (.phi (.number .Sing))] none = true := by rfl end Minimalist From 2ed3902b6a35af11669812557df378839b507153 Mon Sep 17 00:00:00 2001 From: Robert Hawkins Date: Thu, 4 Jun 2026 08:52:55 -0700 Subject: [PATCH 3/3] fix(Fragments,Studies): finish UD constructor migration across graph --- Linglib/Fragments/Italian/Nouns.lean | 10 +-- Linglib/Fragments/Italian/Pronouns.lean | 4 ++ .../Fragments/Jarawara/PossessedNouns.lean | 20 +++--- Linglib/Fragments/Mayan/Kiche/Agreement.lean | 3 + Linglib/Fragments/Spanish/Clitics.lean | 4 ++ .../Semantics/Presupposition/PhiFeatures.lean | 12 ++-- Linglib/Semantics/Quantification/Lexicon.lean | 3 + Linglib/Studies/Adamson2024.lean | 6 +- Linglib/Studies/ElkinsTorrenceBrown2026.lean | 2 +- Linglib/Studies/Harbour2016.lean | 4 +- Linglib/Studies/Preminger2014.lean | 2 +- Linglib/Studies/Scott2023Agreement.lean | 64 +++++++++---------- Linglib/Syntax/Minimalist/SpeechActs.lean | 4 ++ 13 files changed, 78 insertions(+), 60 deletions(-) diff --git a/Linglib/Fragments/Italian/Nouns.lean b/Linglib/Fragments/Italian/Nouns.lean index 6f8d84736..5ae0a800d 100644 --- a/Linglib/Fragments/Italian/Nouns.lean +++ b/Linglib/Fragments/Italian/Nouns.lean @@ -105,7 +105,7 @@ structure NP where Uses `il` for masculine singular and `la` for feminine singular (the lo/gli allomorphs are phonologically conditioned and not modeled here). -/ -def defNP (n : NounEntry) (num : Number := .sg) : NP := +def defNP (n : NounEntry) (num : Number := .Sing) : NP := let det := match num, n.gender with | .Sing, .feminine => Determiner.la | .Sing, _ => Determiner.il -- masculine is default @@ -118,10 +118,10 @@ def indefNP (n : NounEntry) : NP := let det := match n.gender with | .feminine => Determiner.una | _ => Determiner.un -- masculine is default - { noun := n, number := .sg, isBare := false, determiner := some det } + { noun := n, number := .Sing, isBare := false, determiner := some det } /-- Create a partitive NP (del/della for mass, dei/delle for plural). -/ -def partNP (n : NounEntry) (num : Number := .sg) : NP := +def partNP (n : NounEntry) (num : Number := .Sing) : NP := let det := match num, n.gender with | .Sing, .feminine => Determiner.della | .Sing, _ => Determiner.del -- masculine is default @@ -130,7 +130,7 @@ def partNP (n : NounEntry) (num : Number := .sg) : NP := { noun := n, number := num, isBare := false, determiner := some det } /-- Create a bare NP (restricted in Italian). -/ -def bareNP (n : NounEntry) (num : Number := .sg) : NP := +def bareNP (n : NounEntry) (num : Number := .Sing) : NP := { noun := n, number := num, isBare := true } -- ============================================================================ @@ -226,7 +226,7 @@ def unGatto : NP := indefNP gatto def delVino : NP := partNP vino /-- "dei libri" (some books, partitive plural) -/ -def deiLibri : NP := partNP libro .pl +def deiLibri : NP := partNP libro .Plur example : ilLibro.isBare = false := rfl example : ilLibro.determiner = some .il := rfl diff --git a/Linglib/Fragments/Italian/Pronouns.lean b/Linglib/Fragments/Italian/Pronouns.lean index d507c0398..df38d1151 100644 --- a/Linglib/Fragments/Italian/Pronouns.lean +++ b/Linglib/Fragments/Italian/Pronouns.lean @@ -1,6 +1,8 @@ import Linglib.Syntax.Pronoun.Basic import Linglib.Syntax.Pronoun.Capabilities import Linglib.Core.UniversalDependencies +import Linglib.Features.Number +import Linglib.Features.Person /-! # Italian Pronoun and Clitic Fragment @@ -28,6 +30,8 @@ and reflexive cases, while 3sg/3pl are not. | 3pl | li/le | loro | si | NOT syncretic -/ +open Features (Number Person) + namespace Italian.Pronouns open Pronoun diff --git a/Linglib/Fragments/Jarawara/PossessedNouns.lean b/Linglib/Fragments/Jarawara/PossessedNouns.lean index 7a5fba631..53d3e4c91 100644 --- a/Linglib/Fragments/Jarawara/PossessedNouns.lean +++ b/Linglib/Fragments/Jarawara/PossessedNouns.lean @@ -199,7 +199,7 @@ def Possessor.isParticipant (p : Possessor) : Bool := [MASC] is deleted when [PL] or [PARTICIPANT] is present. -/ def Possessor.mascSurvivesImpoverishment (p : Possessor) : Bool := match p.gender with - | some .masc => !p.isParticipant && p.number == .sg + | some .masc => !p.isParticipant && p.number == .Sing | _ => false /-- Whether any MARKED feature remains after impoverishment. @@ -213,18 +213,18 @@ def manoForm (p : Possessor) : PossessedForm := if p.hasMarkedFeature then .mascForm else .femForm /-- Table 5/6 verification: each possessor combination. -/ -theorem mano_1sg : manoForm ⟨.first, .sg, none⟩ = .mascForm := rfl -theorem mano_2sg : manoForm ⟨.second, .sg, none⟩ = .mascForm := rfl -theorem mano_1pl : manoForm ⟨.first, .pl, none⟩ = .mascForm := rfl -theorem mano_2pl : manoForm ⟨.second, .pl, none⟩ = .mascForm := rfl -theorem mano_3m_sg : manoForm ⟨.third, .sg, some .masc⟩ = .mascForm := rfl -theorem mano_3f_sg : manoForm ⟨.third, .sg, some .fem⟩ = .femForm := rfl -theorem mano_3pl : manoForm ⟨.third, .pl, none⟩ = .femForm := rfl +theorem mano_1sg : manoForm ⟨.first, .Sing, none⟩ = .mascForm := rfl +theorem mano_2sg : manoForm ⟨.second, .Sing, none⟩ = .mascForm := rfl +theorem mano_1pl : manoForm ⟨.first, .Plur, none⟩ = .mascForm := rfl +theorem mano_2pl : manoForm ⟨.second, .Plur, none⟩ = .mascForm := rfl +theorem mano_3m_sg : manoForm ⟨.third, .Sing, some .masc⟩ = .mascForm := rfl +theorem mano_3f_sg : manoForm ⟨.third, .Sing, some .fem⟩ = .femForm := rfl +theorem mano_3pl : manoForm ⟨.third, .Plur, none⟩ = .femForm := rfl /-- 3.M.PL: [MASC] is deleted by impoverishment in context of [PL], and 3rd person is not [PARTICIPANT], so no MARKED feature remains. -/ -theorem mano_3m_pl : manoForm ⟨.third, .pl, some .masc⟩ = .femForm := rfl +theorem mano_3m_pl : manoForm ⟨.third, .Plur, some .masc⟩ = .femForm := rfl /-- 3.F.PL: no [MASC], 3rd person not [PARTICIPANT] → elsewhere. -/ -theorem mano_3f_pl : manoForm ⟨.third, .pl, some .fem⟩ = .femForm := rfl +theorem mano_3f_pl : manoForm ⟨.third, .Plur, some .fem⟩ = .femForm := rfl -- ============================================================================ -- § 3: Free vs Possessed Forms (Table 4; [dixon-2004] p. 312) diff --git a/Linglib/Fragments/Mayan/Kiche/Agreement.lean b/Linglib/Fragments/Mayan/Kiche/Agreement.lean index 41983d392..22d25a10c 100644 --- a/Linglib/Fragments/Mayan/Kiche/Agreement.lean +++ b/Linglib/Fragments/Mayan/Kiche/Agreement.lean @@ -3,6 +3,7 @@ import Linglib.Core.UniversalDependencies import Linglib.Features.Prominence import Linglib.Fragments.Mayan.Params import Linglib.Typology.Extraction +import Linglib.Features.Number /-! # K'iche' Agreement Fragment [mondloch-2017] @@ -70,6 +71,8 @@ formal. The formal forms (laal SG, alaq PL) are syntactically postverbal and do not participate in the prefix paradigm. -/ +open Features (Number) + namespace Kiche -- ============================================================================ diff --git a/Linglib/Fragments/Spanish/Clitics.lean b/Linglib/Fragments/Spanish/Clitics.lean index b6ca409c4..f144226af 100644 --- a/Linglib/Fragments/Spanish/Clitics.lean +++ b/Linglib/Fragments/Spanish/Clitics.lean @@ -1,4 +1,6 @@ import Linglib.Core.UniversalDependencies +import Linglib.Features.Number +import Linglib.Features.Person /-! # Spanish Clitic Paradigm @@ -21,6 +23,8 @@ This syncretism drives the availability of stylistic applicatives. -/ +open Features (Number Person) + namespace Spanish.Clitics -- ============================================================================ diff --git a/Linglib/Semantics/Presupposition/PhiFeatures.lean b/Linglib/Semantics/Presupposition/PhiFeatures.lean index ceef22179..dd82ee200 100644 --- a/Linglib/Semantics/Presupposition/PhiFeatures.lean +++ b/Linglib/Semantics/Presupposition/PhiFeatures.lean @@ -232,11 +232,11 @@ theorem person_nesting_from_phi (speaker addressee : E) so `phiPresup_nesting` applies to both: the nesting is structural, not a per-domain coincidence. -/ theorem person_number_isomorphism : - PhiFeatures.specLevel Features.Person.first = + PhiFeatures.specLevel Features.Person.firstF = PhiFeatures.specLevel Features.Number.singularF ∧ - PhiFeatures.specLevel Features.Person.second = + PhiFeatures.specLevel Features.Person.secondF = PhiFeatures.specLevel Features.Number.dualF ∧ - PhiFeatures.specLevel Features.Person.third = + PhiFeatures.specLevel Features.Person.thirdF = PhiFeatures.specLevel Features.Number.pluralF := ⟨rfl, rfl, rfl⟩ @@ -338,13 +338,13 @@ theorem gender_nesting_from_phi (isInanimate isFemale : E → Prop) all three domains share the phi kernel structure. -/ theorem gender_person_number_isomorphism : PhiFeatures.specLevel Features.Gender.neuterF = - PhiFeatures.specLevel Features.Person.first ∧ + PhiFeatures.specLevel Features.Person.firstF ∧ PhiFeatures.specLevel Features.Gender.neuterF = PhiFeatures.specLevel Features.Number.singularF ∧ PhiFeatures.specLevel Features.Gender.feminineF = - PhiFeatures.specLevel Features.Person.second ∧ + PhiFeatures.specLevel Features.Person.secondF ∧ PhiFeatures.specLevel Features.Gender.masculineF = - PhiFeatures.specLevel Features.Person.third := + PhiFeatures.specLevel Features.Person.thirdF := ⟨rfl, rfl, rfl, rfl⟩ end GenderPresuppositions diff --git a/Linglib/Semantics/Quantification/Lexicon.lean b/Linglib/Semantics/Quantification/Lexicon.lean index 3cb598a17..e98db830f 100644 --- a/Linglib/Semantics/Quantification/Lexicon.lean +++ b/Linglib/Semantics/Quantification/Lexicon.lean @@ -1,4 +1,5 @@ import Linglib.Core.UniversalDependencies +import Linglib.Features.Number /-! # Quantifier lexicon — shared structure @@ -23,6 +24,8 @@ in the study files that commit to specific values. weak determiners pass `there is/are`) -/ +open Features (Number) + set_option autoImplicit false namespace Semantics.Quantification.Lexicon diff --git a/Linglib/Studies/Adamson2024.lean b/Linglib/Studies/Adamson2024.lean index e26c6b180..13b3863ee 100644 --- a/Linglib/Studies/Adamson2024.lean +++ b/Linglib/Studies/Adamson2024.lean @@ -519,11 +519,11 @@ def jarawaraPFDerive (poss : Jarawara.Possessor) : Jarawara.PossessedForm := Jarawara.manoForm poss -- PF pipeline: 1SG possessor → [PARTICIPANT] is MARKED → mano -theorem jarawara_pf_1sg : jarawaraPFDerive ⟨.first, .sg, none⟩ = .mascForm := rfl +theorem jarawara_pf_1sg : jarawaraPFDerive ⟨.first, .Sing, none⟩ = .mascForm := rfl -- PF pipeline: 3.M.SG → [MASC] survives → mano -theorem jarawara_pf_3msg : jarawaraPFDerive ⟨.third, .sg, some .masc⟩ = .mascForm := rfl +theorem jarawara_pf_3msg : jarawaraPFDerive ⟨.third, .Sing, some .masc⟩ = .mascForm := rfl -- PF pipeline: 3.M.PL → [MASC] impoverished by [PL] → mani -theorem jarawara_pf_3mpl : jarawaraPFDerive ⟨.third, .pl, some .masc⟩ = .femForm := rfl +theorem jarawara_pf_3mpl : jarawaraPFDerive ⟨.third, .Plur, some .masc⟩ = .femForm := rfl /-- Jarawara iPossessable n has {D} → relational semantic type. The n head licenses an iPossessor AND yields relational (π) semantics. -/ diff --git a/Linglib/Studies/ElkinsTorrenceBrown2026.lean b/Linglib/Studies/ElkinsTorrenceBrown2026.lean index 7b33fb127..072f52d32 100644 --- a/Linglib/Studies/ElkinsTorrenceBrown2026.lean +++ b/Linglib/Studies/ElkinsTorrenceBrown2026.lean @@ -521,7 +521,7 @@ theorem both_probes_unvalued : theorem phi_and_oblique_agree_parallel : -- φ-Agree pipeline: value person, then number, then spellout (applyAgree voiceProbe dp3sg (.phi (.person .third))).bind - (λ fb => applyAgree fb dp3sg (.phi (.number .sg))) = some voiceFullyAgreed ∧ + (λ fb => applyAgree fb dp3sg (.phi (.number .Sing))) = some voiceFullyAgreed ∧ spellout setAVocab voiceFullyAgreed (some .v) = some "t-" ∧ -- Oblique-Agree pipeline: value oblique, then spellout applyAgree voiceOblProbe [.valued (.oblique true)] (.oblique false) = diff --git a/Linglib/Studies/Harbour2016.lean b/Linglib/Studies/Harbour2016.lean index ef4952297..91a5b6754 100644 --- a/Linglib/Studies/Harbour2016.lean +++ b/Linglib/Studies/Harbour2016.lean @@ -244,8 +244,8 @@ theorem person_hierarchy_is_spec_ordering : PhiFeatures.specLevel Features.Person.secondF ∧ PhiFeatures.specLevel Features.Person.secondF > PhiFeatures.specLevel Features.Person.thirdF := - PhiFeatures.specLevel_strict_order Features.Person.first_is_maximal - Features.Person.second_is_intermediate Features.Person.third_is_minimal + PhiFeatures.specLevel_strict_order Features.Person.firstF_is_maximal + Features.Person.secondF_is_intermediate Features.Person.thirdF_is_minimal /-- The number hierarchy `sg > du > pl` is the *same* specification ordering — the structural reflection of the phi kernel, not an identification of the categories. -/ diff --git a/Linglib/Studies/Preminger2014.lean b/Linglib/Studies/Preminger2014.lean index 5c28f67aa..cf9758d2c 100644 --- a/Linglib/Studies/Preminger2014.lean +++ b/Linglib/Studies/Preminger2014.lean @@ -133,7 +133,7 @@ instance : DecidablePred IsAuthor := fun c => /-- Convert a person-number cell to a PhiFeature list for the Agree infrastructure. -/ def toPhiFeatures (c : Agreement.Cell) : List PhiFeature := - [.person c.toPersonLevel, .number (if c.isPlural then .pl else .sg)] + [.person c.toPersonLevel, .number (if c.isPlural then .Plur else .Sing)] -- ============================================================================ -- § 2: DM Vocabulary Insertion ([halle-marantz-1993]) diff --git a/Linglib/Studies/Scott2023Agreement.lean b/Linglib/Studies/Scott2023Agreement.lean index b0d10b10c..a4baa39d9 100644 --- a/Linglib/Studies/Scott2023Agreement.lean +++ b/Linglib/Studies/Scott2023Agreement.lean @@ -71,7 +71,7 @@ open Agreement /-- PhiFeature list per Mam person-number cell. -/ def mamToPhiFeatures (c : Agreement.Cell) : List PhiFeature := - [.person c.toPersonLevel, .number (if c.isPlural then .pl else .sg)] + [.person c.toPersonLevel, .number (if c.isPlural then .Plur else .Sing)] /-- Set A (ERG) vocabulary entries: φ-features on Voice (.v) yield the morphological exponent ([scott-2023] Table 2.8). @@ -104,16 +104,16 @@ def agreeProbe : ArgPosition → Option Cat -- ============================================================================ /-- Voice's probe features: [uPerson, uNumber]. - Placeholder values (.third, .sg) are irrelevant — `sameType` matching + Placeholder values (.third, .Sing) are irrelevant — `sameType` matching ensures any Person/Number goal is found regardless. -/ def voiceProbe : FeatureBundle := - [.unvalued (.phi (.person .third)), .unvalued (.phi (.number .sg))] + [.unvalued (.phi (.person .third)), .unvalued (.phi (.number .Sing))] /-- Infl's probe features: [uPerson, uNumber]. In intransitives, these are valued by S. In transitives, the probe is blocked by Voice_TR before reaching any DP. -/ def inflProbe : FeatureBundle := - [.unvalued (.phi (.person .third)), .unvalued (.phi (.number .sg))] + [.unvalued (.phi (.person .third)), .unvalued (.phi (.number .Sing))] -- ============================================================================ -- § 2: Goal Feature Bundles (3SG test case) @@ -121,7 +121,7 @@ def inflProbe : FeatureBundle := /-- A 3SG DP's features: [Person:3, Number:sg]. -/ def dp3sg : FeatureBundle := - [.valued (.phi (.person .third)), .valued (.phi (.number .sg))] + [.valued (.phi (.person .third)), .valued (.phi (.number .Sing))] -- ============================================================================ -- § 3: Agree Valuation — Voice agrees with agent @@ -130,25 +130,25 @@ def dp3sg : FeatureBundle := /-- Voice's [uPerson] is valued as [Person:3] from a 3SG agent. -/ theorem voice_agrees_person : applyAgree voiceProbe dp3sg (.phi (.person .third)) = - some [.valued (.phi (.person .third)), .unvalued (.phi (.number .sg))] := by + some [.valued (.phi (.person .third)), .unvalued (.phi (.number .Sing))] := by native_decide /-- After person agreement, Voice's [uNumber] is valued as [Number:sg]. This is the second step of φ-Agree: person first, then number. -/ theorem voice_agrees_number : - let afterPerson := [.valued (.phi (.person .third)), .unvalued (.phi (.number .sg))] - applyAgree afterPerson dp3sg (.phi (.number .sg)) = - some [.valued (.phi (.person .third)), .valued (.phi (.number .sg))] := by + let afterPerson := [.valued (.phi (.person .third)), .unvalued (.phi (.number .Sing))] + applyAgree afterPerson dp3sg (.phi (.number .Sing)) = + some [.valued (.phi (.person .third)), .valued (.phi (.number .Sing))] := by native_decide /-- Full φ-valuation of Voice by a 3SG agent: both person and number valued. -/ def voiceFullyAgreed : FeatureBundle := - [.valued (.phi (.person .third)), .valued (.phi (.number .sg))] + [.valued (.phi (.person .third)), .valued (.phi (.number .Sing))] /-- The two-step Agree pipeline produces a fully valued bundle. -/ theorem voice_agree_pipeline : (applyAgree voiceProbe dp3sg (.phi (.person .third))).bind - (λ fb => applyAgree fb dp3sg (.phi (.number .sg))) = + (λ fb => applyAgree fb dp3sg (.phi (.number .Sing))) = some voiceFullyAgreed := by native_decide @@ -164,7 +164,7 @@ theorem setA_spellout_3sg : /-- Set A spellout for 1SG: Voice with [Person:1, Number:sg] yields A1SG marker. -/ theorem setA_spellout_1sg : let v1sg : FeatureBundle := - [.valued (.phi (.person .first)), .valued (.phi (.number .sg))] + [.valued (.phi (.person .first)), .valued (.phi (.number .Sing))] spellout setAVocab v1sg (some .v) = some "n-/w-" := by native_decide @@ -178,7 +178,7 @@ theorem setA_spellout_1sg : entry is selected: "tz'=". -/ theorem setB_intransitive_3sg : let inflAgreed : FeatureBundle := - [.valued (.phi (.person .third)), .valued (.phi (.number .sg))] + [.valued (.phi (.person .third)), .valued (.phi (.number .Sing))] spellout setBVocab inflAgreed (some .T) = some "tz'=" := by native_decide @@ -199,7 +199,7 @@ theorem setB_transitive_default : vs. probe failure). -/ theorem setB_same_surface : let inflAgreed3sg : FeatureBundle := - [.valued (.phi (.person .third)), .valued (.phi (.number .sg))] + [.valued (.phi (.person .third)), .valued (.phi (.number .Sing))] let inflBlocked : FeatureBundle := [] spellout setBVocab inflAgreed3sg (some .T) = spellout setBVocab inflBlocked (some .T) := by @@ -210,7 +210,7 @@ theorem setB_same_surface : agreement, producing a distinct exponent. -/ theorem setB_intransitive_1sg : let t1sg : FeatureBundle := - [.valued (.phi (.person .first)), .valued (.phi (.number .sg))] + [.valued (.phi (.person .first)), .valued (.phi (.number .Sing))] spellout setBVocab t1sg (some .T) = some "chin" := by native_decide @@ -223,7 +223,7 @@ theorem setB_transitive_ignores_object : spellout setBVocab inflBlocked (some .T) = some "tz'=" ∧ -- Compare: a 1SG intransitive S would trigger "chin" let inflAgreed1sg : FeatureBundle := - [.valued (.phi (.person .first)), .valued (.phi (.number .sg))] + [.valued (.phi (.person .first)), .valued (.phi (.number .Sing))] spellout setBVocab inflAgreed1sg (some .T) = some "chin" := by exact ⟨by native_decide, by native_decide⟩ @@ -248,7 +248,7 @@ theorem probe_restriction_yields_default : spellout setBVocab ([] : FeatureBundle) (some .T) = some "tz'=" ∧ -- Intransitive 1SG: probe succeeds → "chin" (not default) spellout setBVocab - [.valued (.phi (.person .first)), .valued (.phi (.number .sg))] + [.valued (.phi (.person .first)), .valued (.phi (.number .Sing))] (some .T) = some "chin" := by exact ⟨by native_decide, by native_decide⟩ @@ -262,15 +262,15 @@ theorem probe_restriction_yields_default : theorem intransitive_pipeline_1sg : -- Infl Agrees with 1SG S (applyAgree inflProbe - [.valued (.phi (.person .first)), .valued (.phi (.number .sg))] + [.valued (.phi (.person .first)), .valued (.phi (.number .Sing))] (.phi (.person .third))).bind (λ fb => applyAgree fb - [.valued (.phi (.person .first)), .valued (.phi (.number .sg))] - (.phi (.number .sg))) = - some [.valued (.phi (.person .first)), .valued (.phi (.number .sg))] ∧ + [.valued (.phi (.person .first)), .valued (.phi (.number .Sing))] + (.phi (.number .Sing))) = + some [.valued (.phi (.person .first)), .valued (.phi (.number .Sing))] ∧ -- Spells out as "chin" (not default "tz'=") spellout setBVocab - [.valued (.phi (.person .first)), .valued (.phi (.number .sg))] + [.valued (.phi (.person .first)), .valued (.phi (.number .Sing))] (some .T) = some "chin" := by exact ⟨by native_decide, by native_decide⟩ @@ -288,7 +288,7 @@ theorem intransitive_pipeline_1sg : theorem full_pipeline_3sg_transitive : -- Step 1-2: Voice Agrees and spells out as Set A (applyAgree voiceProbe dp3sg (.phi (.person .third))).bind - (λ fb => applyAgree fb dp3sg (.phi (.number .sg))) = some voiceFullyAgreed ∧ + (λ fb => applyAgree fb dp3sg (.phi (.number .Sing))) = some voiceFullyAgreed ∧ spellout setAVocab voiceFullyAgreed (some .v) = some "t-" ∧ -- Step 3-4: Infl probe blocked → default Set B spellout setBVocab ([] : FeatureBundle) (some .T) = some "tz'=" ∧ @@ -378,7 +378,7 @@ theorem transitive_is_probe_failure : its φ-features. `attemptAgree` maps the `some _` result to `.valued`. -/ theorem intransitive_is_real_agreement : attemptAgree inflProbe - [.valued (.phi (.person .first)), .valued (.phi (.number .sg))] + [.valued (.phi (.person .first)), .valued (.phi (.number .Sing))] (.phi (.person .third)) = .valued := by native_decide @@ -416,7 +416,7 @@ theorem satisfaction_derives_patient_no_agree : /-- In an intransitive clause, `mamInflSatisfaction` is satisfied by φ-features and DOES copy them — matching `IsPhiAgreed .S`. -/ theorem satisfaction_derives_intranS_agree : - let dp1sg := [.valued (.phi (.person .first)), .valued (.phi (.number .sg))] + let dp1sg := [.valued (.phi (.person .first)), .valued (.phi (.number .Sing))] mamInflSatisfaction.isSatisfied dp1sg none = true ∧ mamInflSatisfaction.copiedFeatures dp1sg none = true ∧ ArgPosition.IsPhiAgreed .S := @@ -430,7 +430,7 @@ theorem satisfaction_matches_fragment : (mamInflSatisfaction.copiedFeatures [] (some .v) = true ↔ ArgPosition.IsPhiAgreed .P) ∧ (mamInflSatisfaction.copiedFeatures - [.valued (.phi (.person .first)), .valued (.phi (.number .sg))] + [.valued (.phi (.person .first)), .valued (.phi (.number .Sing))] none = true ↔ ArgPosition.IsPhiAgreed .S) := by refine ⟨?_, ?_⟩ @@ -476,7 +476,7 @@ def mamImpoverishmentRule : Morphology.DM.Impoverishment.ImpoverishmentRule := (λ fb => fb.any (λ f => match f with | .valued (.phi (.person .first)) => true | _ => false)) - (.phi (.number .sg)) + (.phi (.number .Sing)) /-- Mam's rule is paradigmatic — discharged by the smart constructor. -/ theorem mamImpoverishment_paradigmatic : @@ -487,29 +487,29 @@ theorem mamImpoverishment_paradigmatic : theorem impoverishment_fires_1sg : mamImpoverishmentRule.condition (Morphology.DM.Impoverishment.Neighborhood.ofBundle - [.valued (.phi (.person .first)), .valued (.phi (.number .sg))]) := by + [.valued (.phi (.person .first)), .valued (.phi (.number .Sing))]) := by decide /-- The impoverishment rule does NOT fire for 3rd person bundles. -/ theorem impoverishment_blocked_3sg : ¬ mamImpoverishmentRule.condition (Morphology.DM.Impoverishment.Neighborhood.ofBundle - [.valued (.phi (.person .third)), .valued (.phi (.number .sg))]) := by + [.valued (.phi (.person .third)), .valued (.phi (.number .Sing))]) := by decide /-- After impoverishment, the number feature is deleted from 1st person bundles, bleeding insertion of the base morpheme *qin*. -/ theorem impoverishment_deletes_number : mamImpoverishmentRule.applyToBundle - [.valued (.phi (.person .first)), .valued (.phi (.number .sg))] = + [.valued (.phi (.person .first)), .valued (.phi (.number .Sing))] = [.valued (.phi (.person .first))] := by decide /-- Without impoverishment (3rd person), the number feature survives. -/ theorem no_impoverishment_preserves : mamImpoverishmentRule.applyToBundle - [.valued (.phi (.person .third)), .valued (.phi (.number .sg))] = - [.valued (.phi (.person .third)), .valued (.phi (.number .sg))] := by + [.valued (.phi (.person .third)), .valued (.phi (.number .Sing))] = + [.valued (.phi (.person .third)), .valued (.phi (.number .Sing))] := by decide end Scott2023 diff --git a/Linglib/Syntax/Minimalist/SpeechActs.lean b/Linglib/Syntax/Minimalist/SpeechActs.lean index 8ad87d2af..7ac177e07 100644 --- a/Linglib/Syntax/Minimalist/SpeechActs.lean +++ b/Linglib/Syntax/Minimalist/SpeechActs.lean @@ -8,6 +8,8 @@ import Linglib.Discourse.Intentionality import Linglib.Discourse.Commitment.Basic import Linglib.Features.Evidentiality import Linglib.Fragments.English.Pronouns +import Linglib.Features.Number +import Linglib.Features.Person /-! # Configurational Point-of-View Roles @@ -35,6 +37,8 @@ c-commands content. -/ +open Features (Number Person) + namespace Minimalist.SpeechActs open Minimalist