| The book addresses ways and means of organizing computations, highlighting the relationship between algorithms and the basic mechanisms and runtime structures necessary to execute them using machines. It completely abstracts from concrete programming languages and machine architectures, taking instead the lambda calculus as the basic programming and program execution model to design various abstract machines for its correct implementation. The emphasis is on fully normalizing machines based on a full-fledged beta-reduction as an essential prerequisite for symbolic computations that treat functions and variables truly as first-class objects. Their weakly normalizing counterparts are shown to be functional abstract machines that sacrifice the flavors of full beta-reductions for decidedly simpler runtime structures and improved runtime efficiency. Further downgrading of the lambda calculus leads to classical imperative (von Neumann) machines that permit side-effecting operations on the runtime environment.
This monograph looks at computer organization from a strictly conceptual point of view to identify the very basic mechanisms and runtime structures necessary to perform algorithmically specified computations. It completely abstracts from concrete programming languages and machine architectures, taking the λ-calculus – a theory of computable functions – as the basic programming and program execution model. In its simplest form, the λ-calculus talks about expressions that are constructed from just three syntactical figures – variables, functions (in this context called abstractions) and applications (of operator to operand expressions) – and about a single transformation rule that governs the substition of variable occurrences in expressions by other expressions. This β-reduction rule contains in a nutshell the whole story about computing, specifically about the role of variables and variable scoping in this game.
Different implementations of the β-reduction rule in conjunction with strategies that define the sequencing of β-reductions in complex expressions give rise to a variety of abstract λ-calculus machines that are studied in this text. These machines share, in one way or another, the components of Landin’s secd machine – a program text to be executed, a runtime environment that holds delayed substitutions, a value stack, and a dump stack for return continuations – but differ with respect to the internal representation of λ-expressions, specifically abstractions, the structure of the runtime environments and the mechanisms of program execution. |
