[Home] [CV] [Publications]


Minus 1a5aa4f1c08b567c9107cba729de26bc87c17ab2b2f690eb45059193a1d6f587 The essence of Rum: A theory of the intensional and extensional aspects of Lisp-type computation
Talcott, C. L. - 1985

Rum is a theory of applicative, side-effect free computations over an algebraic data structure. It goes beyond a theory of functions computed by programs, treating both intensional and extensional aspects of computation. Powerful programming tools such as %functions as values, streams, object-oriented programming, escape mechanisms, and co-routines can be represented. Intensional properties include the number of multiplications executed, the number of context switches, and the maximum stack depth required in a computation. Extensional properties include notions of equality for streams and co-routines and characterization of functionals implementing strategies for searching tree-structured spaces. Precise definitions of informal concepts such as stream and co-routine are given and their mathematical theory is developed. Operations on programs treated include program transformations which introduce functional and control abstractions; a compiling morphism that provides a representation of control abstractions as functional abstractions; and operations that transform intensional properties to extensional properties. The goal is not only to account for programming practice in Lisp, but also to improve practice by providing mathematical tools for developing programs and building programming systems. Rum views computation as a process of generating computation structures – trees for context-independent computations and sequences for context-dependent computations. The recursion theorem gives a fixed-point function that computes computationally minimal fixed points. The context insensitivity theorem says that context-dependent computations are uniformly parameterized by the calling context and that computations in which context dependence is localized can be treated like context-independent computations. Rum machine structure and morphism are introduced to define and prove properties of compilers. The hierarchy of comparison relations on programs ranges from intensional equality to maximum approximation and equivalence relations that are extensional. The fixed-point function computes the least fixed point with respect to the maximum approximation. Comparison relations, combined with the interpretation of programs using computation structures, provide operations on programs both with meanings to preserve and meanings to transform.