Saturday, May 24, 2014

Zoo of term assignments for linear sequent calculus

It's pretty common to give term assignments to logics presented through natural deduction. We usually call them "(typed) functional programming languages."

What's less common, though possible, is to give a term assignment to sequent representations. I've come across enough of these for linear logic in particular that I can make a little petting zoo for you.

Terms as concurrent processes, from Caires, Pfenning, and Toninho's Session Types:




Terms as stories (or more accurately, narrative structures), from Bosser, Cortieu, Forest, and Cavazza's "Structural Analysis of Narratives with the Coq Proof Assistant":

Terms as plans, from Cresswell, Smail, and Richardson's "Deductive Synthesis of Recursive Plans in Linear Logic" (paywall warning, but searching those terms also turns up a .ps.gz):




The latter two are especially interesting to me because (a) they elide term markers for certain rules (such as tensor left), and moreso because they don't really go into what reduction means in these settings: proofs-as-programs is powerful not just because of the surface syntax puns, but because it goes as deep as reduction semantics. The definition of program evaluation -- as in, running computation -- can be derived from "harmony" properties of the two rules defining each logical connective (more formally these properties are called local expansion and contraction). A similar idea is demonstrated for session types and the Cut rule.

Maybe there's nothing interesting to say there in the context of stories and plans, but I'd be surprised -- especially if we start talking about equivalence rather than reduction.

1 comment:

  1. One fact which I think is insufficiently appreciated is that most compilers end up transforming programs from natural deduction to sequent calculus --- we just call it A-normal form, or let-normal form, or even CPS! Basically any representation which names every subexpression can be seen as a term assignment for a sequent calculus.

    ReplyDelete