Prof. Olivier Danvy Lecture at NII Logic Seminar
Date: December 16, 2010, 14:00--16:00
Place: National Institute of Informatics, Room 2005 (20th floor) 場所: 国立情報学研究所 20階 2005室 (半蔵門線,都営地下鉄三田線・新宿線 神保町駅または東西線 竹橋駅より徒歩5分) (地図 http://www.nii.ac.jp/introduce/access1-j.shtml)
Speaker: Prof. Olivier Danvy (University of Aarhus)
Title: Small-step and Big-step Aspects of Computation (A Walk in the Semantic Park)
Abstract: 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.
問合せ先: 龍田 真 (国立情報学研究所) e-mail: [email protected] http://research.nii.ac.jp/~tatsuta