Syntax!

There is a new draft on my web page, that should be of interest to those who enjoyed my posts about reversing data structures and the relation between natural deduction and sequent calculus. It is an article submitted to APLAS 2013, and it is called Proofs, upside down. In a nutshell, I am arguing for the use of functional PL tools, in particular classic functional program transformations, to understand and explain proof theory phenomena. Here, I show that there is the same relationship between natural deduction and (a restriction of) the sequent calculus than between this recursive function:

let rec tower_rec = function
 | [] -> 1
 | x :: xs -> x ∗∗ tower_rec xs
let tower xs = tower_rec xs

written in "direct style", and that equivalent, iterative version:

let rec tower_acc acc = function
 | [] -> acc
 | x :: xs -> tower_acc (x ∗∗ acc) xs
let tower xs = tower_acc 1 (List.rev xs)

written in "accumulator-passing style". And that relationship is the composition of CPS-transformation, defunctionalization and reforestation, the well-known transformations we all came to know and love!

I hope you enjoy it. Of course, any comment will be much appreciated, so don’t hesitate to drop a line below!

Proofs, upside down
A functional correspondence between natural deduction and the sequent calculus
It is well-known in proof theory that sequent calculus proofs differ from natural deduction proofs by "reversing" elimination rules upside down into left introduction rules. It is also well-known that to each recursive, functional program corresponds an equivalent iterative, accumulator-passing program, where the accumulator stores the continuation of the iteration, in "reversed" order. Here, we compose these remarks and show that a restriction of the intuitionistic sequent calculus, LJT, is exactly an accumulator-passing version of intuitionistic natural deduction NJ. More precisely, we obtain this correspondence by applying a series of off-the-shelf program transformations à la Danvy et al. on a type checker for the bidirectional λ-calculus, and get a type checker for the λ-calculus, the proof term assignment of LJT. This functional correspondence revisits the relationship between natural deduction and the sequent calculus by systematically deriving the rules of the latter from the former, and allows to derive new sequent calculus rules from the introduction and elimination rules of new logical connectives.