A Derivational Approach to Calculi, Evaluation, and Abstract Machines

Place:
IT University of Copenhagen
Rued Langgaards Vej
2300 Copenhagen S

Schedule and rooms:

Lecturer:
Olivier Danvy, BRICS, University of Aarhus

To each of the participants: can you send an e-mail to Olivier so that he can give you access to the pdf file of the slides used in the first lecture?

Exercise posted 5 May 2006:

(1) Exercise: Calder mobiles
Consider a binary tree of natural numbers, and compute whether it is well balanced.
Do it in one traversal at most.

(2) Write two versions of the fibonacci function, (a) the usual slow one with two recursive calls and an addition, and (b) a fast one of your
choice.
Then CPS transform them, and defunctionalize the result.
Then analyze the result of defunctionalization.

(3) According to Item 158 of HAKMEM, the following function computes the sinus function:
fun sin (x, epsilon)
= let fun visit x
= if abs x < epsilon
then x
else let val s = visit (x / 3.0)
in 3.0 * s - 4.0 * s * s * s
end
in visit x
end

(a) is this definition lambda-lifted or lambda-dropped? Why? Write the "other'' version (ie, if you think it is lambda-lifted, write the lambda-dropped version, and vice-versa)

(b) justify the correctness of this function;

(c) test how accurate it is compared to the sinus function from the ML math library;

(d) CPS transform it, and defunctionalize the result;

(e) analyze the result of defunctionalization.

Course description:
How does one specify a computation? Some use calculi, the best-known of which is probably the lambda-calculus. Some use abstract
machines, i.e., state-transition systems. Some use evaluation functions, i.e., interpreters. Some use compilers towards some byte
code and virtual machines operating over this byte code.

How does one check that the various semantic artifacts mentioned just above are compatible with each other? For example, how does one
check that a code processor correctly implements a calculus? More generally, how does one _design_ such semantic artifacts?

It is the thesis of this course that in many interesting cases, these semantic artifacts can be derived from each other, and furthermore
that the derivations are based on simple program transformations. A technique called `refocusing' makes it possible to go from one-step
reduction to a pre-abstract machine, and from there to a staged abstract machine and then an eval/apply abstract machine, and under
some conditions to a push/enter machine. Conversely, a combination of simple program transformations (lambda-lifting, closure
conversion, CPS transformation, defunctionalization) makes it possible to mechanically transform interpreters (implementations of
denotational semantics and of big-step operational semantics) into abstract machines (implementations of small-step operational
semantics). The derivational approach makes it possible to relate one-step reduction and evaluation, and to reconstruct known abstract
machines as well as to construct new ones. We will also briefly touch upon compilers and virtual machines.

References:
John Reynolds
"Definitional Interpreters for Higher-Order Programming Languages"
http://www.brics.dk/~hosc/vol11/4-reynolds.html
http://www.brics.dk/~hosc/vol11/4-reynolds2.html

Mads Sig Ager and Olivier Danvy and Jan Midtgaard "A Functional Correspondence between Monadic Evaluators and Abstract Machines for Languages with Computational Effects"
http://www.brics.dk/RS/04/28/ TCS 342(1):149-172 (extended version)

Malgorzata Biernacka and Olivier Danvy "A Syntactic Correspondence between Context-Sensitive Calculi and Abstract Machines"
http://www.brics.dk/RS/05/38/
Accepted for publication in Theoretical Computer Science

Malgorzata Biernacka and Olivier Danvy "A Concrete Framework for Environment Machines"
http://www.brics.dk/RS/06/3/
To appear in ACM Transactions in Compututational Logic

Prerequisites:
A basic knowledge of Standard ML, and having followed a compiler course.

Exam:
Students who wish to get the ECTS credits will have to hand in a report.

Credit:
2.5 ECTS points

Registration:
Please send an e-mail to <ghd@itu.dk> with cc to <hilde@itu.dk> if you want to participate. No later than 2 May 2006

List of participants:
Mikkel Bundgaard, ITU
Søren Debois, ITU
Kristen Nielsen, DIKU
Lars Hartman, DIKU
Søren Sjørup, DIKU
Jeffrey Sarnat, ITU
Adam Poswolsky, ITU
Rasmus Lerchedal, ITU