Thursday, September 9, 2010

Local soundness and completeness are PL-like properties

Currently, I'm trying to write up a tech report that clearly and fully present a peculiar modal logic that I discovered with the help of another graduate student last spring. In this tech report, I'm trying to closely follow what I think is correct to call the judgmental methodology , a philosophy for designing logics that was first outlined by Martin Lof in the 1983 Siena lectures and was refined by Pfenning and Davies in the 1999 paper "A Judgmental Reconstruction of Modal Logic."

Something that I think I knew but that I hadn't ever fully internalized is the degree to which the developments and checks recommended by the judgmental methodology are much closer to what you want when defining a programming language (where type safety - progress and preservation - are primary concerns) than what you want when defining a logic (where consistency, which is a sort of normalization property, is a big concern).

A really, really high level picture of the methodology followed by Pfenning and Davies is this:
  • Define a substitution principle
  • Show that everything that looks it should be a reducible expression (redex) is actually, you know, reducible (local soundness)
  • Show that everything that has an interesting type can be η-expanded (local completeness)
  • Check that the substitution principle which you claimed to be true and possibly used in the previous two steps actually holds
Now, as it turns out, proving the property of local completeness gets you most of the way there to the property called global completeness, but local soundness is woefully inadequate to get what you might call global soundness, the property that given a proof with redexes you can reduce redexes over and over until you get a proof with no redexes anymore. What I think local soundness ensures is that you'll always be able to keep reducing things that looks like redexes unless there aren't any more things that look like redexes. But this is just a progress property, that everything that "looks like a redex" actually is one. The combined local soundness proofs additionally can be seen as the cases of a variant form of the preservation theorem called subject reduction - this means that the local soundness proofs demonstrate both (a sort of) progress property and (a sort of) preservation property.

Is it really the case that the only "more interesting" part of type safety theorems is the fact that programming languages have values - places where, in practice, you want to stop with all of this reducing business - and the safety proof has to show that these uses of values are somehow consistent with the desired progress theorem? And has the "progress-ey" part of local soundness been considered elsewhere? Certainly the preservation-ey part is well-known enough to have its own name, "subject reduction." It seems like the kind of discussion that would be natural to find in the hybrid child of Proofs and Types and TAPL, but I don't believe such a book exists.

1 comment:

  1. Since you're citing my work, thought I'd add my 2 cents. To start: I pretty much agree with most of what you've said here.

    I'd add that local soundness gives you basically all the local behaviour (involving only local parts of a proof) that you'd have if you had global soundness. In particular you can reduce away any redex you want. To me this is quite a strong property to have compared to local soundness not holding.

    What you don't have is the global behaviour that you can always do a sequence of reductions to remove all redices. And I agree that it can be a long way from local soundness to global soundness (Girard's Paradox is a good example of this). Sometimes it's not so far though - such as when the proof terms and reductions can be translated to a known terminating system.

    Regardless when designing systems of logic it is sensible to consider local soundness early on as a basic criteria for sensibility and only consider global soundness much later when most of the other desirable properties appear to be achieved.

    When it comes to programming languages with values and expressions, taking a purely logical C-H viewpoint I'd say that you should consider the underlying core to be a language like Moggi's meta-language - or equivalently with a lax modality. This makes the situation no different to reduction in a logic.

    But clearly it's often not done this way. And then, yes the extra is basically making sure the requirements for values, etc., all match up. But, it's also different because subject reduction generally doesn't always hold - it only holds for redices in evaluation position.

    [This looks like an interesting blog, BTW.]