Structural focalization updated

I've uploaded to both ArXiV and my webpage a significantly revised draft of the paper Structural focalization, which I've spoken about here before. Feedback is welcome!

One of the points I make about the structural focalization technique is that, because it is all so nicely structurally inductive, it can be formalized in Twelf. As part of a separate project, I've now also repeated the whole structural focalization development in Agda! The code is available from GitHub. While a structural focalization proof has some more moving parts than a simple cut-and-identity proof, it also has one significant advantage over every Agda proof of cut admissibility that I'm aware of: it requires no extra structural metrics beyond normal structural induction! (My favorite structural metric is the totally nameless representation, but there are other ways of threading that needle, including, presumably, these "sized types" that everyone seems to talk about.)

In regular, natural-deduction substitution, you can get away without structural metrics by proving the statement that if \(\Gamma \vdash A\) and \(\Gamma, A, \Gamma' \vdash C\) then \(\Gamma, \Gamma' \vdash C\); the extra "slack" given by \(\Gamma'\) means that you operate by structural induction on the second given derivation without ever needing to apply weakening or exchange. Most cut-elimination proofs are structured in such a way that you have to apply left commutative and right commutative cuts on both of the given derivations, making this process tricky at the best; I've never gotten it to work at all, but you might be able to do something like "if \(\Gamma, \Gamma' \longrightarrow A\) and \(\Gamma, A, \Gamma'' \longrightarrow C\) then \(\Gamma, \Gamma', \Gamma'' \longrightarrow C\)." If someone can make this work let me know!

A focused sequent calculus, on the other hand, has three separate phases of substitution. The first phase is principal substitution, where the type gets smaller and you can do whatever you want to the derivations, including weakening them. The second phase is rightist substitution, which acts much like natural-deduction substitution, and where you can similarly get away with adding "slack" to the second derivation. The third phase is leftist substitution, and you can get by in this phase by adding "slack" to the first derivation: the leftist cases read something like "if \(\Gamma, \Gamma' \longrightarrow A\) and \(\Gamma, A \longrightarrow C\) then \(\Gamma, \Gamma' \longrightarrow C\)."

In Structural focalization, I note that the structural focalization technique could be seen as a really freaking complicated way of proving the cut and identity for an unfocused sequent calculus. But in Agda, there's a reason you might actually want to do things the "long way" - not only do you have something better when you finish (a focalization result), but you get cut and identity without needing an annoying structural metric.

My New Focalization Technique is Unstoppable

While it took, as they say, a bit of doing, I have a completed draft of a paper on my website that I believe provides a really elegant solution to what has been a very, very annoying problem for some time: writing down a proof called the completeness of focusing. Don't worry, the paper explains what that means: it has to, because one of the things the paper argues is that most existing statements of the completeness of focusing aren't general enough! In the process, this writeup gave me a good (enough) excuse to talk in a very general way about a lot of fundamental phenomena around the idea of polarization in logic that we've been noticing in recent years.

Anyway, the draft is here - Structural Focalization. The accompanying Twelf development is, of course, on the Twelf wiki: Focusing. I've thrown the paper and the Twelf code up on arXiv while I figure out while I figure out what to do with it; comments would be greatly appreciated!

I don't want to have a post that's just "hey here's a paper," so here's an addition, a follow-up to the rather popular "Totally Nameless Representation" post from awhile back. I still prove weakening in Agda by exactly the technique presented there, which commenter thecod called the "presheaf method." But for natural deduction systems, I almost never use the term metric approach that was the core of what I was presenting in "totally nameless representation," since it works just fine to use the approach where term M of type A (the one you're substituting for x) is in context Γ and the term N (the one with x free) is in context Γ' ++ A :: Γ - the free variable x is allowed to be in the middle of the context, in other words; you don't have to use exchange on the second term, so you're always calling induction on something Agda recognizes as structurally smaller.

This worked for natural deduction systems, but I didn't think it would work for sequent calculi, since you needed to toy around with both contexts and induct on both terms in presentation of cut for a sequent calculus. However, for a focused sequent calculus like what I present in the paper, you still can do without the totally nameless metric! If you set things up right, the rightist substitutions (where you work on decomposing the right term, the one with the variable free) allow you to extend the context only of the first term, and the leftist substitutions (where you work on decomposing the left term, the one you're substituting for the variable) allow you to work on the second term, and the two are only connected by the principal substitutions (which reduce the type, which more or less lets you get away with anything as far as the induction principle is concerned).

A code example of this, which could use some more commentary, can be found on GitHub: Polar.agda.

Two new papers

I have a post on typestate that has been languishing while I've been spending a lot of time on CMU's admissions committe, but now that that's over I hopefully will be able to get back to it. But first, two papers:

Logical Approximation for Program Analysis

