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.

Comments

  1. Neel KrishnaswamiMay 26, 2014 at 8:29 AM

    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

Post a Comment

Popular posts from this blog

Reading academic papers while having ADHD

Disclaimer : Any discussion of experience with disability walks a tricky line between individual and more "general" experiences. I'll try to make it clear when I'm speaking for just myself vs. reporting "common knowledge" about ADHD, but in either case, remember that ADHD manifests very differently for different people. Please don't make assumptions that my experiences or preferences are the same as yours or someone else you know with ADHD. If you do research, you have to read a lot of papers. Reading papers is challenging for most people, especially when you're new to it, but what if on top of that, you're fighting against a brain that would rather be doing literally anything else? Read on to learn how real live ADHD academics manage this challenge in practice.
Read more

Using Twine for Games Research (Part II)

Image
This  preliminary discussion  introduced my thoughts on using Twine as a tool for creating prototypes for games research. I'll start with documenting my first case study: a hack-and-slash RPG-like setting where the player character has a record of attributes ("stats") that evolve through actions that turn certain resources (money, health, items) into others. I've selected this hack-and-slash example because it falls outside the canonical "branching story" domain thought to be Twine's primary use case, but it is not too much trickier to implement. It relies crucially on the management of state in ways that simple branching stories would not, but it does so in a fairly straightforward way. If all goes well, this post may also serve as a tutorial on the "basics" of Twine (links + variables + expressions). In particular, I'll be using  Twine 2/Harlowe , and I haven't seen many tutorials for this new version published yet. To me, the mai
Read more

Using Twine for Games Research (Part III)

Image
Where we last left off , I described Twine's basic capabilities and illustrated how to use them in Twine 2 by way of a tiny hack-and-slash RPG mechanic. You can play the result , and you should also be able to download that HTML file and use Twine 2's "import file" mechanism to load the editable source code/passage layout. Notice that, in terms of game design, it's not much more sophisticated than a slot machine: the only interesting decision we've incorporated is for the player to determine when to stop pushing her luck with repeated adventures and go home with the current spoils. What makes this type of RPG strategy more interesting to me is the sorts of decisions that can have longer-term effects, the ones where you spend an accumulation of resources on one of several things that might have a substantial payoff down the road. In a more character-based setting, this could be something like increasing skill levels or adding personality traits. Often, th
Read more