HR F#: Lambda Calculus - Reductions #1

The Lambda Calculus - Reductions #1 is rather unusual. Instead of submitting the code, the required submission is a shortening of the lambda-expression.

Reduce the following expression to no more than one term. ... ((λx.(x y))(λz.z))

There is a nice introduction to the lambda-calculus: A Tutorial Introduction to the Lambda Calculus. Some relevant excerpts from it:

  • <expression> := <name> | <function> | <application>
  • <function> := λ <name>.<expression>
  • <application> := <expression><expression>
  • An example of a function is the following: λx.x. This expression defines the identity function.
  • Functions can be applied to expressions. An example of an application is
  • In λ calculus all names are local to definitions. ... A name
    not preceded by a λ is called a “free variable”.

In programming language terms, the λ is a keyword defining a function. It is followed by the list of arguments and then the function body, separated by dot. The "free" variable is just defined somewhere else and available in the current scope.

So the expression "((λx.(x y))(λz.z))" can be rewritten as following (I will give examples in JS and F# programming languages):

// JavaScript
((x) => (x(y)))((z) => z)

// F#
(fun x -> x y)(fun z -> z)

(fun z -> z) is just an identity function. The entire expression is an application of the function that applies its argument to value with identity function as argument. So the expression returns y and it is the right answer.