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 postscript versions of this paper: a4 size and letter size.
JG 94.5.3