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