Lambda calculus as described above seems to permit functions of a single variable only.
However, many useful functions, such as binary arithmetic operations, require more than one parameter; for example, sum(a,b) = a+b matches the
syntactic specification sum: N×N→N, where N denotes the natural numbers.
Lambda calculus admits two solutions to this problem:
- Allow ordered pairs as lambda expressions, say using the notation
<x,y>, and define the addition function on pairs:
sum <a, b> = a + b
- Another method is Currying, which is the technique of transforming a function that takes multiple arguments in such a way that it can be called as a chain of functions each with a single argument.
The notion of Currying allows for functions of several variables to be interpreted simply as functions of a single variable returning functions of the remaining variables.
Use the curried version of the function with the property that arguments are supplied one at a time:
add: N → N → N
≡ add: N → ( N → N ) (→ associates to the right)
where add a b = a + b.
An application of add has the form add a b, and is equivalent to (add a) b, since function application associates to the left.
In other words, applying add to one argument yields a new function which is then applied to the second argument.
Now (add a): N→N is a function with the property that ((add a) b) = a + b.
Using add, we can define inc:
inc = add 1