How to express modalities in lambda calculus - are some extensions required?

Question

Lambda calculus can be used for encoding semantics of natural language, e.g. http://yoavartzi.com/tutorial/ contains full details about semantic parsing of natural language: converting natural language texts into lambda expressions - Cornell Semantic Parsing Framework is used https://github.com/cornell-lic/spf.

My question is - how to express modalities in lambda calculus - are some extensions required? E.g. usual classical modal logics can express beliefs/duties-permissions/knowledge and other kind of modalities. Relational (Kripke) semantics is used for modal logics. So - how can we extend of combine lambda calculus to express modalities?

There is idea to express modalities as just another kind of predicates https://www.amazon.co.uk/Toward-Predicate-Approaches-Modality-Trends-ebook/dp/B016XM48V0 but are there some alternatives, more "natrual" ways to introduce modalities in lambda calculus? Full handling of natural language certainly requires this.

Answer 1

Are extensions required? Not really. You can take an axiomatic description of a modal logic and simply provide a "primitive" lambda term for each. The modal operators would become type constructors. Haskell's IO monad can be viewed this way. Coherence conditions like the monad laws would provide some conversions between terms.

A different approach, which does involve extending the lambda calculus, is described in Frank Pfenning's and Rowan Davies' A Judgmental Reconstruction of Modal Logic. Note, this is for an intuitionistic modal logic. This involves changing the context, or specifically, having multiple contexts to include hypothetically valid propositions. You get rules like:$$ \frac{\Delta;\cdot\vdash M : A}{\Delta;\Gamma\vdash\mathsf{box}\ M:\square A}\qquad\frac{\Delta;\Gamma\vdash M:\square A\quad\Delta,u::A;\Gamma\vdash N:B}{\Delta;\Gamma\vdash\mathsf{let\ box}\ u=M\ \mathsf{in}\ N : B}$$ You should read the $\mathsf{let\ box}\ u = M\ \mathsf{in}\dots$ as pattern matching/a destructuring bind against $M$.

We have:$$ (\lambda m.\mathsf{let\ box}\ u= m\ \mathsf{in}\ u) : \square A \to A \\ (\lambda f.\lambda x.\mathsf{let\ box}\ f'=f\ \mathsf{in\ let\ box}\ x'=x\ \mathsf{in\ box}\ (f'x')) : \square(A\to B)\to\square A\to\square B \\ (\lambda m.\mathsf{let\ box}\ u=m\ \mathsf{in\ box}\ (\mathsf{box}\ u)) : \square A \to \square \square A$$ Handling possibility as opposed to or in addition to necessity requires a bit more cleverness.