Discussing "A Modal Analysis of Staged Computation"

(Link)

Authors: Rowan Davies and Frank Pfenning (Carnegie Mellon University)

Reference: Davies, Rowan, and Frank Pfenning. "A modal analysis of staged computation". Journal of the ACM (JACM) 48.3 (2001): 555-604.

Why this paper? Cited by A Fibrational Approach to Multiplicative Additive Indexed Linear Logic and Proofs and Refutations for Intuitionistic and Second-Order Logic

This week we have some work I know and love (although I think I’ve spent more time with the shorter conference version, published in 1996). The central idea is for a programmer to state using their type system in which order (expressed as stages) their program will execute. This would allow various optimisations to be applied automatically at compile time. We achieve this via a new type constructor, written ☐. Code of type ☐A is understood as unevaluated code of that type. For example, there is always a function from ☐A to A, which works by evaluating the code.

The cool thing here for a logician interested in the Curry-Howard isomorphism between proofs and programs is that this new type-former behaves exactly like the necessity, or box, modality of the well known modal logic S4 (more precisely, the intuitionistic version of this logic, without the possibility, or diamond, modality). For example, necessitation (a standard feature of all normal modal logics) corresponds to the ability to treat an arbitrary closed program as code, which does not hold of programs with free variables. So this paper, developing as it does lambda calculi for this box, is both a contribution to a particular programming language problem and to the proof theory of an important modal logic.

There are a number of different calculi developed in this paper, with the most important split between the dual context and context stack approaches. This nicely prefigures more recent work in modal lambda calculus, which supports the conclusion that while other approaches work for specific modal logics, these are the two approaches powerful enough to work for a large variety of modal logics; see here for a modern view of the first approach, and a paper of mine for the second. Another split is between the calculi that hew closely to the simply typed lambda calculus and (although this is not proved, it is fairly clear) are guaranteed to terminate, versus the ‘Mini-ML’ variations that achieve Turing completeness via general fixed points, at the cost of muddying the relationship with logic.

Given the context stack approach is close to my heart, I’ll make some more specific comments on this. Without getting distracted by bike shedding I'll briefly note that I do prefer the older term for this approach, Fitch-style (named in honour of work in proof theory by Frederic Fitch) over the coinage of Kripke-style here (Saul Kripke’s famous ‘possible worlds’ semantics should correspond to any reasonable proof theory, although admittedly Fitch’s approach feels closest to this semantics). The basic idea is that use of our Box modality corresponds to navigating through various layers of contexts; this is a wonderfully general idea and not fixed to the particular logic S4.

One interesting feature of S4 is that ☐…☐A is logically equivalent to ☐A for any number of boxes. My work has shown that if we are willing to allow all boxed types to further be isomorphic (true for many applications, but perhaps not appropriate for this work) we can significantly simplify the calculus of this paper. This works by removing the need for natural number indices to track how many layers of contexts are being popped at a given point of the program, and hence removing the need for ‘modal structural transformations’ in the reduction relation that are needed to relabel indices at various points. This actually contradicts the assertion in this paper that indices are necessary because of a certain ‘coherence’ problem; in fact that problem can be shown to resolve (the proof of this is not that easy), so the indices are in fact only necessary to preserve, if desired, the generality of having ☐…☐A be possibly non-isomorphic (genuinely different) to ☐A.