My paper with Frank Pfenning, Logical Approximation for Program Analysis, has been accepted to HOSC. This paper extends of the work from the PEPM 2009 paper Linear logical approximations [ACM Link] - the acceptance is actually to a HOSC special issue on PEPM 2009. However, this paper also synthesizes a lot of stuff from our LICS 2009 paper Substructural Operational Semantics as Ordered Logic Programming. The point of this journal paper is to provide a story about allowing substructural operational semantics specifications of programming language, written in the style of the LICS 2009 paper/my thesis proposal, to be approximated. The approximation process lets us derive program analyses like control flow and alias analysis in the style of the PEPM 2009 paper.

Anyway: PDF, which I'm still polishing for final submission this weekend.

It occurs to me that I should write some more substructural operational semantics posts on this blog, seeing as that's my thesis topic and all.

Constructive Provability Logic

Since Bernardo and I got the principles of constructive provability logic nailed down, we've done a little more exploring. The most important thing about this paper, relative to the technical report, is that it presents a less restricted version of constructive provability logic (the "de-tethered variant" CPL*); I think this less restricted version is going to be critical to understanding logic programming through the lens of constructive provability logic, which is my ultimate goal for the project. The second new thing about the paper is that we nailed down (with one perplexing exception) which of the "normal" axioms of intuitionistic modal logic do or don't hold.

What does this mean? Well, any classical logician will tell you that, in order to be a modal logic, you have to obey one axiom - the "K" axiom, □(A → B) → □A → □B - and one rule, which is that if you can prove A with no assumptions then you can also prove □A ("necessitation"). And any intuitionistic modal logic worth its salt is going to do the same, so far so good. However, intuitionstic modal logic also has a possibility modality ◇A. In classical logic saying something is possible is the same as saying that it's not necessarily false, so ◇A is defined as ¬□¬A. But in intuitionistic logic we tend to think of possibility as a genuinely different thing, and that's where stuff gets complicated. The two most important proof theories for intuitionistic modal logic are probably Alex Simpson's IK - which describes a whole bunch of intuitionistic modal logics - and Pfenning-Davies S4, which describes S4. Some of the axioms that Simpson claims are fundamental to intuitionistic modal logics, like (◇A → □B) → □(A → B), don't hold in Pfenning-Davies S4; it turns out that particular axiom doesn't hold in constructive provability logic, either.

As we discuss in the paper, it seems like the de-tethered variant, CPL*, lies between Pfenning-Davies S4 and Simpson-style S4 on the "which axioms hold" meter, whereas CPL (the tethered version of constructive provability logic from the tech report) may or may not have the same "normal" axioms as Pfenning-Davies; we are currently stuck on whether the ◇◇A → ◇A holds in CPL - it definitely holds in CPL*, Simpson-style S4, and Pfenning-Davies S4, but we are a bit perplexed by our inability to prove or disprove it in CPL.

Here's the PDF, and here's the bitbucket repository with all our Agda. As a side note, "oh, all these proofs are in Agda so we're not discussing them" makes the whole "omitted due to space" thing feel way, way less sketchy. This is just a submission at this point, so comments are especially welcome!

Type Inference, In and Out of Context

Our reading group read the 2010 MSFP paper Type Inference In Context by Adam Gundry, Conor McBride, and James McKinna (ACM link). This was mostly because not all of us went to ICFP and not all of us that went to ICFP saw that MSFP talk (I was at HLPP and others were at WMM, IIRC man there are lots of acronyms in this sentence.)

Anyway, the people that went to the MSFP talk really liked the talk, so we read the paper. Some of it was confusing because state monad is not my native language. To understand it better, I re-implemented it in ML after the reading group. William and I then got into a discussion about how he had written a trying-to-be-very-clean implementation of the imperative type inference algorithm for MinML, so I adapted the algorithm further to the larger MinML language, and then adapted Williams code so that it ran in parallel with mine. And then I decided I wanted to throw the whole thing on my door as a parallel-corpus sort of thing.

The result is an impossibly sized PDF poster that I can turn into 6 tabloid sheets and put on my door, titled "Type Inference, In & Out of Context." It isn't aimed at being particularly introductory, but if you have read the MSFP paper it may be helpful as a guide to ML transfer, and I found the comparison to the imperative version of type inference quite enlightening.

There's a secondary interesting question here: what are good ways to present large pieces of literate code for dissemination? I kind of like this narrated poster form, especially for parallel corpuses, and I like literate Twelf things like the page on lax logic, but because I haven't had a lot of feedback and haven't been a reader of a lot of these sorts of things, I don't know how good I am at pulling it off. I'd appreciate feedback!

[Update Nov 18, 2010] Michael Sullivan notes that one aspect of "good ways to present large pieces of literate code" is actually providing the code so it doesn't have to be ineffectually cut and pasted from a pdf. The code is available in three files: typebase.sml (the language definition, snoc lists, and cons lists), typenoctx.sml (the imperative algorithm), and typeinctx.sml (the pure algorithm).