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.
JG 2011.11.08