lambda calculus and currying


Computable functions are a fundamental concept within computer science and mathematics. The λ-calculus provides a simple semantics for computation, enabling properties of computation to be studied formally. The λ-calculus incorporates two simplifications that make this semantics simple.

One first simplification is that the λ-calculus treats functions "anonymously", without giving them explicit names. For example, the function

\operatorname{sqsum}(x, y) = x \times x + y \times y

can be rewritten in anonymous form as

(x, y) \mapsto x \times x + y \times y

(read as “the pair of x and y is mapped to x \times x + y \times y”). Similarly,

\operatorname{id}(x) = x

can be rewritten in anonymous form as x \mapsto x, where the input is simply mapped to itself.

The second simplification is that the λ-calculus only uses functions of a single input. An ordinary function that requires two inputs, for instance the \operatorname{sqsum} function, can be reworked into an equivalent function that accepts a single input, and as output returns another function, that in turn accepts a single input. For example,

(x, y) \mapsto x \times x + y \times y

can be reworked into

x \mapsto (y \mapsto x \times x + y \times y)

This method, known as currying, transforms a function that takes multiple arguments into a chain of functions each with a single argument.

Function application of the \operatorname{sqsum} function to the arguments (5, 2), yields at once

((x, y) \mapsto x \times x + y \times y)(5, 2)
 = 5 \times 5 + 2 \times 2
 = 29,

whereas evaluation of the curried version requires one more step

((x \mapsto (y \mapsto x \times x + y \times y))(5))(2)
 = (y \mapsto 5 \times 5 + y \times y)(2)
 = 5 \times 5 + 2 \times 2
 = 29

to arrive at the same result.

Subpages (1): Kolmogorov Complexity