feat(Semantics/Modification): Modifier substrate + RelativeClause.denote

Linglib.lean

@@ -2321,7 +2321,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

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⟩⟩
 

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

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. -/