題目： “Small-step and Big-step Aspects of Computation (A Walk in the Semantic Park)”
講師：Olivier Danvy氏 (Department of Computer Science, Aarhus University, Denmark)
開催場所：青葉山キャンパス 情報科学研究科棟 2階 大講義室
主査 篠原 歩
- 題目：“Small-step and Big-step Aspects of Computation (A Walk in the Semantic Park)”
- 講師：Olivier Danvy（Department of Computer Science, Aarhus University, Denmark）
- 概要：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.
- 講師略歴：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.