November 30th, 2009

beartato phd

(no subject)

Vivek and Dale have this paper which I have some issues with to be sure (it is wildly classical for one thing) but fundamentally it is about focusing and fiddly encodings, and so I am on the same page as it in some sense.

I read it a while ago, but I wanted to point out to yinz the beginning Section 2.3, for it's a nice crisp articulation of certain notions of adequacy.

Let me go off on a brief tangent on the topic of adequacy theorems. In the past I have been down on adequacy, particularly when it seems like merely a token effort of "oh hm well I guess I have to invent a funny thing-on-paper to exactly match the thing-in-twelf that I coded up". However if I take care to hear "adequacy" in my head as being in the same semantic niche as "isomorphism" (in which niche of course it rightfully is) then the confusion clears up.

Are "isomorphisms" important in mathematics? You bet your boolean algebra of clopen subsets they are. Is it important that a given mathematical object is "isomorphic"? Er, what? Isomorphic to what? Answer: No, it doesn't make sense to ask if an object is "isomorphic", nor does it matter a damn bit if a twelf encoding is "adequate" in a vacuum. If you're isomorphic to something else of interest, then that is a useful fact, yes, and if you're an adequate twelf re-presentation of some existing math, then that's cool. But you shouldn't think that a mathematical object or a twelf encoding can't stand alone as the definition of a new concept. Anyhow on the topic of equivalences, n-category theory teaches us that there are various notions of identity, isomorphism, equivalence, weak equivalence and so on --- it's important to know how much the same your fancy new gadget is to various known things in the mathematical wilderness, if at all.

End of tangent! Because Section 2.3 is specifically an articulation of exactly the three notions of adequacy/equivalence that keep coming up over and over when comparing logics, with the third only really gaining prominence in my mind since learning about focusing.

Let me just recapitulate the story a bit here, since allegedly it is so important. Say we have logics K and L. The three notions at stake are

  1. ("provability equivalence") K proves A if and only if L proves A
  2. ("proof equivalence") The set of K-proofs of A are in bijective correspondence with the set of L-proofs of A
  3. ("proof search equivalence") The set of partial K-derivations ending in A are in bijective correspondence with the set of partial L-derivations ending in A

(1) is all you can hope to get if you're just talking about semantics of a logic: if all models say it, then the proof theory says it, and vice-versa. Would you ever hope that the set of all crazy ZFC proofs of a Kripke model satisfying some condition exactly line up with the S4 proofs? Heck no.

Then (2) is sort of the "categorification" of (1). Suddenly we care about the arrows, the way that things are provable/reachable, not just that they are provable/reachable. It only makes sense in terms of a reasonably well-behaved proof theory.

As for (3) I don't actually know how what category theory has to say about it. It is what focusing is good for: faithfully modelling even local failures of proof search, not just global ones. I suppose, reflecting on the issue now, that what counts as a "partial derivation" in a focused system is one that is stable at the leaves, i.e. no inversion or already-committed synchronous work left to do. This is precisely what can model guarded read choice even in an asynchronous π-calculus: if focus goes down one branch of the sum and doesn't stabilize by data ready to ready to receive, then it does not correspond to any transition in the π-calculus transition system.