LISP and Symbolic Computation, 7(1)11-38
Recursion from IterationAndrzej Filinski, School of Computer Science, Carnegie Mellon University, Pittsburgh, PA 15213-3891
|
Abstract: In a simply-typed, call-by-value (CBV) language with
first-class continuations, the usual CBV fixpoint operator can be
defined in terms of a simple, infinitely-looping iteration
primitive. We first consider a natural but flawed definition, based on
exceptions and "iterative deepening" of finite unfoldings, and point
out some of its shortcomings. Then we present the proper construction
using full first-class continuations, with both an informal derivation
and a proof that the behavior of the defined operator faithfully
mimics a "built-in" recursion primitive. In fact, given an additional
uniformity assumption, the construction is a two-sided inverse of the
usual definition of iteration from recursion. Continuing, we show that
the CBV looping primitive is in fact the direct-style equivalent of a
continuation-passing-style fixpoint, and that this correspondence
extends all the way to traditional definitions of these operators in
terms of reflexive types. Keywords: continuations, recursion, iteration, definability, uniformity |
[local copy]
![[picture of journal cover]](../LISP.JPG)