Assignment-relative denotations

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$, and abstracting over an index the body does not read gives a constant function.

Main definitions

• Montague.lambdaAbsG: abstraction over an index.

Implementation notes

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

• I. Heim, A. Kratzer, Semantics in Generative Grammar (1998)
• S. Charlow, A modular theory of pronouns and binding (2018)