diff --git a/Linglib.lean b/Linglib.lean index 2088303dd..78a13aae7 100644 --- a/Linglib.lean +++ b/Linglib.lean @@ -1152,6 +1152,7 @@ import Linglib.Studies.Marantz1991 import Linglib.Studies.Pesetsky2013 import Linglib.Studies.BakerVinokurova2010 import Linglib.Studies.Comrie1989 +import Linglib.Studies.Cinque2020 import Linglib.Typology.ClauseChaining import Linglib.Studies.SarvasyAikhenvald2025 import Linglib.Studies.Partee1987 @@ -2181,7 +2182,6 @@ import Linglib.Syntax.Minimalist.Modification import Linglib.Syntax.Minimalist.Scope import Linglib.Syntax.Minimalist.TraceInterpretation import Linglib.Syntax.Minimalist.CombinationSchemata -import Linglib.Syntax.Minimalist.RelativeClauses import Linglib.Syntax.Minimalist.Basic import Linglib.Syntax.Minimalist.Derivation import Linglib.Syntax.Minimalist.HeadFunction diff --git a/Linglib/Studies/Cinque2020.lean b/Linglib/Studies/Cinque2020.lean new file mode 100644 index 000000000..8345d659f --- /dev/null +++ b/Linglib/Studies/Cinque2020.lean @@ -0,0 +1,287 @@ +import Linglib.Typology.RelativeClause.Basic + +/-! +# Cinque (2020): a unified double-Headed analysis of relative clauses +@cite{cinque-2020} + +Formalizes the core of @cite{cinque-2020}: all attested relative-clause types +derive from a single **double-Headed** structure — an *internal* Head and an +*external* Head (both indefinite `dP`s, smaller than DP), with the relative +clause merged pre-nominally — via two derivation routes (§1.5): + +* **Raising** — the *internal* Head raises to Spec,CP and is the overt Head, + licensing deletion of the external Head (@cite{kayne-1994} ch. 8). + Reconstruction / island effects are detectable: the overt Head is in a chain + with the RC-internal position. +* **Matching** — the *external* Head raises and is overt, licensing deletion of + the internal Head. Reconstruction is not detectable. + +Deletion of the internal Head is licit only when it exactly matches the external +Head (both indefinite `dP`); when the relativized internal Head is bigger — a +DP/KP, or a DP/KP inside a PP (an oblique) — no deletion is possible and the +internal Head is realized by a *wh*-pronoun or a resumptive (§1.5). + +The different RC types merge at different heights of the nominal extended +projection (§3.5): non-restrictives attach above DP (external Head includes +strong determiners), restrictives lower (external Head = weak determiners only), +participials lower still. The internal-Head realization "strategies" (ch. 4) +are gap + invariant relativizer, gap + relative pronoun, resumptive, PRO, +non-reduction, and verb-coding. + +This is the genuine syntactic treatment that **computes** a +`RelativeClause.Realization` from the reified derivation — the consumer the +substrate's projection hook was built for, and the honest counterpart to the +HPSG `RelClauseDerivation.realization` (which `RelativeClause.Realization` +already serves). @cite{de-vries-2018} surveys the framework-neutral typology +this single structure is meant to cover. + +## Main declarations +* `Cinque2020.RC` — the reified double-Headed relative clause. +* `Cinque2020.RC.realization` — its computed projection onto + `RelativeClause.Realization`. +* `Cinque2020.RC.WellFormed` — the deletion-licensing condition. + +## Implementation notes +The reification stays at the level §1.5 states explicitly (two Heads, derivation +route, internal-Head category and strategy, merge height); the tree geometry +(Spec,CP, the `dP`/DP cartography) is below this level and not modelled. PRO and +the verb-coding strategy have no exact `RelativeClause.NPRelType` counterpart in +the Keenan-Comrie/WALS inventory the substrate was built from and are +approximated when projecting. +-/ + +namespace Cinque2020 + +open RelativeClause + +/-! ### The two derivations from the single double-Headed structure -/ + +/-- The derivation route (@cite{cinque-2020} §1.5). -/ +inductive Derivation + /-- The internal Head raises to Spec,CP and is overt; the external Head is + deleted (@cite{kayne-1994}). -/ + | raising + /-- The external Head is overt; the internal Head is deleted / a proform. -/ + | matching + deriving DecidableEq, Repr + +/-- Which of the two Heads surfaces overtly. -/ +inductive HeadChoice + | internal + | external + deriving DecidableEq, Repr + +/-- The overt Head is fixed by the derivation, not stipulated separately. -/ +def Derivation.overtHead : Derivation → HeadChoice + | .raising => .internal + | .matching => .external + +/-! ### The internal Head and its realization strategy -/ + +/-- Category of the relativized internal Head (@cite{cinque-2020} §1.5). + Deletion under identity with the external Head turns on this: only an + indefinite `dP` exactly matches the (indefinite `dP`) external Head. -/ +inductive InternalHeadCategory + /-- An indefinite `dP` exactly matching the external Head — deletion licit. -/ + | indefiniteDP + /-- A DP/KP, or a DP/KP inside a PP (oblique) — bigger than `dP`, no deletion. -/ + | biggerDPKP + deriving DecidableEq, Repr + +/-- Strategies for realizing the internal Head (@cite{cinque-2020} ch. 4). -/ +inductive Strategy + /-- Gap + invariant relativizer (English *that*, Italian *che*). -/ + | invariantRelativizer + /-- Gap + relative pronoun / adjective (*who*/*which*, Italian *cui*). -/ + | relativePronoun + /-- Resumptive pronoun / epithet. -/ + | resumptive + /-- PRO (participial relative clauses). -/ + | pro + /-- Full repetition of the Head (non-reduction). -/ + | nonReduction + /-- The verb-coding strategy. -/ + | verbCoding + deriving DecidableEq, Repr + +/-- Does this strategy realize the internal Head by *deleting* it under identity + with the external Head (the gap + invariant-relativizer case)? Only the + invariant-relativizer strategy does. PRO is a null *proform*, not deletion: + @cite{cinque-2020} keeps deletion / non-pronunciation distinct from + proform-replacement, so PRO is not subject to the exact-match licensing. -/ +def Strategy.DeletesInternalHead (s : Strategy) : Prop := s = .invariantRelativizer + +instance (s : Strategy) : Decidable s.DeletesInternalHead := by + unfold Strategy.DeletesInternalHead; infer_instance + +/-- Project a Cinque strategy onto the substrate `NPRelType`. PRO and + verb-coding have no exact counterpart in the substrate inventory and are + approximated (PRO ≈ a silent gap; verb-coding ≈ non-reduction). -/ +def Strategy.toNPRelType : Strategy → NPRelType + | .invariantRelativizer => .gap + | .relativePronoun => .relPronoun + | .resumptive => .resumptive + | .pro => .gap + | .nonReduction => .nonReduction + | .verbCoding => .nonReduction + +/-! ### Relative-clause types and merge height -/ + +/-- RC types, by increasing height of external merge in the nominal extended + projection (@cite{cinque-2020} §3.5): a bigger external Head merges higher. -/ +inductive RCType + | participial + | restrictive + | maximalizing + | kindDefining + | nonRestrictive + deriving DecidableEq, Repr + +/-- Relative merge height (bigger external Head = higher), per @cite{cinque-2020} + §3.5: participials lowest (smallest external Head); amount/maximalizing below + ordinary restrictives (§3.5.5, presented as a tentative refinement of the + §1.5 simplification that they merge alike); kind-defining between restrictives + and non-restrictives (§3.5.3); non-restrictives highest (above DP). -/ +def RCType.mergeHeight : RCType → Nat + | .participial => 0 + | .maximalizing => 1 + | .restrictive => 2 + | .kindDefining => 3 + | .nonRestrictive => 4 + +/-! ### The reified relative clause -/ + +/-- A relative clause in @cite{cinque-2020}'s unified analysis: the single + double-Headed structure (both Heads present by construction), a derivation + route, the internal-Head category and realization strategy, the relativized + AH position, and the position of the RC w.r.t. the Head. -/ +structure RC where + rcType : RCType + derivation : Derivation + internalHeadCategory : InternalHeadCategory + strategy : Strategy + position : AHPosition + rcPosition : RCPosition + deriving Repr + +/-- The overt Head of an RC, determined by its derivation. -/ +def RC.overtHead (r : RC) : HeadChoice := r.derivation.overtHead + +/-- Reconstruction / island effects are detectable iff the overt Head is the + *internal* one (raising) — it is then in a chain with the RC-internal + position (@cite{cinque-2020} §1.5). -/ +def RC.Reconstructs (r : RC) : Prop := r.derivation = .raising + +instance (r : RC) : Decidable r.Reconstructs := by + unfold RC.Reconstructs; infer_instance + +/-- @cite{cinque-2020}'s deletion-licensing condition: the internal Head may be + deleted (the gap + invariant-relativizer strategy) only when it exactly + matches the external Head (an indefinite `dP`). A bigger internal Head + (oblique DP/KP, or DP/KP in a PP) must be spelled out — a relative pronoun + or a resumptive. -/ +def RC.WellFormed (r : RC) : Prop := + r.strategy.DeletesInternalHead → r.internalHeadCategory = .indefiniteDP + +instance (r : RC) : Decidable r.WellFormed := by + unfold RC.WellFormed; infer_instance + +/-- The framework-neutral `RelativeClause.Realization` this derivation projects + to — **computed** from the reified structure (the relativized position and + the NP_rel type the internal-Head strategy yields), not stipulated. The hook + by which Cinque's analysis connects to the relativization substrate. -/ +def RC.realization (r : RC) : Realization := + { position := r.position, npRel := r.strategy.toNPRelType } + +/-! ### Consequences -/ + +/-- A matching derivation shows no reconstruction (@cite{cinque-2020} §1.5). -/ +theorem matching_not_reconstructs (r : RC) (h : r.derivation = .matching) : + ¬ r.Reconstructs := by + unfold RC.Reconstructs; rw [h]; decide + +/-- **Deletion licensing.** A well-formed RC whose relativized internal Head is + bigger than an indefinite `dP` cannot use the gap-deletion (invariant + relativizer) strategy — it must spell the internal Head out. -/ +theorem bigger_head_no_gap_deletion (r : RC) (h : r.WellFormed) + (hbig : r.internalHeadCategory = .biggerDPKP) : + r.strategy ≠ .invariantRelativizer := by + intro hs + have hd : r.strategy.DeletesInternalHead := hs + have hmatch : r.internalHeadCategory = .indefiniteDP := h hd + rw [hbig] at hmatch + exact absurd hmatch (by decide) + +/-- Non-restrictive RCs merge higher than restrictives (@cite{cinque-2020} §3.5). -/ +theorem nonRestrictive_above_restrictive : + RCType.restrictive.mergeHeight < RCType.nonRestrictive.mergeHeight := by decide + +/-- Participial RCs have the lowest external merge. -/ +theorem participial_lowest (t : RCType) : + RCType.participial.mergeHeight ≤ t.mergeHeight := by + cases t <;> decide + +/-- Amount/maximalizing RCs merge lower (closer to the Head) than ordinary + restrictives — @cite{cinque-2020} §3.5.5, presented there as a tentative + refinement of the §1.5 simplification that they merge in the same position. -/ +theorem maximalizing_below_restrictive : + RCType.maximalizing.mergeHeight < RCType.restrictive.mergeHeight := by decide + +/-! ### Worked examples -/ + +/-- English "the book that John read ___": matching, internal Head exactly + matches the external (indefinite `dP`), gap via the invariant relativizer + *that*; object relative. -/ +def englishThatObject : RC := + { rcType := .restrictive, derivation := .matching, + internalHeadCategory := .indefiniteDP, strategy := .invariantRelativizer, + position := .directObject, rcPosition := .postNominal } + +example : englishThatObject.WellFormed := by decide + +/-- It **computes** to the substrate realization `(directObject, gap)` — the same + value HPSG's `RelClauseDerivation.realization` computes for this sentence, + now from Cinque's derivation rather than stipulated. -/ +theorem englishThatObject_realization : + englishThatObject.realization = { position := .directObject, npRel := .gap } := rfl + +/-- "the man to whom I spoke": oblique relativization. The internal Head is + bigger than `dP` (a PP-internal DP/KP), so deletion is barred and a relative + pronoun is used. -/ +def englishWhomOblique : RC := + { rcType := .restrictive, derivation := .matching, + internalHeadCategory := .biggerDPKP, strategy := .relativePronoun, + position := .oblique, rcPosition := .postNominal } + +example : englishWhomOblique.WellFormed := by decide +example : + englishWhomOblique.realization = { position := .oblique, npRel := .relPronoun } := rfl + +/-- The deletion-licensing bite: an oblique (bigger) internal Head *cannot* be + deleted via the invariant relativizer — that derivation is ill-formed. -/ +theorem oblique_gap_deletion_illFormed : + ¬ ({ rcType := .restrictive, derivation := .matching, + internalHeadCategory := .biggerDPKP, strategy := .invariantRelativizer, + position := .oblique, rcPosition := .postNominal } : RC).WellFormed := by decide + +/-- Hebrew resumptive relativization at the genitive: matching, internal Head + spelled out as a resumptive pronoun. -/ +def hebrewResumptiveGenitive : RC := + { rcType := .restrictive, derivation := .matching, + internalHeadCategory := .biggerDPKP, strategy := .resumptive, + position := .genitive, rcPosition := .postNominal } + +example : + hebrewResumptiveGenitive.realization = { position := .genitive, npRel := .resumptive } := rfl + +/-- A raising derivation (overt Head = internal Head) shows reconstruction. -/ +def englishRaisingObject : RC := + { rcType := .restrictive, derivation := .raising, + internalHeadCategory := .indefiniteDP, strategy := .invariantRelativizer, + position := .directObject, rcPosition := .postNominal } + +example : englishRaisingObject.overtHead = .internal := rfl +example : englishRaisingObject.Reconstructs := by decide +example : ¬ englishThatObject.Reconstructs := by decide + +end Cinque2020 diff --git a/Linglib/Syntax/HPSG/Core/RelativeClauses.lean b/Linglib/Syntax/HPSG/Core/RelativeClauses.lean index d1bf1be98..c6c0e23aa 100644 --- a/Linglib/Syntax/HPSG/Core/RelativeClauses.lean +++ b/Linglib/Syntax/HPSG/Core/RelativeClauses.lean @@ -1,4 +1,5 @@ import Linglib.Syntax.HPSG.Core.HeadFiller +import Linglib.Typology.RelativeClause.Basic /-! # Relative Clauses in HPSG @@ -24,6 +25,16 @@ combine with a head noun via the Head-Modifier Schema. - `RelClauseDerivation` — end-to-end derivation of a relative clause - `relClauseModifies` — the Head-Modifier step +## Connection to the `RelativeClause` substrate + +This HPSG derivation projects to the framework-neutral descriptive profile in +`Typology/RelativeClause/Basic.lean`: `Relativizer.npRel` reads off the +`RelativeClause.NPRelType` (complementizer → gap, relative pronoun → +`relPronoun`), and `RelClauseDerivation.realization` exposes the +`RelativeClause.Realization` a derivation realizes. This is the shared +*descriptive* projection only — the GAP/MOD *mechanism* is HPSG-specific and is +not unified with other frameworks' derivations. + ## Connection to @cite{sag-wasow-bender-2003} Ch. 14 SWB2003 explicitly defers relative clause analysis ("beyond the scope @@ -35,6 +46,7 @@ mechanism from SWB2003 Ch. 14 combined with the MOD feature. namespace HPSG.RelativeClauses open HPSG +open RelativeClause (NPRelType AHPosition Realization) -- ============================================================================ -- Relativizers @@ -57,6 +69,14 @@ def relWho : Relativizer := { word := ⟨"who", .PRON, { wh := true }⟩ } def relWhich : Relativizer := { word := ⟨"which", .PRON, { wh := true }⟩ } def relWhom : Relativizer := { word := ⟨"whom", .PRON, { wh := true }⟩ } +/-- The `RelativeClause.NPRelType` this relativizer realizes: a `wh`-pronoun + (who/which/whom) is a relative pronoun; the complementizer "that"/∅ leaves + a gap. Projects the HPSG relativizer onto the framework-neutral substrate. -/ +def Relativizer.npRel (r : Relativizer) : NPRelType := + match r.word.cat with + | .PRON => .relPronoun + | _ => .gap + -- ============================================================================ -- Relative Clause Derivation -- ============================================================================ @@ -72,6 +92,9 @@ This models the two-step process: structure RelClauseDerivation where /-- The relativizer (who/which/that) -/ rel : Relativizer + /-- The relativized grammatical position (which AH slot the gap sits in: + subject relative, object relative, …). -/ + position : AHPosition /-- The gapped clause (e.g., "John read ___") -/ gappedClause : TrackedSign /-- The gap in the clause must be compatible with the relativizer -/ @@ -92,6 +115,13 @@ def RelClauseDerivation.result (d : RelClauseDerivation) : TrackedSign := def RelClauseDerivation.isMod (d : RelClauseDerivation) : Bool := d.result.sign.synsem.mod.isSome +/-- The framework-neutral `RelativeClause.Realization` this derivation projects + to: the relativized AH position paired with the NP_rel type. The shared hook + onto the substrate — comparable across frameworks, even though the GAP/MOD + derivation itself is HPSG-specific. -/ +def RelClauseDerivation.realization (d : RelClauseDerivation) : Realization := + { position := d.position, npRel := d.rel.npRel } + -- ============================================================================ -- Head-Modifier Combination -- ============================================================================ @@ -158,6 +188,7 @@ private def clause_tracked : TrackedSign := -- Step 3: Relativizer "that" discharges the gap private def relClause : RelClauseDerivation := { rel := relThat + position := .directObject gappedClause := clause_tracked gapCompatible := .inr (by decide) } @@ -165,6 +196,9 @@ private def relClause : RelClauseDerivation := #guard relClause.isMod #guard relClause.result.sign.synsem.mod == some .NOUN +/-- Object relative ("the book that John read ___") realizes a directObject gap. -/ +example : relClause.realization = { position := .directObject, npRel := .gap } := rfl + -- The gap is discharged (SLASH empty after relativizer fills it) -- Note: "that" is SCONJ, not compatible with NOUN gap via categoriesMatch, -- so discharge keeps the slash. For the relative clause, the gap is @@ -210,6 +244,7 @@ private def subj_gapped_clause : TrackedSign := -- "who" as relativizer with [MOD NP] private def who_relClause : RelClauseDerivation := { rel := relWho + position := .subject gappedClause := subj_gapped_clause gapCompatible := .inr (by decide) } @@ -224,6 +259,9 @@ private def modified_boy : Option Sign := #guard modified_boy.isSome +/-- Subject relative ("the boy who saw Mary") realizes a subject relative-pronoun. -/ +example : who_relClause.realization = { position := .subject, npRel := .relPronoun } := rfl + end SubjectRelative -- ============================================================================ diff --git a/Linglib/Syntax/Minimalist/RelativeClauses.lean b/Linglib/Syntax/Minimalist/RelativeClauses.lean deleted file mode 100644 index 95144de3e..000000000 --- a/Linglib/Syntax/Minimalist/RelativeClauses.lean +++ /dev/null @@ -1,310 +0,0 @@ -import Linglib.Syntax.Minimalist.TraceInterpretation -import Linglib.Syntax.Minimalist.Basic - -/-! -# Relative Clause Semantics: A Worked Example - -Demonstrates the full machinery from Syntax/Minimalist/TraceInterpretation.lean -with a concrete linguistic example: "the book that John read _" - -## The Derivation - -``` - DP - / \ - the NP - / \ - book CP - / \ - Op₁ IP - / \ - John VP - / \ - read t₁ -``` - -## Semantic Composition - -1. **Trace interpretation**: ⟦t₁⟧^g = g(1) -2. **VP composition**: ⟦read t₁⟧^g = read(g(1)) (applied to subject later) -3. **IP composition**: ⟦John read t₁⟧^g = read(j, g(1)) -4. **Predicate Abstraction at CP**: ⟦Op₁ [John read t₁]⟧^g = λx. read(j, x) -5. **Predicate Modification with head noun**: λx. book(x) ∧ read(j, x) -6. **Definite description**: ιx[book(x) ∧ read(j,x)] - --/ - -namespace Minimalist.RelativeClauses - -open Core.Logic.Intensional Core.Logic.Intensional.Variables Semantics.Composition.Modification -open Minimalist - --- ============================================================================ --- Example Model: Reading Scenario --- ============================================================================ - -/-- -A model for the "book that John read" example. - -Domain: john, mary, book1, book2, newspaper --/ -inductive ReadEntity where - | john - | mary - | book1 -- the book John read - | book2 -- a book John didn't read - | newspaper -- something that isn't a book - deriving Repr, DecidableEq, Inhabited - -/-- The model for our example -/ -def readModel : Frame := { - Entity := ReadEntity - Index := Unit -} - --- ============================================================================ --- Lexical Semantics --- ============================================================================ - -open ReadEntity - -/-- "John" denotes the entity john -/ -def john_sem : readModel.Denot .e := john - -/-- "Mary" denotes the entity mary -/ -def mary_sem : readModel.Denot .e := mary - -/-- "book" is true of book1 and book2 -/ -def book_sem : readModel.Denot (.e ⇒ .t) := - λ x => match x with - | .book1 => True - | .book2 => True - | _ => False - -/-- "read" as a relation: John read book1, Mary read book2 -/ -def read_sem : readModel.Denot (.e ⇒ .e ⇒ .t) := - λ obj => λ subj => match subj, obj with - | .john, .book1 => True -- John read book1 - | .mary, .book2 => True -- Mary read book2 - | .mary, .newspaper => True -- Mary also read the newspaper - | _, _ => False - -instance : DecidablePred book_sem := - λ x => match x with - | .book1 | .book2 => isTrue trivial - | .john | .mary | .newspaper => isFalse not_false - -instance : ∀ (obj : ReadEntity), DecidablePred (read_sem obj) - | .book1 => λ subj => match subj with - | .john => isTrue trivial - | .mary | .book1 | .book2 | .newspaper => isFalse not_false - | .book2 => λ subj => match subj with - | .mary => isTrue trivial - | .john | .book1 | .book2 | .newspaper => isFalse not_false - | .newspaper => λ subj => match subj with - | .mary => isTrue trivial - | .john | .book1 | .book2 | .newspaper => isFalse not_false - | .john | .mary => λ subj => match subj with - | .john | .mary | .book1 | .book2 | .newspaper => isFalse not_false - --- ============================================================================ --- Building the Relative Clause: "that John read _" --- ============================================================================ - -/-- -The trace in object position: t₁ - -This represents the gap in "that John read _". -The trace has index 1. --/ -def trace1 : DenotG readModel .e := interpTrace 1 - -/-- -VP meaning: "read t₁" - -⟦read t₁⟧^g = λy. read(g(1))(y) = λy. read(y, g(1)) - -Note: Our read_sem takes object first, then subject. -So "read t₁" is the function waiting for a subject. --/ -def vp_readTrace : DenotG readModel (.e ⇒ .t) := - λ g => λ subj => read_sem (trace1 g) subj - -/-- -IP meaning: "John read t₁" - -⟦John read t₁⟧^g = read(j, g(1)) --/ -def ip_johnReadTrace : DenotG readModel .t := - applyG vp_readTrace (constDenot john_sem) - -/-- -Verify IP meaning: it's true iff the trace's value was read by John --/ -theorem ip_meaning_correct (g : Core.Assignment readModel.Entity) : - ip_johnReadTrace g = read_sem (g 1) john := rfl - -/-- -CP meaning via Predicate Abstraction: "Op₁ [John read t₁]" - -⟦Op₁ [John read t₁]⟧^g = λx. ⟦John read t₁⟧^{g[1↦x]} - = λx. read(j, x) - -This creates a predicate "things that John read". --/ -def cp_relativeClause : DenotG readModel (.e ⇒ .t) := - predicateAbstraction 1 ip_johnReadTrace - -/-- -Verify CP meaning: λx. read(j, x) --/ -theorem cp_meaning_correct (g : Core.Assignment readModel.Entity) (x : ReadEntity) : - cp_relativeClause g x = read_sem x john := by - simp only [cp_relativeClause, predicateAbstraction, lambdaAbsG, - ip_johnReadTrace, applyG, vp_readTrace, constDenot, john_sem, - trace1, interpTrace, interpPronoun, update_same] - --- ============================================================================ --- Combining with Head Noun: "book that John read" --- ============================================================================ - -/-- Head noun "book" as assignment-relative (trivially constant) -/ -def book_denot : DenotG readModel (.e ⇒ .t) := constDenot book_sem - -/-- -NP meaning: "book that John read _" - -Via Predicate Modification: -⟦book [that John read _]⟧ = λx. book(x) ∧ read(j, x) --/ -def np_bookThatJohnRead : DenotG readModel (.e ⇒ .t) := - relativePM 1 book_denot ip_johnReadTrace - -/-- -The NP meaning is the intersection of "book" and "things John read" --/ -theorem np_meaning_correct (g : Core.Assignment readModel.Entity) (x : ReadEntity) : - np_bookThatJohnRead g x = (book_sem x ∧ read_sem x john) := by - simp only [np_bookThatJohnRead, relativePM, predicateModification, - book_denot, constDenot, predicateAbstraction, lambdaAbsG, - ip_johnReadTrace, applyG, vp_readTrace, trace1, john_sem, - interpTrace, interpPronoun, update_same] - --- ============================================================================ --- The Definite Description: "the book that John read" --- ============================================================================ - -/-- -The iota operator: ιx.P(x) - -Returns the unique x satisfying P, if one exists. -For computational simplicity, we search through a list of candidates. --/ -def iota (candidates : List ReadEntity) (p : ReadEntity → Bool) : Option ReadEntity := - match candidates.filter p with - | [x] => some x -- exactly one satisfying element - | _ => none -- zero or multiple: presupposition failure - -/-- All entities in our domain -/ -def allEntities : List ReadEntity := [.john, .mary, .book1, .book2, .newspaper] - -/-- -"the book that John read" denotes book1 - -This is the unique entity satisfying: - book(x) ∧ read(j, x) --/ -def the_book_that_john_read (_g : Core.Assignment readModel.Entity) : Option ReadEntity := - iota allEntities (λ x => decide (book_sem x ∧ read_sem x john)) - -/-- -Main theorem: "the book that John read" denotes book1 - -This shows the compositional derivation yields the correct result: -- book1 is a book -- John read book1 -- No other book was read by John -- Therefore ιx[book(x) ∧ read(j,x)] = book1 --/ -theorem the_book_correct (g : Core.Assignment readModel.Entity) : - the_book_that_john_read g = some ReadEntity.book1 := by - simp only [the_book_that_john_read] - decide - --- ============================================================================ --- Properties of the Derivation --- ============================================================================ - -/-- -The relative clause creates the right predicate: -it's true of exactly the things John read. --/ -theorem relClause_extension (g : Core.Assignment readModel.Entity) : - (cp_relativeClause g book1) ∧ - (¬ cp_relativeClause g book2) ∧ - (¬ cp_relativeClause g newspaper) := by - simp only [cp_meaning_correct, read_sem] - exact ⟨trivial, not_false_eq_true ▸ trivial, not_false_eq_true ▸ trivial⟩ - -/-- -The modified NP is true of exactly book1. --/ -theorem np_extension (g : Core.Assignment readModel.Entity) : - (np_bookThatJohnRead g book1) ∧ - (¬ np_bookThatJohnRead g book2) ∧ - (¬ np_bookThatJohnRead g john) := by - simp only [np_meaning_correct, book_sem, read_sem] - exact ⟨⟨trivial, trivial⟩, fun ⟨_, h⟩ => h, fun ⟨h, _⟩ => h⟩ - -/-- -Assignment independence: the final NP meaning doesn't depend on -the assignment (all variables are bound). --/ -theorem np_assignment_independent (g₁ g₂ : Core.Assignment readModel.Entity) : - np_bookThatJohnRead g₁ = np_bookThatJohnRead g₂ := by - funext x - simp only [np_meaning_correct] - --- ============================================================================ --- Alternative: Using relativePM Directly --- ============================================================================ - -/-- -An equivalent formulation using the relativePM combinator directly. -This shows the interface abstracts over the composition steps. --/ -def np_bookThatJohnRead' : DenotG readModel (.e ⇒ .t) := - relativePM 1 (constDenot book_sem) (applyG (λ g subj => read_sem (g 1) subj) (constDenot john)) - -/-- The two formulations are equivalent -/ -theorem np_formulations_equiv (g : Core.Assignment readModel.Entity) : - np_bookThatJohnRead g = np_bookThatJohnRead' g := by - funext x - simp only [np_bookThatJohnRead, np_bookThatJohnRead', relativePM, - predicateModification, book_denot, constDenot, john_sem, - predicateAbstraction, lambdaAbsG, ip_johnReadTrace, - applyG, vp_readTrace, trace1, interpTrace, interpPronoun, - update_same] - --- ============================================================================ --- Connection to Syntactic Structure --- ============================================================================ - -/-- -The syntactic structure with a trace. - -This shows how the semantic derivation corresponds to the syntax: -the trace created via `mkTrace 1` is interpreted via `interpTrace 1`. --/ -def traceExample : SyntacticObject := mkTrace 1 - -/-- -Extracting the trace index from a syntactic object. --/ -theorem trace_example_has_index : getTraceIndex traceExample = some 1 := by - show (Multiset.toList (Minimalist.traceIndices (mkTrace 1))).head? = some 1 - rw [show Minimalist.mkTrace 1 = SyntacticObject.trace 1 from rfl, - Minimalist.traceIndices_trace, Multiset.toList_singleton] - rfl - -end Minimalist.RelativeClauses diff --git a/Linglib/Typology/RelativeClause/Basic.lean b/Linglib/Typology/RelativeClause/Basic.lean index 1a3d13960..72ef5647a 100644 --- a/Linglib/Typology/RelativeClause/Basic.lean +++ b/Linglib/Typology/RelativeClause/Basic.lean @@ -21,6 +21,8 @@ Accessibility Hierarchy. Mirrors `Features.Case` for case inventories. to the head noun (post-nominal, pre-nominal, internally-headed, correlative). * `RelativeClause.NPRelType` — what occupies the relativized position (gap, resumptive, relative pronoun, …). +* `RelativeClause.Realization` — what one derivation realizes (AH position + + NP_rel type); the framework-neutral hook a syntactic account projects to. * `RelativeClause.Marker` — a relative-clause marker or construction, with the `Covers` / `IsContinuous` / `IsPrimary` predicates fragments and studies consume. @@ -179,6 +181,25 @@ def NPRelType.resumptiveKind : NPRelType → Option ResumptiveKind | .resumptive => some .unspecified | _ => none +/-! ### Realization -/ + +/-- What a single relative-clause derivation *realizes*, stated + framework-neutrally: the relativized @cite{keenan-comrie-1977} AH position + and the NP_rel type occupying it. + + This is the hook by which a syntactic framework's derivation connects to the + shared relativization substrate: HPSG's GAP/MOD derivation, Minimalism's + trace + predicate-abstraction, etc. each *project* to a `Realization`, even + though their derivation mechanisms are framework-specific and not unified. + Distinct from the per-language WALS `Profile` (a typological survey of a + language's strategies); a `Realization` describes one derivation. -/ +structure Realization where + /-- The relativized position on the Accessibility Hierarchy. -/ + position : AHPosition + /-- What occupies the relativized position (gap, resumptive, …). -/ + npRel : NPRelType + deriving DecidableEq, Repr + /-! ### Relative-clause marker -/ /-- A relative clause marker or construction in a language. diff --git a/blog/references.bib b/blog/references.bib index adffb7c6e..aecfd0d5c 100644 --- a/blog/references.bib +++ b/blog/references.bib @@ -17194,6 +17194,30 @@ @incollection{cinque-2004 validated = {true}, sources = {Fragments/Italian/Modals.lean;Phenomena/Modality/Bridge/EventRelativityRestructuring.lean} }% REF: Mac Congáil (2004). Irish Grammar. Cois Life. +@book{cinque-2020, + author = {Cinque, Guglielmo}, + year = {2020}, + title = {The Syntax of Relative Clauses: A Unified Analysis}, + series = {Cambridge Studies in Linguistics}, + number = {166}, + publisher = {Cambridge University Press}, + isbn = {9781108479707}, + doi = {10.1017/9781108856195}, + subfield = {syntax}, + role = {formalized}, + sources = {Studies/Cinque2020.lean} +} +@incollection{de-vries-2018, + author = {de Vries, Mark}, + year = {2018}, + title = {Relative Clauses in Syntax}, + booktitle = {Oxford Research Encyclopedia of Linguistics}, + publisher = {Oxford University Press}, + doi = {10.1093/acrefore/9780199384655.013.56}, + subfield = {syntax}, + role = {cited}, + sources = {Studies/Cinque2020.lean} +} @article{embick-2004, author = {Embick, David}, year = {2004},