### New draft: Proofs, upside down

#### by Matthias Puech

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.

Pretty cute.

A comment though. The step where you hoist the environment and target type out of the spine is not well justified. You promise at the beginning that you will derive a sequent calculus from a natural deduction using well understood syntactic transformations. However, this particular step (which, is nonetheless essential) seems to require profound understanding of what is actually happening to env and c during the recursive steps. It kind of breaks the promise. That’s a bit of a limitation, but the broader point stands.

Thanks a lot for the comment Arnaud, and, well… touché! I was under the impression that the proper way of explaining this pass is to develop a finer notion defunctionalization, which could be parameterized by some constant arguments (the resulting apply function would have arguments). Since it’s not standard, I preferred to leave it as an extra, unprincipled optimization pass. I think I read Danvy et al. having a similar problem and a resulting “env threading” transformation pass, but I don’t remember where… Maybe it will ring a bell to someone?

Hey Arnaud. If you (or anyone) is interested, there *is* actually a refinment of defunctionalization allowing such constant argument threading: it’s called Lightweight Defunctionalization (see e.g. Banerjee et. al.: Design and correctness of program transformations based on control-flow analysis). I updated the paper, so that the pass Arnaud was rightfully not happy with disappears. Thanks to Olivier and the reviewers of the papers for the pointer!

[…] My previous draft, Proofs, upside down was accepted for presentation at APLAS 2013. See you in […]