The Transformation Calculus

Jacques Garrigue. In Proceedings of the 15th Conference on Foundations of Software Technology and Theoretical Computer Science. Bangalore, India, December 1995. Spring-Verlag LNCS 1026.
Also RIMS Preprint 1042, Research Institute for Mathematical Sciences, Kyoto University, October 1995.

Abstract. The lambda-calculus, by its ability to express any computable function, is theoretically able to represent any algorithm. However, notwithstanding their equivalence in expressiveness, it is not so easy to find a natural translation for algorithms described in an imperative way.

The transformation calculus, a conservative extension of lambda-calculus, corrects this flaw by re-introducing an implicit notion of state in the calculus. This is essentially done by combining two features, selective currying permitting an explicit naming of arguments, like was done in selective \lbd-calculus, and the possibility of composing terms, to express an imperative order in operations.

Particularly we show how these features permit to express scope-free variables, which can be used roughly like classical mutable ones, without explicit handling of a state between the operations implying them.

This calculus stays very close to lambda-calculus, and keeps most of its properties. We prove here its confluence.

You can get the electronic versions of the report (longer, DVI and PDF files), and the conference paper (shorter, A4 and letter Postscript, and A4 PDF files).

JG 2011.11.08