Label-Selective Lambda-Calculi and Transformation Calculi

Abstract. The label-selective lambda-calculus, in its different variants, and its offspring, the transformation calculus, are the results of a research on the role of Currying in the lambda calculus.

Currying is the simple trick by which functions of multiple arguments can be written in the lambda calculus, which is essentialy mono-argument. The idea is to transform a function on a pair, into a function whose result, once applied to its first argument, must be applied to its second one. That is f(a,b) = (f(a))(b).

In our first system, the label-selective lambda-calculus, we give a method to curry starting from a labeled record, in place of a simple pair. The calculus we encode in has to be more complex than simple lambda-calculus, because of these labels, but it appears to keep the quasi totality of its properties. We have of course confluence, and models similar to lambda calculus; and we can apply both simple and polymorphic typings, for which we get strong normalization, as we had with lambda calculus. An immediate application of such a system is to add out-of-order labeled application to curried functional languages, like ML. Since Currying introduces partial applications, we combinatorically augment the number of possible partial applications.

The second extension, which results in the transformation calculus, introduces the idea of a Currying-compliant composition of terms. Classical functional composition is incompatible with Currying, but ours is, by intuitively making multiple connections at once. Again this system is confluent, and we defined typings for it. Selective lambda-calculus is already included, but the new power of this calculus is in viewing arguments as a flow of data, which can be manipulated by composed transformations. It allows one to write imperative algorithms, changing variables, in a purely functional framework. By this it provides a syntactical view on previous works done on the semantics of Algol, and other imperative extensions of functional languages.

Finally we present a third calculus, that of symmetrical transformations, which extends the transformation calculus to n-ary relations. This can give interesting insights on problems like distributed computation or, more mathematically, function inversion.

These three systems are studied from the three points of view of their syntactial properties, their typing, and their semantics.