Higher-Order and Symbolic Computation, 13(3)159-160

Editorial

Olivier Danvy and Carolyn Talcott

This issue of HOSC is composed of four contributed articles.

In "Static and Dynamic Program Compilation by Interpreter Specialization," Thibault, Consel, Lawall, Marlet, and Muller report the modern relevance of the first Futamura projection [1]. They present and assess experiments applying a state-of-the-art partial evaluator for C programs, Tempo, to both byte-code and structured-language interpreters, and this both at compile time (for statically loaded code) and at run time (for dynamically loaded code). The results indicate that specializing interpreters can be a competitive method for implementing programming languages.

In "Higher-Order UnCurrying," Hannan and Hicks present a type-based algorithm for uncurrying higher-order programs. They first axiomatize the relationship between curried and uncurried terms and develop a declarative framework for reasoning about uncurrying. They present a practical algorithm, based on algorithm W, generating maximally uncurried forms. This algorithm enables first-class functions to be uncurried, instead of the usual second-class functions as found in typical contemporary compilers for functional languages. The paper also discusses the issues involved in automatically computing uncurried versions of terms based on non-standard type information.

In "Linear-Time Self-Interpretation of the Pure Lambda Calculus," Mogensen shows that a self-interpreter for untyped lambda-terms exists that operates in linear time. He defines a remarkably simple encoding of lambda-terms M |-> [M] and constructs a self-interpreter "selfint" for it such that selfint [M] ->> M if M is in weak head normal form. The self-interpreter is shown to simulate reduction to weak head normal form using only linearly more resources than ordinary reduction, for call-by-name, call-by-value, and call-by-need, and considering various resource measures. The kind of encoding considered here is interesting because one can "edit" encoded lambda-terms: for example there exists a lambda-term "first" such that first [MN] ->> [M]. However, it is not possible to find a lambda-term "F" such that F(MN) ->> M.

In "A Polymorphic Environment Calculus and its Type-Inference Algorithm," Nishizaki formally investigates first-class environments. To this end, he considers the polymorphic environment calculus--a lambda calculus in which environments, represented as explicit substitutions, are first-class values. This calculus enjoys subject reduction and supports (an extension of) ML-style polymorphism, with a type-inference algorithm realizing the accompanying most general type property.

Reference

1. Y. Futamura. Partial evaluation of computation process--An approach to a compiler-compiler. Higher-Order and Symbolic Computation, 12(4) (1999). Reprinted from Systems * Computers * Controls 2(5), 1971.

June 2003 - hosc@brics.dk