I’m currently learning modal logic. It’s turning out to be awesome. I’m hoping, sometime (oh, in the next hundred years or so) to be able to use it to formalise the
Any kind of labelled transition system can be talked about modally, but so can many other things, such as time. A simple example: defining two modalities
P (future and past) plus their respective duals
H) such that
P are inverses means that theorems such as
p -> GPp
p -> HFp
are universally true of such systems. (Respectively: if something is true now then at all future times it will have been true in the past; if something is true now, then at all past times it was going to be true in the future.) Temporal modal logic is obviously relevant to interaction [Pnu92], but modality in general seems to offer a nice framework for thinking about lots and lots of things: state, control, and dynamic scoping, to mention some existing applications, but also incremental computation, transactional concurrency, declarative concurrency, mobile code; the list goes on. And on.
That’s the theory side of things, for now. On the practical front, I’m trying to understand monads and monad transformers well enough to implement a backtracking interpreter in Haskell that addresses the famously poor interaction between a normal-order or lazy reduction strategy and function caching or memoisation. The problem is simple: to be any good as an incrementalisation technique, memoisation needs to know the values of arguments to functions up front. But normal-order reduction defers the evaluation of arguments until they’re needed. A prima facie conflict of interests.
I have a vague notion of a solution, an idea gleaned from Avi Pfeffer’s work on IBAL [Pfe06], but much more investigation is required. The nice thing about implementing the interpreter using monads is that it should transfer easily into a modal language, as it turns out monads themselves are closely related to modal logic [Kob97][Pfe01].
(Actually call-by-need – the technique usually used to implement call-by-name – uses something like memoisation to avoid evaluating arguments more than once. But call-by-need is still a