From 83ea1a20666eb293d6f5941b230647d80aadbcca Mon Sep 17 00:00:00 2001 From: Robert Hawkins Date: Sat, 30 May 2026 19:02:57 -0700 Subject: [PATCH 1/5] feat(Syntax/HPSG): project RelativeClause profile from RC derivation --- Linglib/Syntax/HPSG/Core/RelativeClauses.lean | 40 +++++++++++++++++++ 1 file changed, 40 insertions(+) diff --git a/Linglib/Syntax/HPSG/Core/RelativeClauses.lean b/Linglib/Syntax/HPSG/Core/RelativeClauses.lean index d1bf1be98..3dc2a0140 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.profile` exposes the +`(AHPosition × NPRelType)` 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) -- ============================================================================ -- 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 descriptive profile this derivation realizes: + the relativized AH position paired with the NP_rel type. This is the + shared projection onto `RelativeClause` — comparable across frameworks, + even though the GAP/MOD derivation itself is HPSG-specific. -/ +def RelClauseDerivation.profile (d : RelClauseDerivation) : AHPosition × NPRelType := + (d.position, 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,10 @@ private def relClause : RelClauseDerivation := #guard relClause.isMod #guard relClause.result.sign.synsem.mod == some .NOUN +/-- Object relative ("the book that John read ___") projects to the + `(directObject, gap)` profile on the `RelativeClause` substrate. -/ +example : relClause.profile = (.directObject, .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 +245,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 +260,10 @@ private def modified_boy : Option Sign := #guard modified_boy.isSome +/-- Subject relative ("the boy who saw Mary") projects to the + `(subject, relPronoun)` profile on the `RelativeClause` substrate. -/ +example : who_relClause.profile = (.subject, .relPronoun) := rfl + end SubjectRelative -- ============================================================================ From 504f420ad503777179be1a21023d376d509aecbd Mon Sep 17 00:00:00 2001 From: Robert Hawkins Date: Sat, 30 May 2026 19:08:21 -0700 Subject: [PATCH 2/5] feat(Syntax/Minimalist): project RelativeClause profile from RC example --- Linglib/Syntax/Minimalist/RelativeClauses.lean | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/Linglib/Syntax/Minimalist/RelativeClauses.lean b/Linglib/Syntax/Minimalist/RelativeClauses.lean index 95144de3e..86d5408e7 100644 --- a/Linglib/Syntax/Minimalist/RelativeClauses.lean +++ b/Linglib/Syntax/Minimalist/RelativeClauses.lean @@ -1,5 +1,6 @@ import Linglib.Syntax.Minimalist.TraceInterpretation import Linglib.Syntax.Minimalist.Basic +import Linglib.Typology.RelativeClause.Basic /-! # Relative Clause Semantics: A Worked Example @@ -38,6 +39,7 @@ namespace Minimalist.RelativeClauses open Core.Logic.Intensional Core.Logic.Intensional.Variables Semantics.Composition.Modification open Minimalist +open RelativeClause (AHPosition NPRelType) -- ============================================================================ -- Example Model: Reading Scenario @@ -164,6 +166,18 @@ theorem cp_meaning_correct (g : Core.Assignment readModel.Entity) (x : ReadEntit ip_johnReadTrace, applyG, vp_readTrace, constDenot, john_sem, trace1, interpTrace, interpPronoun, update_same] +/-- The framework-neutral descriptive profile this Minimalist derivation + realizes, projected onto `Typology/RelativeClause/Basic.lean`. The trace + `t₁` sits in the *object* slot of `read` (`vp_readTrace` feeds `trace1` as + `read_sem`'s first argument) → `directObject`; it is a fully-interpreted + bound trace, not a resumptive pronoun → `gap`. The trace+predicate-abstraction + *mechanism* is Minimalism-specific; only this profile is shared. -/ +def cp_relativeClause_profile : AHPosition × NPRelType := (.directObject, .gap) + +/-- "The book that John read ___" is an object-relative gap. -/ +theorem cp_relativeClause_profile_eq : + cp_relativeClause_profile = (.directObject, .gap) := rfl + -- ============================================================================ -- Combining with Head Noun: "book that John read" -- ============================================================================ From b4c9b858e1dcad26cd12f23daa4ee27b10821173 Mon Sep 17 00:00:00 2001 From: Robert Hawkins Date: Sat, 30 May 2026 19:15:34 -0700 Subject: [PATCH 3/5] refactor(RelativeClause): name the per-derivation Realization hook --- Linglib/Syntax/HPSG/Core/RelativeClauses.lean | 28 +++++++++---------- .../Syntax/Minimalist/RelativeClauses.lean | 22 +++++++-------- Linglib/Typology/RelativeClause/Basic.lean | 21 ++++++++++++++ 3 files changed, 44 insertions(+), 27 deletions(-) diff --git a/Linglib/Syntax/HPSG/Core/RelativeClauses.lean b/Linglib/Syntax/HPSG/Core/RelativeClauses.lean index 3dc2a0140..c6c0e23aa 100644 --- a/Linglib/Syntax/HPSG/Core/RelativeClauses.lean +++ b/Linglib/Syntax/HPSG/Core/RelativeClauses.lean @@ -30,8 +30,8 @@ combine with a head noun via the Head-Modifier Schema. 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.profile` exposes the -`(AHPosition × NPRelType)` a derivation realizes. This is the shared +`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. @@ -46,7 +46,7 @@ mechanism from SWB2003 Ch. 14 combined with the MOD feature. namespace HPSG.RelativeClauses open HPSG -open RelativeClause (NPRelType AHPosition) +open RelativeClause (NPRelType AHPosition Realization) -- ============================================================================ -- Relativizers @@ -115,12 +115,12 @@ def RelClauseDerivation.result (d : RelClauseDerivation) : TrackedSign := def RelClauseDerivation.isMod (d : RelClauseDerivation) : Bool := d.result.sign.synsem.mod.isSome -/-- The framework-neutral descriptive profile this derivation realizes: - the relativized AH position paired with the NP_rel type. This is the - shared projection onto `RelativeClause` — comparable across frameworks, - even though the GAP/MOD derivation itself is HPSG-specific. -/ -def RelClauseDerivation.profile (d : RelClauseDerivation) : AHPosition × NPRelType := - (d.position, d.rel.npRel) +/-- 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 @@ -196,9 +196,8 @@ private def relClause : RelClauseDerivation := #guard relClause.isMod #guard relClause.result.sign.synsem.mod == some .NOUN -/-- Object relative ("the book that John read ___") projects to the - `(directObject, gap)` profile on the `RelativeClause` substrate. -/ -example : relClause.profile = (.directObject, .gap) := rfl +/-- 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, @@ -260,9 +259,8 @@ private def modified_boy : Option Sign := #guard modified_boy.isSome -/-- Subject relative ("the boy who saw Mary") projects to the - `(subject, relPronoun)` profile on the `RelativeClause` substrate. -/ -example : who_relClause.profile = (.subject, .relPronoun) := rfl +/-- 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 index 86d5408e7..ab97a1781 100644 --- a/Linglib/Syntax/Minimalist/RelativeClauses.lean +++ b/Linglib/Syntax/Minimalist/RelativeClauses.lean @@ -39,7 +39,7 @@ namespace Minimalist.RelativeClauses open Core.Logic.Intensional Core.Logic.Intensional.Variables Semantics.Composition.Modification open Minimalist -open RelativeClause (AHPosition NPRelType) +open RelativeClause (AHPosition NPRelType Realization) -- ============================================================================ -- Example Model: Reading Scenario @@ -166,17 +166,15 @@ theorem cp_meaning_correct (g : Core.Assignment readModel.Entity) (x : ReadEntit ip_johnReadTrace, applyG, vp_readTrace, constDenot, john_sem, trace1, interpTrace, interpPronoun, update_same] -/-- The framework-neutral descriptive profile this Minimalist derivation - realizes, projected onto `Typology/RelativeClause/Basic.lean`. The trace - `t₁` sits in the *object* slot of `read` (`vp_readTrace` feeds `trace1` as - `read_sem`'s first argument) → `directObject`; it is a fully-interpreted - bound trace, not a resumptive pronoun → `gap`. The trace+predicate-abstraction - *mechanism* is Minimalism-specific; only this profile is shared. -/ -def cp_relativeClause_profile : AHPosition × NPRelType := (.directObject, .gap) - -/-- "The book that John read ___" is an object-relative gap. -/ -theorem cp_relativeClause_profile_eq : - cp_relativeClause_profile = (.directObject, .gap) := rfl +/-- The `RelativeClause.Realization` this Minimalist worked example projects to. + The trace `t₁` sits in the *object* slot of `read` (`vp_readTrace` feeds + `trace1` as `read_sem`'s first argument) → `directObject`; it is a + fully-interpreted bound trace, not a resumptive pronoun → `gap`. The + trace + predicate-abstraction *mechanism* is Minimalism-specific; only this + realization is the shared hook onto the substrate. (Minimalism reifies the + derivation as a bare denotation, so this is a documented annotation of the + worked example rather than a computed projection.) -/ +def cp_relativeClause_realization : Realization := { position := .directObject, npRel := .gap } -- ============================================================================ -- Combining with Head Noun: "book that John read" 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. From 7aceebabf8e197312fc0d7b3c3a0b4137822e444 Mon Sep 17 00:00:00 2001 From: Robert Hawkins Date: Sat, 30 May 2026 19:32:04 -0700 Subject: [PATCH 4/5] feat(Studies): Cinque2020 RC analysis replacing the Minimalist demo --- Linglib.lean | 2 +- Linglib/Studies/Cinque2020.lean | 278 +++++++++++++++ .../Syntax/Minimalist/RelativeClauses.lean | 322 ------------------ blog/references.bib | 24 ++ 4 files changed, 303 insertions(+), 323 deletions(-) create mode 100644 Linglib/Studies/Cinque2020.lean delete mode 100644 Linglib/Syntax/Minimalist/RelativeClauses.lean diff --git a/Linglib.lean b/Linglib.lean index bec650168..a8cc3c609 100644 --- a/Linglib.lean +++ b/Linglib.lean @@ -1153,6 +1153,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 @@ -2182,7 +2183,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..459e58cc7 --- /dev/null +++ b/Linglib/Studies/Cinque2020.lean @@ -0,0 +1,278 @@ +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 (leaving no + overt internal element)? Only the invariant-relativizer strategy and PRO do. -/ +def Strategy.deletesInternalHead : Strategy → Bool + | .invariantRelativizer => true + | .pro => true + | _ => false + +/-- 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). Participials have the + smallest external Head; non-restrictives the biggest (above DP). -/ +def RCType.mergeHeight : RCType → Nat + | .participial => 0 + | .restrictive => 1 + | .maximalizing => 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) : Bool := + match r.derivation with + | .raising => true + | .matching => false + +/-- @cite{cinque-2020}'s deletion-licensing condition: the internal Head may be + deleted (the gap, invariant-relativizer / PRO strategies) 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 resumptive. (Stated as the decidable `¬deletes ∨ matches`.) -/ +def RC.WellFormed (r : RC) : Prop := + r.strategy.deletesInternalHead = false ∨ 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 -/ + +/-- Raising makes the *internal* Head overt. -/ +theorem overtHead_raising : Derivation.raising.overtHead = .internal := rfl + +/-- Matching makes the *external* Head overt. -/ +theorem overtHead_matching : Derivation.matching.overtHead = .external := rfl + +/-- A matching derivation shows no reconstruction. -/ +theorem matching_no_reconstruction (r : RC) (h : r.derivation = .matching) : + r.reconstructs = false := by + unfold RC.reconstructs; rw [h] + +/-- **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 + rcases h with hf | hi + · rw [hs] at hf; exact absurd hf (by decide) + · rw [hbig] at hi; exact absurd hi (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 + +/-! ### 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. -/ +example : 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. -/ +example : + ¬ ({ 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.reconstructs = true := rfl +example : englishThatObject.reconstructs = false := rfl + +end Cinque2020 diff --git a/Linglib/Syntax/Minimalist/RelativeClauses.lean b/Linglib/Syntax/Minimalist/RelativeClauses.lean deleted file mode 100644 index ab97a1781..000000000 --- a/Linglib/Syntax/Minimalist/RelativeClauses.lean +++ /dev/null @@ -1,322 +0,0 @@ -import Linglib.Syntax.Minimalist.TraceInterpretation -import Linglib.Syntax.Minimalist.Basic -import Linglib.Typology.RelativeClause.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 -open RelativeClause (AHPosition NPRelType Realization) - --- ============================================================================ --- 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] - -/-- The `RelativeClause.Realization` this Minimalist worked example projects to. - The trace `t₁` sits in the *object* slot of `read` (`vp_readTrace` feeds - `trace1` as `read_sem`'s first argument) → `directObject`; it is a - fully-interpreted bound trace, not a resumptive pronoun → `gap`. The - trace + predicate-abstraction *mechanism* is Minimalism-specific; only this - realization is the shared hook onto the substrate. (Minimalism reifies the - derivation as a bare denotation, so this is a documented annotation of the - worked example rather than a computed projection.) -/ -def cp_relativeClause_realization : Realization := { position := .directObject, npRel := .gap } - --- ============================================================================ --- 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/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}, From 18fa2cfbba4e1a1bde55e0fc448007a4b1de7c73 Mon Sep 17 00:00:00 2001 From: Robert Hawkins Date: Sat, 30 May 2026 19:42:27 -0700 Subject: [PATCH 5/5] fix(Studies/Cinque2020): correct maximalizing merge height; Prop predicates --- Linglib/Studies/Cinque2020.lean | 81 ++++++++++++++++++--------------- 1 file changed, 45 insertions(+), 36 deletions(-) diff --git a/Linglib/Studies/Cinque2020.lean b/Linglib/Studies/Cinque2020.lean index 459e58cc7..8345d659f 100644 --- a/Linglib/Studies/Cinque2020.lean +++ b/Linglib/Studies/Cinque2020.lean @@ -104,12 +104,15 @@ inductive Strategy | verbCoding deriving DecidableEq, Repr -/-- Does this strategy realize the internal Head by *deleting* it (leaving no - overt internal element)? Only the invariant-relativizer strategy and PRO do. -/ -def Strategy.deletesInternalHead : Strategy → Bool - | .invariantRelativizer => true - | .pro => true - | _ => false +/-- 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 @@ -134,12 +137,15 @@ inductive RCType | nonRestrictive deriving DecidableEq, Repr -/-- Relative merge height (bigger external Head = higher). Participials have the - smallest external Head; non-restrictives the biggest (above DP). -/ +/-- 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 - | .restrictive => 1 - | .maximalizing => 2 + | .maximalizing => 1 + | .restrictive => 2 | .kindDefining => 3 | .nonRestrictive => 4 @@ -164,18 +170,18 @@ 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) : Bool := - match r.derivation with - | .raising => true - | .matching => false +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 / PRO strategies) 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 resumptive. (Stated as the decidable `¬deletes ∨ matches`.) -/ + 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 = false ∨ r.internalHeadCategory = .indefiniteDP + r.strategy.DeletesInternalHead → r.internalHeadCategory = .indefiniteDP instance (r : RC) : Decidable r.WellFormed := by unfold RC.WellFormed; infer_instance @@ -189,16 +195,10 @@ def RC.realization (r : RC) : Realization := /-! ### Consequences -/ -/-- Raising makes the *internal* Head overt. -/ -theorem overtHead_raising : Derivation.raising.overtHead = .internal := rfl - -/-- Matching makes the *external* Head overt. -/ -theorem overtHead_matching : Derivation.matching.overtHead = .external := rfl - -/-- A matching derivation shows no reconstruction. -/ -theorem matching_no_reconstruction (r : RC) (h : r.derivation = .matching) : - r.reconstructs = false := by - unfold RC.reconstructs; rw [h] +/-- 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 @@ -207,9 +207,10 @@ theorem bigger_head_no_gap_deletion (r : RC) (h : r.WellFormed) (hbig : r.internalHeadCategory = .biggerDPKP) : r.strategy ≠ .invariantRelativizer := by intro hs - rcases h with hf | hi - · rw [hs] at hf; exact absurd hf (by decide) - · rw [hbig] at hi; exact absurd hi (by decide) + 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 : @@ -220,6 +221,12 @@ 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 @@ -235,7 +242,8 @@ 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. -/ -example : englishThatObject.realization = { position := .directObject, npRel := .gap } := rfl +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 @@ -251,7 +259,7 @@ example : /-- The deletion-licensing bite: an oblique (bigger) internal Head *cannot* be deleted via the invariant relativizer — that derivation is ill-formed. -/ -example : +theorem oblique_gap_deletion_illFormed : ¬ ({ rcType := .restrictive, derivation := .matching, internalHeadCategory := .biggerDPKP, strategy := .invariantRelativizer, position := .oblique, rcPosition := .postNominal } : RC).WellFormed := by decide @@ -272,7 +280,8 @@ def englishRaisingObject : RC := internalHeadCategory := .indefiniteDP, strategy := .invariantRelativizer, position := .directObject, rcPosition := .postNominal } -example : englishRaisingObject.reconstructs = true := rfl -example : englishThatObject.reconstructs = false := rfl +example : englishRaisingObject.overtHead = .internal := rfl +example : englishRaisingObject.Reconstructs := by decide +example : ¬ englishThatObject.Reconstructs := by decide end Cinque2020