feat(Semantics/Composition): intensions in the engine, real IFA

Linglib/Semantics/Composition/Assignment.lean

@@ -6,33 +6,26 @@ public import Mathlib.Logic.Function.DependsOn
 /-!
 # Assignment-relative denotations
 
-This file defines the denotation of binders relative to a variable assignment `g : ℕ → E`, which
-gives each index a value. In the textbook of Heim and Kratzer, the Traces and Pronouns Rule has a
-pronoun or trace with index `n` denote `g n`, the evaluation `Function.eval n` of the assignment,
-and Predicate Abstraction has a binder at `n` abstract over the value of `n` by updating `g`. An
-assignment-relative denotation in `α` is a function `Assignment E → α`, a computation of Lean's
-reader monad `ReaderM (Assignment E)`. Charlow factors the standard theory through this monad: its
-`pure`, `<*>` and `joinM` are his lift `ρ`, application `⊛` and flattener `μ`, and `lambdaAbsG` is
-his categorematic abstraction `Λᵢ`.
-
-The indices a denotation reads are those it depends on, in the sense of mathlib's `DependsOn`. An
-abstraction over `n` reads the indices its body reads other than `n`, and abstracting over an
-index the body does not read gives a constant function.
+A *variable assignment* gives each index a value. A pronoun or trace with index $n$ denotes the
+value it gives $n$, by Heim and Kratzer's Traces and Pronouns Rule, and a binder with index $n$
+abstracts over that value, by Predicate Abstraction; Charlow factors both through the reader monad.
+An abstraction over $n$ [reads the indices its body reads other than $n$](##dependsOn_lambdaAbsG),
+and abstracting over an index the body does not read
+[gives a constant function](##lambdaAbsG_eq_const_iff).
 
 ## Main definitions
 
-* `lambdaAbsG`: abstraction over an index.
-
-## Main results
-
-* `dependsOn_lambdaAbsG`: abstraction over `n` removes `n` from the indices a body depends on.
-* `lambdaAbsG_eq_const_iff`: abstraction over `n` is constant at every assignment exactly when
-  the body does not depend on `n`.
+* `Montague.lambdaAbsG`: abstraction over an index.
 
 ## Implementation notes
 
-Assignments are total, where Heim and Kratzer's are partial, so a pronoun denotes at every
-assignment. Nothing fixes `E` to entities: at an assignment of situations, a pronoun is a
+An assignment is a function `g : ℕ → E`, and a pronoun with index `n` denotes `g n`, the
+evaluation `Function.eval n` of the assignment. An assignment-relative denotation in `α` is a
+function `Assignment E → α`, a computation of Lean's `ReaderM (Assignment E)`, whose `pure`, `<*>`
+and `joinM` are Charlow's lift `ρ`, application `⊛` and flattener `μ`, and `lambdaAbsG` is his
+`Λᵢ`. The indices a denotation reads are those it depends on in the sense of mathlib's
+`DependsOn`. Assignments are total, where Heim and Kratzer's are partial, so a pronoun denotes at
+every assignment. Nothing fixes `E` to entities: at an assignment of situations, a pronoun is a
 situation pronoun.
 
 ## References
@@ -50,8 +43,8 @@ open scoped Assignment
 
 variable {E α : Type*} {n : ℕ}
 
-/-- `lambdaAbsG n body` is the abstraction of `body` over index `n`, which at the assignment `g`
-maps `x` to the value of `body` at `g[n ↦ x]`. -/
+/-- The abstraction of `body` over the index `n`: at the assignment `g` it maps `x` to the value
+of `body` at `g[n ↦ x]`. -/
 def lambdaAbsG (n : ℕ) (body : Assignment E → α) : Assignment E → E → α :=
   fun g x ↦ body (g[n ↦ x])
 

Linglib/Semantics/Composition/Coordination.lean

@@ -6,26 +6,27 @@ public import Linglib.Semantics.Composition.Tree
 /-!
 # Coordination in the composition engine
 
-This file adds coordination to the composition engine of `Composition/Tree.lean` as a binary
-mode beside functional application, intensional application and predicate modification. Two
-sisters of the same conjoinable type combine by what their coordinator denotes on the pair,
-`Coordinator.denote`, in the pointwise complete Boolean algebra of that type, which the mode
-finds at runtime through `Ty.Domain.completeBooleanAlgebra?`. Predicate modification is the
-conjunctive case at `⟨e,t⟩`, so the engine's modification mode already agrees with the
-coordinator's denotation.
+Two sisters of the same conjoinable type, a type that ends in $t$, can combine by coordination:
+their coordinator's denotation applies to the pair in the pointwise Boolean algebra of the type,
+so that *and* conjoins truth values, predicates and quantifiers alike. Coordination is a mode
+beside functional application, intensional application and predicate modification, and
+predicate modification is
+[the conjunctive case at the type of predicates](##combine?_eq_coordinate?_of_conjunctive), so
+the engine's modification mode agrees with what *and* denotes.
 
 ## Main definitions
 
 * `Coordinator.coordinate?`: the coordination mode.
 
-## Main results
+## Implementation notes
 
-* `Coordinator.combine?_eq_coordinate?_of_conjunctive`: predicate modification is conjunctive
-  coordination at `⟨e,t⟩`.
+The mode finds the Boolean algebra of its daughters' type at run time, through
+`Ty.Domain.completeBooleanAlgebra?`; `Coordinator.denote` is the coordinator's denotation.
 
 ## References
 
 * [heim-kratzer-1998]
+* [partee-rooth-1983]
 -/
 
 @[expose] public section
@@ -34,9 +35,9 @@ namespace Coordinator
 
 open Montague
 
-/-- `coordinate? c d1 d2` combines two sisters of the same conjoinable type by what the
-coordinator `c` denotes on the pair, in the complete Boolean algebra of their type, threaded
-through the effect `M`, and is `none` on sisters of different or non-conjoinable types. -/
+/-- The coordination of two sisters of the same conjoinable type by what the coordinator `c`
+denotes on the pair, in the complete Boolean algebra of their type and through the effect `M`;
+`none` on sisters of different or non-conjoinable types. -/
 def coordinate? {E W : Type} {M : Type → Type} [Applicative M] (c : Coordinator)
     (d1 d2 : Denotation E W M) : Option (Denotation E W M) :=
   if h : d1.1 = d2.1 then

Linglib/Semantics/Composition/EventIdentification.lean

@@ -3,35 +3,26 @@ module
 public import Linglib.Semantics.Modification.Basic
 
 /-!
-# Event Identification
+# Event identification
 
-This file defines Event Identification, the composition principle by which Kratzer adds an
-argument-introducing head to a predicate of events. The head denotes a relation between
-individuals and events, the predicate a set of events, and the two combine by conjunction at the
-event, leaving the individual argument open: an agent head and *feed the dog* yield the relation
-that holds of an individual and an event when the individual is the agent of the event and the
-event is a feeding of the dog. Event Identification is meet with the predicate lifted to a
-relation constant in the individual, so it is the relational counterpart of predicate
-modification, and repeated applications chain conditions on the same event.
+*Event identification* is Kratzer's rule for adding an argument-introducing head to a predicate
+of events: the head's relation between individuals and events and the predicate's set of events
+combine by conjunction at the event, leaving the individual open. It is
+[meet with the predicate lifted to a relation](##eventIdentification_eq_inf), the relational
+counterpart of predicate modification, and
+[two applications conjoin their predicates](##eventIdentification_eventIdentification).
 
 ## Main definitions
 
 * `ArgumentStructure.eventIdentification`: the combination of a relation and a predicate.
 
-## Main results
-
-* `eventIdentification_eq_inf`, `eventIdentification_eq_comp`: Event Identification is meet
-  with the lifted predicate, and predicate modification of each section of the relation.
-* `eventIdentification_eventIdentification`: two applications conjoin the predicates.
-* `eventIdentification_eq_bot_iff`: the result is empty exactly when, for every individual, the
-  relation's events and the predicate's are disjoint.
-
 ## Implementation notes
 
 Kratzer's rule is partial: it is undefined when the two inputs restrict the event to disjoint
-sorts, actions and states. Here it is total, and such inputs yield the empty relation
-(`eventIdentification_eq_bot_iff`). The carrier is any pair of types, so that the type-driven
-composition engine, whose events share the domain of individuals, uses the same operation.
+sorts, actions and states. Here it is total, and such inputs
+[yield the empty relation](##eventIdentification_eq_bot_iff). The carrier is any pair of types,
+so that the type-driven composition engine, whose events share the domain of individuals, uses
+the same operation.
 
 ## References
 

Linglib/Semantics/Composition/Extensional.lean

@@ -6,29 +6,14 @@ public import Linglib.Logic.Modal.Defs
 /-!
 # Extensional operators
 
-An operator on intensions is *extensional* at an index when the value it yields there depends only
-on the extension of its argument at that index. Negation is extensional: whether *it is not
-raining* is true at a world depends only on whether *it is raining* is true there. Necessity is
-not, since whether *it must be raining* is true at a world depends on whether *it is raining* is
-true at the worlds accessible from it. Among adjectives, which map properties to properties,
-*gray* is extensional and *skillful* is not: where the cobblers are exactly the darts players, the
-gray cobblers are the gray darts players, but the skillful cobblers need not be the skillful darts
-players.
-
-An operator is extensional exactly when it is
-[a function on extensions applied index by index](##isExtensional_iff_exists_eq_piMap). At an
-index where it is extensional, an operator
-[gives the same value on an intension and on the constant intension with the same
-extension](##isExtensionalAt_iff_forall_const), and so
-[cannot tell a variable it binds from one fixed at that index](##isExtensionalAt_iff_forall_diag):
-a situation variable bound under negation reads as if it were free. The truth-functional
-connectives are extensional, and so are composites of extensional operators.
-
-In general the value of an operator at an index depends on its argument at some set of indices,
-and the operator is extensional there when that set can be taken to be the index alone. Necessity
-in a Kripke frame depends at a world on
-[exactly the worlds accessible from it](##ModalLogic.dependsOn_box_iff), so it is
-[extensional only at a world that accesses no world but itself](##isExtensionalAt_box_iff).
+An operator on intensions is *extensional* at an index when its value there depends only on its
+argument's extension there: negation is extensional, necessity is not, and among adjectives
+*gray* is and *skillful* is not. An operator is extensional exactly when it is
+[a function on extensions applied index by index](##isExtensional_iff_exists_eq_piMap), and at an
+index where it is extensional it
+[cannot tell a variable it binds from one fixed there](##isExtensionalAt_iff_forall_diag).
+Necessity is [extensional only at a world that accesses no world but
+itself](##isExtensionalAt_box_iff).
 
 ## Main definitions
 

Linglib/Semantics/Composition/FirstOrder.lean

@@ -10,13 +10,12 @@ public import Mathlib.Tactic.FinCases
 /-!
 # The first-order fragment of type-driven composition
 
-The first-order constants over a signature are its constant and relation symbols, the
-determiners *every*, *some* and *no*, negation, conjunction and disjunction. Every logical form
-over them reads back to a first-order formula whose realization is the logical form's
-denotation. The readback evaluates the logical form in a syntactic model built from mathlib's
-terms and bounded formulas, and a logical relation with the standard model proves it sound, so
-first-order consequence between readbacks is entailment between trees, as
-`Semantics/Dynamic/DRS/Reduction.lean` shows for DRT.
+A logical form built only from names, predicates, the determiners *every*, *some* and *no*, and
+the truth-functional connectives reads back to a first-order formula with the same truth
+conditions, [soundly](##realizes_readback). So
+[a tree holds exactly where its readback is true](##holdsAt_iff_realizeAt),
+[entailment between trees is first-order consequence](##models_imp_iff_entails), and
+[families of trees satisfy compactness](##holdsAt_compactness).
 
 ## Main definitions
 
@@ -27,19 +26,10 @@ first-order consequence between readbacks is entailment between trees, as
 * `Term.readback`, `Term.toFormula`: the readback of a logical form.
 * `Ty.Realizes`: the logical relation between the syntactic and the standard model.
 
-## Main results
-
-* `Term.realizes_readback`: a logical form's readback realizes its denotation whenever the
-  readbacks of its constants realize theirs.
-* `Term.realizeAt_toFormula`: a first-order logical form denotes the realization of its readback.
-* `PhraseStructure.Tree.holdsAt_iff_realizeAt`, `PhraseStructure.Tree.holdsAt_of_models`,
-  `PhraseStructure.Tree.models_imp_iff_entails`, `PhraseStructure.Tree.holdsAt_compactness`: a
-  tree holds (`PhraseStructure.Tree.HoldsAt`) where its readback is realized, entailment between
-  trees is first-order consequence, and families of trees satisfy compactness.
-
 ## Implementation notes
 
-The syntactic model is indexed by the number of bound variables in scope, and gives truth values
+The syntactic model is built from mathlib's terms and bounded formulas, and indexed by the
+number of bound variables in scope, and gives truth values
 and functions at every larger number, so a determiner binds the next de Bruijn variable of
 `BoundedFormula` without computing a fresh name. Formulas are never carried to more bound
 variables, since `BoundedFormula.castLE` keeps the index an inner quantifier binds. *Most* is not