Technical Faculty Institute of Computer Science and Applied Mathematics Christian-Albrechts-University of Kiel

Computer Organization and Architecture


Werner Kluge, Prof.(em.)

E-Mail: wk@informatik.uni-kiel.de



Major parts of my past research work are outlined in a monograph on Abstract Computing Machines which has been published in the Springer EATCS series (ISBN 3-540-21146-2).
This monograph is on the relationship between basic programming paradigms as they derive from Lambda calculus and the abstract machines featuring the runtime structures and mechanisms that are essential for program execution. It sets out with a brief discussion of an expression-oriented style of programming, addresses the problem of correctly dealing with free variables as a prerequisite for symbolic computations, and gives a brief introduction to Lambda calculus as the underlying theory.
In its main part, the book is primarily concerned with the description of what are called fully normalizing Lambda-calculus machines. They support the runtime structures and mechanisms necessary to correctly perform substitutions that may involve free variables, and to do symbolic self-optimizations under functions (abstractions), thus treating both functions and variables truly as first class objects.
These machines are related to various weakly normalizing counterparts which are the work horses for the implementation of conventional functional languages. They rule out substitution and evaluation under abstractions to avoid problems with free variables, which considerably simplifies the machinery but at the same time also sacrifices many of the amenities of symbolic computations.
Abstract machines for imperative languages are shown to be direct descendants of weakly normalizing Lambda-calculus machines. They permit side-effecting substitutions on an otherwise nearly identical runtime environment which, however, destroy the Church-Rosser property of the Lambda calculus, merely keeping its scoping rules intact.
I used the material contained in this book in various graduate courses on basic concepts of computer organization/architecture; some of the material of the first five chapters I also used in undergraduate courses on function-based programming.

As it so happens when publication deadlines have to be met, the book contains a few errors, many of which are just typos. But it also includes a serious mistake concerning the definition in chapter 5 of the SE(M)CD machine, which I run across while preparing course material for a summer school. A correction of this blunder and also of the typos that have been detected so far can be found under errata

A more recent paper on Abstract Lambda Calculus Machines that is based on material contained in this monograph appeared in the proceedings of the

2nd Central European Functional Programminmg School CEFP 2007
Cluj-Napoca June 23 - 30 2007, LNCS 5161 (2008), pp. 112 -- 157,
It describes two fully normalizing lambda calculus machines which are descendants of weakly normalizing SECD-machines. They both support a nameless lambda calculus that has bound variable occurrences replaced with binding indices. Full normalization is achieved by a few more state transition rules that eta-extend unapplied abstractions to full applications, inserting in ascending order binding indices for missing arguments. Updating these indices in the course of performing full-fledged beta-reductions is accomplished by means of a simple counting mechanism that inflicts very little overhead. The simpler of these machines abides by the concept of saving (and unsaving) on a dump structure machine contexts upon each individual beta-reduction, while the more sophisticated one performs what are called beta-reductions-in-the-large that head-normalize entire spines of beta-redices in the same contexts. It employs an additional trace stack M that facilitates traversing spines in search for and contracting redices.


List of publications

Our research on Lambda-calculus machines led to the implementation of two versions of a fully normalizing applicative order graph reducer called PI-RED. Here is the link to a tar file that contains a directory which includes PI-RED executables that run on Unix/Linux systems. Right now, the contents of this file are a bit messy, a README that explains how these executables need to be installed and used is in preparation.
Werner Kluge
Last modified: August 17, 2009