Essence of Rum: A Theory of the Intensional and Extensional Aspects of Lisp-Type Computation

摘要

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 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 includes 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.