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*.
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