January 21st, 2009

eyes black and white

Curry-Howarding evaluation traces

In the conclusion of his article "When Are Two Algorithms the Same?" Yuri Gurevich (who BTW fails to cite Mitch Wand on FEXPR) notes:

In addition to the Curry-Howard correspondence, there is another connection between proofs and computation. If we take an algorithm for computing a function f and we run it on input x obtaining output y, then the record of the computation can be regarded as a proof, in an appropriate formal system, of the equation f (x) = y.

But as Philip Wadler remarks, for each programming language and type system, there is a Curry-(deBruijn)-Howard isomorphism between that language and the proofs of some logic proposition system. The connection that Yuri noticed, and that I incidentally used as the basis for my 1998 mémoire de DEA (~ Master's Thesis), is thus not a wholly novel connection but indeed a particular case of such a generalized Curry-Howard isomorphism, for the type system whereby evaluation trace or tactic T is of type E↓ iff it shows how evaluation of expression E can terminate.

The computational content of the proof that E terminates is a concrete evaluation trace. In the proper framework, an abstract evaluation tactic or strategy may be of type E↓ if it can be reduced to such a concrete evaluation trace in the "type"-directed context of evaluating E. Thus, if you're only considering expressions from a system that has strong normalization properties, then the trivial strategy "reduce wherever you can" has type E↓ for all E in the system, which isn't very informative. If on the other hand you're considering a richer system where termination is not decidable, then you can have informative proofs that include important information on what choices to make at various points of the evaluation attempt. If evaluation of an expression E doesn't terminate, there is indeed no terminating evaluation trace and no computational content. To achieve a full intuitionnistic logic, you can conceivably extend your computation system with expressions such as E→F that terminates iff termination of E implies termination of F, yielding a function that takes an evaluation trace of E as input and output an evaluation trace of the F. Use ⊥ for F and you have the usual negation — and of course, just because E doesn't terminate doesn't necessary imply that E→⊥ terminates, which is the stronger statement that you can actually prove from within the system that E doesn't terminate. Hopefully for your system, evaluating the Gödel sentence Y(G↦G→⊥) won't terminate.

NB: if you're willing to stretch it a bit more, E itself is of type ⊳V iff some trace or tactic shows it evaluates to value V; but then your proof object is trivial and you moved all the intelligence to the opaque evaluation metasystem, which makes the correspondence useless, unlike the previous point of view, that is actually useful in enabling the same tools to do more things (or the same things to be done by fewer tools).