Label-selective lambda-calculi and transformation calculi
Jacques Garrigue · 1995
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 la...