From 0076fe974452937a0b5e8537fd833891e4c9fb24 Mon Sep 17 00:00:00 2001 From: Robert Hawkins Date: Sun, 31 May 2026 02:48:39 -0700 Subject: [PATCH] feat(Semantics/Modification): Modifier substrate + RelativeClause.denote --- Linglib.lean | 5 +- Linglib/Semantics/ArgumentStructure/LF.lean | 15 +- .../Semantics/Composition/Abstraction.lean | 59 ++++ .../Semantics/Composition/Modification.lean | 186 ----------- Linglib/Semantics/Composition/Tree.lean | 6 +- Linglib/Semantics/Modification/Basic.lean | 80 +++++ .../Modification/RelativeClause.lean | 76 +++++ Linglib/Studies/AhnKocabDavidson2026.lean | 16 +- Linglib/Studies/Bondarenko2022.lean | 11 +- Linglib/Studies/HawkinsGweonGoodman2021.lean | 12 +- .../Syntax/Minimalist/RelativeClauses.lean | 310 ------------------ .../Minimalist/TraceInterpretation.lean | 82 +---- 12 files changed, 266 insertions(+), 592 deletions(-) create mode 100644 Linglib/Semantics/Composition/Abstraction.lean delete mode 100644 Linglib/Semantics/Composition/Modification.lean create mode 100644 Linglib/Semantics/Modification/Basic.lean create mode 100644 Linglib/Semantics/Modification/RelativeClause.lean delete mode 100644 Linglib/Syntax/Minimalist/RelativeClauses.lean diff --git a/Linglib.lean b/Linglib.lean index 2088303dd..4e4ab57c4 100644 --- a/Linglib.lean +++ b/Linglib.lean @@ -2181,7 +2181,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 @@ -2321,7 +2320,9 @@ import Linglib.Core.Categorical.ScaleCat import Linglib.Semantics.Composition.SyntaxInterface import Linglib.Studies.Borer2005 import Linglib.Semantics.ArgumentStructure.VoiceSemantics -import Linglib.Semantics.Composition.Modification +import Linglib.Semantics.Composition.Abstraction +import Linglib.Semantics.Modification.Basic +import Linglib.Semantics.Modification.RelativeClause import Linglib.Semantics.Quantification.CovertQuantifier import Linglib.Semantics.Quantification.Binominal import Linglib.Semantics.Classifier.Basic diff --git a/Linglib/Semantics/ArgumentStructure/LF.lean b/Linglib/Semantics/ArgumentStructure/LF.lean index 3ccbe5953..bc98127f1 100644 --- a/Linglib/Semantics/ArgumentStructure/LF.lean +++ b/Linglib/Semantics/ArgumentStructure/LF.lean @@ -1,4 +1,5 @@ import Linglib.Semantics.ArgumentStructure.Defs +import Linglib.Semantics.Modification.Basic /-! # Thematic Roles — Davidsonian logical forms + axioms @@ -27,6 +28,7 @@ forms, and adverbial modification (Davidson's key payoff). namespace Semantics.ArgumentStructure open Core.Time +open Modifier (intersective intersective_apply) /-! ### Thematic axioms (Aktionsart selection + uniqueness) -/ @@ -71,17 +73,20 @@ abbrev EventModifier (Time : Type*) [LinearOrder Time] := Event Time → Prop /-- Apply a modifier to an event predicate via conjunction. @cite{davidson-1967}: adverbial modification is conjunction of event predicates. "John kicked the ball quickly" = ∃e. kick(e) ∧ - Agent(j,e) ∧ Patient(b,e) ∧ quickly(e). -/ + Agent(j,e) ∧ Patient(b,e) ∧ quickly(e). + + Davidson's adverbial modification is the intersective modifier + (`Semantics.Modification.intersective`) at event-predicate type. -/ def modify {Time : Type*} [LinearOrder Time] (P : Event Time → Prop) (M : EventModifier Time) : Event Time → Prop := - λ e => P e ∧ M e + intersective P M /-- Modification is commutative: "quickly and loudly" = "loudly and quickly". -/ theorem modify_comm {Time : Type*} [LinearOrder Time] (P : Event Time → Prop) (M₁ M₂ : EventModifier Time) : modify (modify P M₁) M₂ = modify (modify P M₂) M₁ := by funext e - simp only [modify] + simp only [modify, intersective_apply] exact propext ⟨λ ⟨⟨hp, hm1⟩, hm2⟩ => ⟨⟨hp, hm2⟩, hm1⟩, λ ⟨⟨hp, hm2⟩, hm1⟩ => ⟨⟨hp, hm1⟩, hm2⟩⟩ @@ -90,7 +95,7 @@ theorem modify_assoc {Time : Type*} [LinearOrder Time] (P : Event Time → Prop) (M₁ M₂ : EventModifier Time) : modify (modify P M₁) M₂ = modify P (λ e => M₁ e ∧ M₂ e) := by funext e - simp only [modify] + simp only [modify, intersective_apply] exact propext ⟨λ ⟨⟨hp, hm1⟩, hm2⟩ => ⟨hp, hm1, hm2⟩, λ ⟨hp, hm1, hm2⟩ => ⟨⟨hp, hm1⟩, hm2⟩⟩ @@ -119,7 +124,7 @@ theorem modified_stative_is_pm {Entity Time : Type*} [LinearOrder Time] (x : Entity) (M : EventModifier Time) : modifiedStativeLogicalForm P frame x M ↔ stativeLogicalForm (modify P M) frame x := by - simp only [modifiedStativeLogicalForm, stativeLogicalForm, modify] + simp only [modifiedStativeLogicalForm, stativeLogicalForm, modify, intersective_apply] exact ⟨fun ⟨s, hp, hh, hm⟩ => ⟨s, ⟨hp, hm⟩, hh⟩, fun ⟨s, ⟨hp, hm⟩, hh⟩ => ⟨s, hp, hh, hm⟩⟩ diff --git a/Linglib/Semantics/Composition/Abstraction.lean b/Linglib/Semantics/Composition/Abstraction.lean new file mode 100644 index 000000000..c0368c528 --- /dev/null +++ b/Linglib/Semantics/Composition/Abstraction.lean @@ -0,0 +1,59 @@ +import Linglib.Core.Logic.Intensional.Frame +import Linglib.Core.Logic.Intensional.Variables + +/-! +# Predicate Abstraction +@cite{heim-kratzer-1998} + +Predicate Abstraction (@cite{heim-kratzer-1998} Ch. 7) is the composition rule +that λ-binds a variable index, turning a proposition (type `t`) into a property +(type `e ⇒ t`): + + `⟦[XP Op_n YP]⟧^g = λx. ⟦YP⟧^{g[n ↦ x]}` + +where `YP` contains a variable (a trace or pronoun) at index `n`. It is the +sibling of Predicate Modification (`Modifier.intersective`, in +`Semantics/Modification/Basic.lean`) — the two non-FA composition rules of +@cite{heim-kratzer-1998} — and is +framework-neutral: any analysis that abstracts over a gap (a Minimalist trace, an +HPSG `SLASH` discharge, a CCG type-raised argument) realizes this rule. + +## Main declarations + +* `predicateAbstraction` — the rule at result type `t` (the common case). +* `predicateAbstractionGen` — the rule at an arbitrary result type `τ`. + +The relative-clause denotation built from this rule (`RelativeClause.denote`) lives +in `Semantics/RelativeClause.lean`. +-/ + +namespace Semantics.Composition.Abstraction + +open Core.Logic.Intensional Core.Logic.Intensional.Variables + +/-- +Predicate Abstraction (@cite{heim-kratzer-1998} Ch. 7): λ-bind at index `n`, +turning a proposition into a property by abstracting over the variable left at `n`. + + `⟦[XP Op_n YP]⟧^g = λx. ⟦YP⟧^{g[n ↦ x]}` +-/ +def predicateAbstraction {F : Frame} (n : ℕ) (body : DenotG F .t) + : DenotG F (.e ⇒ .t) := + lambdaAbsG n body + +/-- +Generalized predicate abstraction for any result type — e.g. "the book that John +said Mary read _", where the trace is embedded and the result needs further +composition. +-/ +def predicateAbstractionGen {F : Frame} {τ : Ty} (n : ℕ) (body : DenotG F τ) + : DenotG F (.e ⇒ τ) := + lambdaAbsG n body + +/-- Applying a predicate-abstracted meaning at index `n` to `x` is evaluation of + the body under the assignment updated at `n` to `x`. -/ +theorem predicateAbstraction_apply {F : Frame} (n : ℕ) (body : DenotG F .t) + (x : F.Entity) (g : Core.Assignment F.Entity) + : (predicateAbstraction n body g) x = body (g[n ↦ x]) := rfl + +end Semantics.Composition.Abstraction diff --git a/Linglib/Semantics/Composition/Modification.lean b/Linglib/Semantics/Composition/Modification.lean deleted file mode 100644 index fe080624d..000000000 --- a/Linglib/Semantics/Composition/Modification.lean +++ /dev/null @@ -1,186 +0,0 @@ -/- -# Predicate Modification -@cite{kamp-1975} @cite{kamp-partee-1995} @cite{parsons-1970} - -Predicate modification (@cite{heim-kratzer-1998} Ch. 4): -`⟦α β⟧ = λx. ⟦α⟧(x) ∧ ⟦β⟧(x)`, valid for intersective adjectives only. - -The adjective classification hierarchy (intersective, subsective, -privative, extensional) is in -`Semantics/Gradability/Classification.lean`. --/ - -import Linglib.Core.Logic.Intensional.Frame -import Linglib.Semantics.Composition.ToyDomain -import Mathlib.Data.Set.Basic - -namespace Semantics.Composition.Modification - -open Core.Logic.Intensional - -section Generic - -/-- Predicate modification: `⟦α β⟧ = λx. ⟦α⟧(x) ∧ ⟦β⟧(x)` -/ -def predMod {E : Type*} (p q : E → Bool) : E → Bool := - λ x => p x && q x - -def truePred {E : Type*} : E → Bool := λ _ => true - -theorem predMod_comm {E : Type*} (p q : E → Bool) : predMod p q = predMod q p := by - funext x; simp only [predMod, Bool.and_comm] - -theorem predMod_assoc {E : Type*} (p q r : E → Bool) : - predMod (predMod p q) r = predMod p (predMod q r) := by - funext x; simp only [predMod, Bool.and_assoc] - -theorem predMod_true_right {E : Type*} (p : E → Bool) : predMod p truePred = p := by - funext x; simp only [predMod, truePred, Bool.and_true] - -theorem predMod_true_left {E : Type*} (p : E → Bool) : predMod truePred p = p := by - funext x; simp only [predMod, truePred, Bool.true_and] - -end Generic - -/-! The adjective classification hierarchy (intersective, subsective, - privative, extensional) is in `Gradability/Classification.lean`. - This file provides the composition operation (Predicate Modification) - that implements the intersective case. -/ - -section PredicateModification - -def predicateModification {F : Frame} - (p₁ p₂ : F.Denot (.e ⇒ .t)) : F.Denot (.e ⇒ .t) := - λ x => p₁ x ∧ p₂ x - -infixl:70 " ⊓ₚ " => predicateModification - -theorem predicateModification_comm {F : Frame} (p₁ p₂ : F.Denot (.e ⇒ .t)) - : p₁ ⊓ₚ p₂ = p₂ ⊓ₚ p₁ := by - funext x - simp only [predicateModification, And.comm] - -theorem predicateModification_assoc {F : Frame} - (p₁ p₂ p₃ : F.Denot (.e ⇒ .t)) - : (p₁ ⊓ₚ p₂) ⊓ₚ p₃ = p₁ ⊓ₚ (p₂ ⊓ₚ p₃) := by - funext x - exact propext and_assoc - -theorem predicateModification_idem {F : Frame} (p : F.Denot (.e ⇒ .t)) - : p ⊓ₚ p = p := by - funext x - exact propext ⟨fun ⟨h, _⟩ => h, fun h => ⟨h, h⟩⟩ - -theorem predicateModification_true_right {F : Frame} (p : F.Denot (.e ⇒ .t)) - : p ⊓ₚ (λ _ => True) = p := by - funext x - exact propext ⟨fun ⟨h, _⟩ => h, fun h => ⟨h, trivial⟩⟩ - -theorem predicateModification_true_left {F : Frame} (p : F.Denot (.e ⇒ .t)) - : (λ _ => True) ⊓ₚ p = p := by - funext x - exact propext ⟨fun ⟨_, h⟩ => h, fun h => ⟨trivial, h⟩⟩ - -theorem predicateModification_false_right {F : Frame} (p : F.Denot (.e ⇒ .t)) - : p ⊓ₚ (λ _ => False) = (λ _ => False) := by - funext x - exact propext ⟨fun ⟨_, h⟩ => h, fun h => h.elim⟩ - -theorem predicateModification_false_left {F : Frame} (p : F.Denot (.e ⇒ .t)) - : (λ _ => False) ⊓ₚ p = (λ _ => False) := by - funext x - exact propext ⟨fun ⟨h, _⟩ => h, fun h => h.elim⟩ - -theorem predicateModification_extension {F : Frame} - (p₁ p₂ : F.Denot (.e ⇒ .t)) - : predicateToSet (p₁ ⊓ₚ p₂) = predicateToSet p₁ ∩ predicateToSet p₂ := by - ext x - simp only [predicateToSet, predicateModification, Set.mem_setOf_eq, Set.mem_inter_iff] - -theorem predicateModification_subset_left {F : Frame} - (p q r : F.Denot (.e ⇒ .t)) - (h : predicateToSet p ⊆ predicateToSet q) - : predicateToSet (p ⊓ₚ r) ⊆ predicateToSet (q ⊓ₚ r) := by - simp only [predicateModification_extension] - exact Set.inter_subset_inter_left _ h - -theorem predicateModification_subset_right {F : Frame} - (p q r : F.Denot (.e ⇒ .t)) - (h : predicateToSet p ⊆ predicateToSet q) - : predicateToSet (r ⊓ₚ p) ⊆ predicateToSet (r ⊓ₚ q) := by - simp only [predicateModification_extension] - exact Set.inter_subset_inter_right _ h - -/-- `(P ⊓ₚ Q)(x) ↔ P(x) ∧ Q(x)` -/ -theorem intersective_equivalence {F : Frame} - (p q : F.Denot (.e ⇒ .t)) (x : F.Entity) - : (p ⊓ₚ q) x ↔ p x ∧ q x := by - exact Iff.rfl - -theorem intersective_equivalence_set {F : Frame} - (p q : F.Denot (.e ⇒ .t)) (x : F.Entity) - : x ∈ predicateToSet (p ⊓ₚ q) ↔ x ∈ predicateToSet p ∧ x ∈ predicateToSet q := - Iff.rfl - -theorem pm_entails_left {F : Frame} - (p q : F.Denot (.e ⇒ .t)) (x : F.Entity) - (h : (p ⊓ₚ q) x) : p x := h.1 - -theorem pm_entails_right {F : Frame} - (p q : F.Denot (.e ⇒ .t)) (x : F.Entity) - (h : (p ⊓ₚ q) x) : q x := h.2 - -theorem pm_intro {F : Frame} - (p q : F.Denot (.e ⇒ .t)) (x : F.Entity) - (hp : p x) (hq : q x) : (p ⊓ₚ q) x := ⟨hp, hq⟩ - -end PredicateModification - -section Examples - -open Semantics.Montague (toyModel) -open Semantics.Montague.ToyEntity Semantics.Montague.ToyLexicon - -def gray_sem : toyModel.Denot (.e ⇒ .t) := - λ x => match x with - | .john => True - | .mary => True - | _ => False - -def cat_sem : toyModel.Denot (.e ⇒ .t) := - λ x => match x with - | .pizza => True - | _ => False - -def big_sem : toyModel.Denot (.e ⇒ .t) := - λ x => match x with - | .book => True - | _ => False - -def grayCat_sem : toyModel.Denot (.e ⇒ .t) := - gray_sem ⊓ₚ cat_sem - -example : predicateToSet grayCat_sem = predicateToSet gray_sem ∩ predicateToSet cat_sem := - predicateModification_extension gray_sem cat_sem - -theorem grayCat_empty : predicateToSet grayCat_sem = ∅ := by - ext x - show grayCat_sem x ↔ x ∈ (∅ : Set _) - simp only [Set.mem_empty_iff_false, iff_false] - cases x <;> simp [grayCat_sem, predicateModification, gray_sem, cat_sem] - -def bigGrayCat_sem : toyModel.Denot (.e ⇒ .t) := - big_sem ⊓ₚ (gray_sem ⊓ₚ cat_sem) - -theorem bigGrayCat_assoc : - big_sem ⊓ₚ (gray_sem ⊓ₚ cat_sem) = (big_sem ⊓ₚ gray_sem) ⊓ₚ cat_sem := - (predicateModification_assoc big_sem gray_sem cat_sem).symm - -theorem grayCat_order : - gray_sem ⊓ₚ (big_sem ⊓ₚ cat_sem) = big_sem ⊓ₚ (gray_sem ⊓ₚ cat_sem) := by - conv_lhs => rw [← predicateModification_assoc] - conv_rhs => rw [← predicateModification_assoc] - rw [predicateModification_comm gray_sem big_sem] - -end Examples - -end Semantics.Composition.Modification diff --git a/Linglib/Semantics/Composition/Tree.lean b/Linglib/Semantics/Composition/Tree.lean index 9a12d9e79..6a53328b3 100644 --- a/Linglib/Semantics/Composition/Tree.lean +++ b/Linglib/Semantics/Composition/Tree.lean @@ -17,11 +17,11 @@ import Linglib.Core.Tree import Linglib.Core.Logic.Intensional.Frame import Linglib.Core.Logic.Intensional.Variables import Linglib.Semantics.Composition.LexEntry -import Linglib.Semantics.Composition.Modification +import Linglib.Semantics.Modification.Basic namespace Semantics.Composition.Tree -open Core.Logic.Intensional Semantics.Composition.Modification +open Core.Logic.Intensional open Core.Logic.Intensional.Variables open Semantics.Montague (Lexicon) @@ -119,7 +119,7 @@ def tryPM {F : Frame} (d1 d2 : TypedDenot F) : Option (TypedDenot F) := | .fn .e .t, .fn .e .t => let p1 : F.Denot (.e ⇒ .t) := h1 ▸ d1.val let p2 : F.Denot (.e ⇒ .t) := h2 ▸ d2.val - some ⟨.fn .e .t, predicateModification p1 p2⟩ + some ⟨.fn .e .t, Modifier.intersective p1 p2⟩ | _, _ => none /-- Binary node: try FA, then IFA, then PM. -/ diff --git a/Linglib/Semantics/Modification/Basic.lean b/Linglib/Semantics/Modification/Basic.lean new file mode 100644 index 000000000..dd31c83ba --- /dev/null +++ b/Linglib/Semantics/Modification/Basic.lean @@ -0,0 +1,80 @@ +import Mathlib.Logic.Basic + +/-! +# Modifiers +@cite{parsons-1970} @cite{kamp-1975} + +A **modifier** of `τ` is a function on the modificand's denotation +(@cite{parsons-1970}: "modifiers as functions on predicates"). Adjectives, +adverbs, and relative clauses are all modifiers — of *different* `τ` (nominal +`e ⇒ t`, event `Event → Prop`, …) — unified by *being* this type, not by +implementing an interface. + +The well-behaved special case is **intersective** modification: conjunction with a +fixed property (`λx. P x ∧ Q x`), on which restrictive relative clauses, +intersective adjectives, and manner adverbs all converge. + +## Main declarations + +* `Modifier` — a modifier of `τ` is an endofunction `τ → τ`. +* `Modifier.intersective` — the intersective modifier built from a property `P`. +* `Modifier.isIntersective` / `.isSubsective` / `.isPrivative` — the + @cite{kamp-1975} modifier-meaning classification, as predicates on a modifier. + +## Implementation notes + +`Modifier.intersective` is the canonical intersective-modification operation; the +concrete reflexes reduce to it (`ArgumentStructure/LF.EventModifier.modify` over +events calls it; the type-driven interpreter's Predicate Modification step is it at +`e ⇒ t`). The adjective-specific classification in `Gradability/Classification` +(over `AdjMeaning`) is the remaining copy to fold onto these forms (follow-up). +-/ + +/-- A modifier of `τ` is a function on the modificand's denotation + (@cite{parsons-1970}). Adjectives, adverbs, and relative clauses are modifiers + of different `τ`; they compose as endofunctions (modifier stacking). -/ +abbrev Modifier (τ : Type*) := τ → τ + +namespace Modifier + +variable {α : Type*} + +/-- The intersective modifier built from a property `P`: combine `P` with the + modificand by pointwise conjunction. The well-behaved special case + (restrictive relative clauses, intersective adjectives, manner adverbs). -/ +def intersective (P : α → Prop) : Modifier (α → Prop) := + fun Q x => P x ∧ Q x + +@[simp] theorem intersective_apply (P Q : α → Prop) (x : α) : + intersective P Q x = (P x ∧ Q x) := rfl + +/-- Head and modifier intersect symmetrically (conjunction is commutative). -/ +theorem intersective_comm (P Q : α → Prop) : intersective P Q = intersective Q P := by + funext x; exact propext And.comm + +/-- A modifier is **intersective** if it is conjunction with some fixed property. -/ +def isIntersective (m : Modifier (α → Prop)) : Prop := + ∃ P : α → Prop, ∀ Q, m Q = intersective P Q + +/-- A modifier is **subsective** if its output always entails the modificand + (`m Q ⊆ Q`): a skillful surgeon is a surgeon. -/ +def isSubsective (m : Modifier (α → Prop)) : Prop := + ∀ Q x, m Q x → Q x + +/-- A modifier is **privative** if its output is disjoint from the modificand + (`m Q ∩ Q = ∅`): a fake gun is not a gun. -/ +def isPrivative (m : Modifier (α → Prop)) : Prop := + ∀ Q x, m Q x → ¬ Q x + +theorem intersective_isIntersective (P : α → Prop) : isIntersective (intersective P) := + ⟨P, fun _ => rfl⟩ + +/-- Intersective ⟹ subsective (@cite{kamp-1975}'s implication structure). -/ +theorem isSubsective_of_isIntersective {m : Modifier (α → Prop)} + (h : isIntersective m) : isSubsective m := by + obtain ⟨P, hP⟩ := h + intro Q x hx + rw [hP Q] at hx + exact hx.2 + +end Modifier diff --git a/Linglib/Semantics/Modification/RelativeClause.lean b/Linglib/Semantics/Modification/RelativeClause.lean new file mode 100644 index 000000000..c9a8fe12b --- /dev/null +++ b/Linglib/Semantics/Modification/RelativeClause.lean @@ -0,0 +1,76 @@ +import Linglib.Core.Logic.Intensional.Frame +import Linglib.Core.Logic.Intensional.Variables +import Linglib.Semantics.Composition.Abstraction +import Linglib.Semantics.Modification.Basic + +/-! +# Relative-clause denotation +@cite{heim-kratzer-1998} + +The framework-neutral meaning of a head noun combined with a (restrictive) +relative clause: an RC is an **intersective clausal modifier** of the head. Its +modifier-property is the relative clause abstracted over its gap (Predicate +Abstraction, @cite{heim-kratzer-1998} Ch. 5); modifying the head with it is the +intersective modification shared with adjectives and PPs. This is the +adnominal-modifier diagnostic (a relative clause's framework-neutral essence is +clausal modification of a nominal head) made compositional: the syntactic +frameworks differ in how they derive the gap abstraction (a Minimalist trace, an +HPSG `SLASH` discharge, a CCG type-raised argument) but converge on this +denotation. + +This is the **semantic half of the `RelativeClause` API**; the classification half +(`Realization`, `AHPosition`, `NPRelType`, …) lives in `Typology/RelativeClause/`, +sharing the root `RelativeClause` namespace without either importing the other. + +## Main declarations + +* `RelativeClause.denote` — the relative-clause denotation, built *by construction* + as `Modification.intersective` applied to the gap-abstracted clause. +* `RelativeClause.denote_comm` — head and clause modify symmetrically. + +## Implementation notes + +Only the restrictive (intersective) denotation is provided; the non-restrictive +(appositive) denotation is a distinct, non-intersective mechanism and is deferred +until a study reifies it. +-/ + +namespace RelativeClause + +open Core.Logic.Intensional Core.Logic.Intensional.Variables +open Semantics.Composition.Abstraction (predicateAbstraction) +open Modifier (intersective intersective_comm) + +/-- +The framework-neutral relative-clause denotation: the head modified by the +relative clause, qua intersective modifier. + +For "the N that ... t_n ...": +1. abstract the relative clause over its gap, `λx. ⟦... t_n ...⟧^{g[n ↦ x]}` + (Predicate Abstraction) — this is the RC's modifier-property; +2. modify the head noun with it intersectively (`Modification.intersective`). + +Result: `λx. ⟦relative clause⟧(x) ∧ N(x)` — the head property intersected with the +abstracted clause property (the restrictive case; see the implementation note). +That the RC is an intersective modifier is true by construction. +-/ +def denote {F : Frame} (n : ℕ) + (headNoun : DenotG F (.e ⇒ .t)) + (relClauseBody : DenotG F .t) + : DenotG F (.e ⇒ .t) := + fun g => intersective (predicateAbstraction n relClauseBody g) (headNoun g) + +/-- Head and relative clause modify symmetrically: the head noun and the + gap-abstracted clause intersect in either order (intersective modification is + commutative). -/ +theorem denote_comm {F : Frame} (n : ℕ) + (headNoun : DenotG F (.e ⇒ .t)) + (relClauseBody : DenotG F .t) + (g : Core.Assignment F.Entity) + : denote n headNoun relClauseBody g = + intersective (headNoun g) (predicateAbstraction n relClauseBody g) := by + show intersective (predicateAbstraction n relClauseBody g) (headNoun g) = + intersective (headNoun g) (predicateAbstraction n relClauseBody g) + exact intersective_comm _ _ + +end RelativeClause diff --git a/Linglib/Studies/AhnKocabDavidson2026.lean b/Linglib/Studies/AhnKocabDavidson2026.lean index 4e4ebca01..0ce60c330 100644 --- a/Linglib/Studies/AhnKocabDavidson2026.lean +++ b/Linglib/Studies/AhnKocabDavidson2026.lean @@ -1,4 +1,3 @@ -import Linglib.Semantics.Composition.Modification import Linglib.Studies.Ariel2001 import Linglib.Pragmatics.GriceanMaxims import Linglib.Pragmatics.Expressives.Basic @@ -49,11 +48,24 @@ set_option autoImplicit false namespace AhnKocabDavidson2026 -open Semantics.Composition.Modification (predMod truePred predMod_true_left predMod_comm) open Features (AccessibilityLevel) open Pragmatics.GriceanMaxims open Pragmatics.Expressives (TwoDimProp) +/-! Local `Bool`-valued predicate conjunction (transitional: this file's + `Bool`/`native_decide` computational layer is being retired; the canonical + intersective modifier is `Modifier.intersective`, Prop-valued). -/ + +private def predMod {E : Type*} (p q : E → Bool) : E → Bool := fun x => p x && q x + +private def truePred {E : Type*} : E → Bool := fun _ => true + +private theorem predMod_comm {E : Type*} (p q : E → Bool) : predMod p q = predMod q p := by + funext x; simp only [predMod, Bool.and_comm] + +private theorem predMod_true_left {E : Type*} (p : E → Bool) : predMod truePred p = p := by + funext x; simp only [predMod, truePred, Bool.true_and] + /-- Basic semantic classes for NP entities (inlined from substrate; @cite{resnik-1996} / @cite{erk-2007} style selectional classes). Used by this paper specifically for `VerbLocusType` → SemClass diff --git a/Linglib/Studies/Bondarenko2022.lean b/Linglib/Studies/Bondarenko2022.lean index f21973210..498af453d 100644 --- a/Linglib/Studies/Bondarenko2022.lean +++ b/Linglib/Studies/Bondarenko2022.lean @@ -570,8 +570,8 @@ theorem nominalizedCP_satisfies_every_theta : -- ════════════════════════════════════════════════════════════════ -- -- Per Layered Grounding obligation (cross-framework auditor): --- consume `Semantics.Composition.Modification`'s --- `predicateModification` (`⊓ₚ`) — DO NOT redefine PM here. The +-- consume `Modifier.intersective` (the intersective-modification +-- substrate) — DO NOT redefine PM here. The -- substrate operates over `Frame.Denot (.e ⇒ .t)` typed-semantics -- predicates; this Studies file states only the abstract -- compositional fact (bare CP composes via PM with v's situation @@ -589,10 +589,9 @@ theorem nominalizedCP_satisfies_every_theta : situation argument iff it has predicate type (⟨s,t⟩ after lifting the individual variable in Bondarenko's lift; substantively, both arguments are situation-predicates and intersect by PM). The - `predicateModification` substrate at - `Semantics/Composition/Modification.lean` is the typed - realisation; this Studies-level predicate is its qualitative - projection. -/ + `Modifier.intersective` substrate at + `Semantics/Modification/Basic.lean` is the typed realisation; this + Studies-level predicate is its qualitative projection. -/ def composesViaPM : ClauseType → Prop | .predicateOfIndividuals => False -- nominalised, no PM compatibility | .predicateOfSituations => True -- bare, PM-compatible diff --git a/Linglib/Studies/HawkinsGweonGoodman2021.lean b/Linglib/Studies/HawkinsGweonGoodman2021.lean index 820a7b46c..6bd5de3bf 100644 --- a/Linglib/Studies/HawkinsGweonGoodman2021.lean +++ b/Linglib/Studies/HawkinsGweonGoodman2021.lean @@ -45,7 +45,6 @@ the RSAConfig loop as paper-specific extensions (Part V). import Linglib.Tactics.RSAPredict import Linglib.Pragmatics.RSA.Basic -import Linglib.Semantics.Composition.Modification import Mathlib.Data.Rat.Defs set_option autoImplicit false @@ -371,12 +370,19 @@ that denotes a characteristic function of type `e → t`: - ⟦blue⟧ = λx. color(x) = target.color - ⟦checked⟧ = λx. texture(x) = target.texture -This is exactly `Semantics.Composition.Modification.predMod` applied iteratively. +This is exactly `predMod` (local; the Prop analogue is `Modifier.intersective`) +applied iteratively. -/ namespace MontaguGrounding -open Semantics.Composition.Modification +/-! Local `Bool`-valued predicate conjunction (transitional: this file's + `Bool`/`rsa_predict` computational layer is being retired; the canonical + intersective modifier is `Modifier.intersective`, Prop-valued). -/ + +private def predMod {E : Type*} (p q : E → Bool) : E → Bool := fun x => p x && q x + +private def truePred {E : Type*} : E → Bool := fun _ => true /-- Shape predicate: matches target's shape (only target has shape=0) -/ def shapePred : VisObj → Bool 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/Syntax/Minimalist/TraceInterpretation.lean b/Linglib/Syntax/Minimalist/TraceInterpretation.lean index d8a90b8bb..ff96c678a 100644 --- a/Linglib/Syntax/Minimalist/TraceInterpretation.lean +++ b/Linglib/Syntax/Minimalist/TraceInterpretation.lean @@ -1,7 +1,7 @@ import Linglib.Syntax.Minimalist.Basic import Linglib.Core.Logic.Intensional.Frame import Linglib.Core.Logic.Intensional.Variables -import Linglib.Semantics.Composition.Modification +import Linglib.Semantics.Composition.Abstraction /-! # Trace Interpretation @@ -15,9 +15,10 @@ Traces left by movement are interpreted as variables bound by 1. Trace Interpretation: a trace t_n is interpreted as g(n) ⟦t_n⟧^g = g(n) -2. Predicate Abstraction: at the landing site of movement, - λ-abstract over the trace's index - ⟦[CP Op_n ... t_n ...]⟧^g = λx. ⟦... t_n ...⟧^{g[n↦x]} +2. Predicate Abstraction (the λ-abstraction at the landing site) and the + relative-clause denotation it feeds are framework-neutral composition rules, + so they live in `Semantics/Composition/Abstraction.lean`; this file is the + Minimalist trace machinery that applies them. ## Trace convention @@ -29,7 +30,8 @@ detected via `isTrace so`. namespace Minimalist -open Core.Logic.Intensional Core.Logic.Intensional.Variables Semantics.Composition.Modification +open Core.Logic.Intensional Core.Logic.Intensional.Variables +open Semantics.Composition.Abstraction -- ============================================================================ -- Trace Interpretation (H&K Ch. 5, 7) @@ -47,37 +49,6 @@ open Core.Logic.Intensional Core.Logic.Intensional.Variables Semantics.Compositi abbrev interpTrace {F : Frame} (n : ℕ) : DenotG F .e := interpPronoun n --- ============================================================================ --- Predicate Abstraction (H&K Ch. 7) --- ============================================================================ - -/-- -Predicate Abstraction: λ-bind at the landing site of movement. - -When a moved element lands at a position, it creates a λ-abstractor -that binds the trace it left behind: - - ⟦[XP Op_n YP]⟧^g = λx. ⟦YP⟧^{g[n↦x]} - -where Op_n is the moved operator and YP contains the trace t_n. - -This rule creates a predicate (type ⟨e,t⟩) from a proposition (type t) -by abstracting over the trace's index. --/ -def predicateAbstraction {F : Frame} (n : ℕ) (body : DenotG F .t) - : DenotG F (.e ⇒ .t) := - lambdaAbsG n body - -/-- -Generalized predicate abstraction for any result type. - -This handles cases like "the book that John said Mary read _" -where the trace is embedded and the result may need further composition. --/ -def predicateAbstractionGen {F : Frame} {τ : Ty} (n : ℕ) (body : DenotG F τ) - : DenotG F (.e ⇒ τ) := - lambdaAbsG n body - -- ============================================================================ -- Composition of Movement Chains -- ============================================================================ @@ -93,16 +64,6 @@ def interpMovement {F : Frame} (n : ℕ) (bodyWithTrace : DenotG F .t) : DenotG F (.e ⇒ .t) := predicateAbstraction n bodyWithTrace -/-- -The binding relationship: predicate abstraction at index n binds traces at n. - -When we apply a predicate-abstracted meaning to an entity, -that entity becomes the value of all traces with the same index. --/ -theorem binding_correct {F : Frame} (n : ℕ) (body : DenotG F .t) - (x : F.Entity) (g : Core.Assignment F.Entity) - : (predicateAbstraction n body g) x = body (g[n ↦ x]) := rfl - -- ============================================================================ -- Connection to Syntactic Objects -- ============================================================================ @@ -205,33 +166,4 @@ theorem abstraction_binds_correct_variable {F : Frame} (n : ℕ) simp only [interpTrace, interpPronoun] exact update_same g n x --- ============================================================================ --- Integration with Predicate Modification --- ============================================================================ - -/-- -Relative clause interpretation combines predicate abstraction with PM. - -For "the N that... t..."": -1. Interpret the relative clause as λx. ⟦... t_n...⟧^{g[n↦x]} -2. Combine with the head noun via Predicate Modification - -Result: λx. N(x) ∧ ⟦relative clause⟧(x) --/ -def relativePM {F : Frame} (n : ℕ) - (headNoun : DenotG F (.e ⇒ .t)) - (relClauseBody : DenotG F .t) - : DenotG F (.e ⇒ .t) := - λ g => predicateModification (headNoun g) (predicateAbstraction n relClauseBody g) - -/-- Relative PM is commutative (the order of N and RC doesn't matter) -/ -theorem relativePM_comm {F : Frame} (n : ℕ) - (headNoun : DenotG F (.e ⇒ .t)) - (relClauseBody : DenotG F .t) - (g : Core.Assignment F.Entity) - : relativePM n headNoun relClauseBody g = - predicateModification (predicateAbstraction n relClauseBody g) (headNoun g) := by - simp only [relativePM, predicateModification_comm] - - end Minimalist