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.

Discussing "Structural Proof Theory"

(Link)

Authors: Sara Negri and Jan von Plato (University of Helsinki)

Reference: Negri, Sara, and von Plato, Jan. Structural proof theory. Cambridge University Press, 2001.

Why this book? Cited by Two-sided Sequent Calculi for FDE-like Four-valued Logics and Proof Theory for Intuitionistic Temporal Logic

There has been an unplanned delay to the blog, as two weeks ago there were not enough new recommendations appearing in Google Scholar to recommend any ‘classic papers’ for me to review via their citations, and then one week ago we got this book, which took me a small while to track down. I therefore expect to post twice this week.

A `structural’ proof is one that proceeds via a set of inference rules that forces one to arrange one’s proof in a tree-like structure, using only a limited set of inference rules and axioms. These inference rules generally reflect the logical connectives used to state the proposition one is trying to prove.  For example, to prove a conjunction one `branches’ to prove each side of the conjunction separately. This may seem a mundane or obvious notion, but is actually very young with respect to the long history of logic, originating with Gerhard Gentzen in the 1930s. The structural approach allows one to study the space of proofs for a given logic as an object of mathematical interest in its own right (hence, proof theory) and can help with finding proofs.

The two important systems for structural proof are natural deduction and sequent calculus, both originating with Gentzen. Natural deduction is intended to reflect the natural way in which one reasons logically, and is an important concept in computer science due to its relationship with types: according to the Curry-Howard isomorphism, programs with a given type can be viewed as natural deduction proofs of a certain proposition, and vice versa. Sequent calculus is a slightly less natural notion where one works on `sequents’ which allow one to manipulate one’s premises as well as one’s conclusion(s). This turns out to be an ideal setting in which to study the space of all proofs for a logic, and can support automated proof search and help to demonstrate that non-theorems are not provable. While the two approaches differ, they also have many similarities; for example, both have a notion of an algorithm (called normalisation or reduction for natural deduction, and cut-elimination for sequent calculus) that automatically simplifies unnecessarily complex or indirect proofs.

This book is a careful development of various notions of natural deduction and sequent calculus for classical, intuitionistic, and intermediate logic, including propositions, predicates, equality, and ‘nonlogical rules’ that give one access to the axioms of various parts of logic. Full proof details are given throughout the book, a number of new results are presented alongside the classic results, and care is taken to place ideas in their historical context. The high level of detail make this a less breezy read than, say, Girard’s Proofs and Types, but it is in invaluable tool to anyone working in the area.