Small-step and Big-step Aspects of Computation (A Walk in the Semantic Park)

On the one hand, there are the De Morgan laws: it is clear how to repeatedly apply them to put a proposition in, say, negational normal form, with many small computational steps. On the other hand, such a normal form can be obtained with one big computational step by recursive descent. On the second hand, there is the lambda-calculus: it is clear how to repeatedly apply its contraction rules to put a lambda-term in, say, weak-head normal form, if one exists, with many small computational steps. On the other hand, such a normal form can be obtained with one big computational step by recursive descent. On the third hand, there are also abstract machines: state transition systems that will obligingly yields normal forms as well, if they exist. There is no fourth hand in this talk: our goal is not to monkey with computation, but to demonstrate a profound structural unity in the various styles of semantic artifacts that have been proposed to specify computation: as a calculus with a reduction strategy, as a small-step system of proof rules, as a small-step system of reductions in contexts, as a small-step abstract machine, as a big-step abstract machine, as a continuation-passing big-step evaluation function, and as a direct-style big-step evaluation function. In the course of this talk, we will materialize this unity by using off-the-shelf program transformations to constructively inter-derive semantic artifacts for deterministic sequential programming languages, or, to be precise, their representation as functional programs.

Biosketch: Olivier Danvy is interested in all aspects of programming languages, including programming. His other mother is the Universite Pierre et Marie Curie (aka. Paris VI: PhD, 1986; and Habilitation, 1993) and his other mother in law is Aarhus University (DSc, 2006), where he is currently supervising his 22nd PhD student, Ian Zerny. In his copious spare time, he co-edits the Springer journal Higher-Order and Symbolic Computation with Carolyn Talcott, and is serving as program chair for ICFP 2011.