Computability Theory Of and With
the Scheme Programming Language
Albert Meyer
There remains a gulf between computation models like Turing machines that appear in theory of computation texts, and introductory programming languages. The simple and powerful Scheme programming language, used in hundreds of introductory programming courses, is a plausible candidate for bridging this divide.
At MIT, we teach informally how Scheme works, initially using a "Substitution Model" for functional procedures, followed by an "Environment Model" to explain assignment commands. Key language properties such as "Scheme procedures are black boxes" and "Scheme has no parallelism" are illustrated by example.
It is possible to formulate a "Substitution" model for a significant part of the Scheme programming language, including assignment statements (the SET! special form), and control abstractions (ERROR, CALL-WITH-CURRENT-CONTINUATION). The behavior of each Scheme special form is defined by two or three rules for rewriting Scheme expressions to Scheme expressions. This provides a Scheme model that is rigorous, intuitive, and accurate.
The model offers a solid theoretical basis for an introductory programming course, and allows ideas like "black-box" procedures to be mathematically defined, and verified, quite simply. It also legitimizes the use of Scheme in a computability course, providing a far more convenient model than Turing machines. Yet it remains debatable whether the model should be in the curriculum of an introductory programming course, and whether "real" Scheme should be used in teaching computability theory.
Short Biography:
Albert R. Meyer is the Hitachi America Professor of Engineering in the MIT Department of Electrical Engineering and Computer Science.
Prof. Meyer got his BA, SM, and PhD degrees from Harvard University. His first faculty appointment was at Carnegie Mellon University in 1967. He has been a member of the MIT faculty since 1969, with visiting appointments at U. Warwick, UC Berkeley, Harvard, ETH Zurich, U. Chicago, and IBM Watson Research Center. He has served as Associate Director of the MIT Lab. for Computer Science and Chairman of the MIT Computer Science Graduate Program.
His research contributions span many areas of theoretical Computer Science. In computational complexity theory, he formulated the Polynomial Time Hierarchy and presented the first examples of exponentially complex problems. In automata theory, he laid the foundations for the modern proof of the Algebraic Decomposition Theorem for finite automata. In programming language theory, he made seminal contributions to the development of Dynamic Logic, Second-order Type Theory, and Concurrent Process Theory.
Prof. Meyer is a Fellow of the American Academy of Arts and Sciences and a Fellow of the ACM. He has been Editor-in-chief of Information and Computation, a leading journal of theoretical Computer Science, since 1982. He has supervised two dozen Ph.D.students now on faculties at over a dozen leading universities and industrial research labs.
Homepage: http://theory.lcs.mit.edu/~meyer/