Higher-Order and Symbolic Computation, 12(2)123-124

Introduction

Olivier Danvy and Carolyn Talcott

While the continuation-passing style (CPS) transformation is reasonably well understood for untyped and for simply typed lambdaterms, what about dependently typed lambdaterms? In their article, Gilles Barthe, John Hatcliff, and Morten Heine Sørensen investigate this issue for pure type systems. Their article is a thoroughly extended version of the one presented at the second ACM Workshop on Continuations (CW'97). Time proved too short to publish it in our special issue on continuations 11(4) and 12(1), but here it is now.

In his article Computing with Contexts, Ian Mason studies a special case of Talcott's binding structures using named variables. This work addresses the challenging problem in higher-order computation of symbolic evaluation of expressions containing binding constructs, that is of computing with contexts--expressions with place holders for missing information. The challenge is representing contexts in a manner that allows computation rules to be applied to contexts (especially those involving substitution for a bound variable) so that computing commutes with filling in missing information (except when that information is needed for the computation step). With such a representation, contexts can be used to elegantly express computation rules and other program transformations, as well as for defining and reasoning about program equivalence. Mason begins by illustrating the problems that arise with traditional lambda-calculus contexts, and proposes an alternative based on holes decorated with substitutions. He then studies alternative notions of substitution and hole filling giving a number of helpful examples to illustrate the distinctions and subtleties. He shows that among the alternatives considered there is a unique choice of notions of substitution and hole filling for which the desired commuting diagram property holds in general. Finally Mason considers options for expressing the beta-reduction rule in terms of operations on contexts. Again he shows that only one choice has the desired properties. Using this as the foundation, he shows how symbolic computation rules can be defined for a variety of lambda-languages using call-by-name or call-by-value and including imperative primitives such as reference cells and control abstractions.

The Euclidian algorithm has long been a little challenge for partial evaluation: indeed it does not fit the usual computational pattern where a function can be unfolded given a static value for its induction variable. This has made the gcd function relatively elusive to specialize. This specialization seems to have been first achieved based on an outside property of the number of iterations of the Euclidian algorithm [1]. Instead, in his article, Chin-Soon Lee achieves this specialization by elegantly using the standard partial-evaluation toolbox, ending up with a traditional tabulation solution. We take the opportunity of this publication to encourage members of the partial-evaluation community to tackle such simple but challenging applications of partial evaluation and to consider HOSC's columns to report their findings.

Reference

1. Danvy, Olivier and Goldberg, Mayer. Partial evaluation of the Euclidian algorithm. Lisp and Symbolic Computation, 10(2):101-111, 1997.

June 2003 - hosc@brics.dk