Experiments with implementations of two theoretical constructions

Abstract

This paper reports two experiments with implementations of constructions from theoretical computer science. The first one deals with Kleene's and Rogers' second recursion theorems and the second is an implementation of Cook's linear time simulation of two way deterministic pushdown automata (2DPDAs). Both experiments involve the treatment of programs as data objects and their execution by means of interpreters.

For our implementations we have been using a small LISP-like language called Mixwell, originally devised for the partial evaluator MIX used in the second experiment. LISP-like languages are especially suitable since programs are data (S-expressions) so the tedious coding of programs as Gödel numbers so familiar from recursive function theory is completely avoided.

We programmed the constructions in the standard proofs of Kleene's and Rogers' recursion theorems and found (as expected) the programs so constructed to be far too inefficient for practical use. We then designed and implemented a new programming language called Reflect in which Kleene and Rogers “fixed-point” programs can be expressed elegantly and much more efficiently. We have programmed some examples in Reflect in an as yet incomplete attempt to find out for which sort of problems the second recursion theorems are useful program generating tools.

The second experiment concerns an automaton that can solve many non-trivial pattern matching problems. Cook [4] has shown that any 2DPDA can be simulated in linear time by a clever memoization technique. We wrote a simple interpreter to execute 2DPDA programs and an interpreter using Cook's algorithm, and we observed that the latter was indeed much faster on certain language recognition problems. Both have, however, a high computational overhead, since they in effect work by interpretation rather than compilation. In order to alleviate this we applied the principle of partial evaluation, see [5], to specialize each of the two interpreters to fixed 2DPDAs. The result was a substantial speedup.