Lambda calculus : Part 1
Kapil Kapre | Friday, May 15, 2012

If you want to learn functional programming and develop an appreciation for compositional style code, learning lambda calculus is one of the things that would help along the way. The following is an attempt to produce a condensed pre-intro of sorts for non-functional programmers.

Lambda calculus is programming language developed in the 1930s by Alonzo Church. Although originally intended to be used as a functional foundation for Mathematics, it wasn't until the 1960s that scientists saw value in absorbing it into Computer Science. Lambda calculus was later hypothesized to be Turing-machine equivalent. Note that unlike Turing machines lambda calculus isn't concerned with details of the hardware required to perform computations. Thus, what we mean by Turing-machine equivalent is that any computation that can be performed by a Turing machine can be expressed in lambda calculus. The core of the language is a transformation rule and a framework to define and apply 'lambda-functions'.

Lambda calculus consists of names, expressions, functions and applications. Names are identifiers for variables. Here a 'variable' is meant to be seen similar to a function variable in a mathematical function. e.g. ƒ(x) = 10x + 12. Typically lowercase letters are used to denote variables. Functions are defined to perform some work on the input variable and actual work is done when they are applied to some input. Lambda expressions are defined to be composed of names, functions and other expressions. Applications are simply lambda expressions applied to input data. When expressions are evaluated, computation transforming the input to some output as defined by the functions is performed. Thus the core computing operation in lambda calculus is the evaluation of expressions. Lets take a look at how terms in lambda calculus are formally defined.

Terminology:

Function = λ Variable.Expression

Expression = Variable | Function | Application

Application = Expression Expression


Examples of Lambda Functions:


λx.xyz
λ is the specifier that precedes a lambda function definition. Here 'x' is the variable and xyz is the expression in which x is being substituted by whatever input apply the function to. Lets define an expression E = λx.xyz Therefore E 10 would result in 10yz as the output.
λx.(λy.xy)
This is a good place to briefly mention the difference between free and bound variables. For e.g. In the expression λx.xy, x is a bound variable and y is a free variable. Intuitively a variable is bound when you can replace the variable identifier and the expressed computation still remains the same. So for e.g. λx.xy ≡ λt.ty ≡ λm.my. We will go into a bit more detail later on.

Lets define a function M = λy.xy, N = λx.M and application A = Ny. We should keep in mind that the y in M is bound. To make it easier to evaluate mentally, we can swap the variables in M so that M = λt.xt. So Ny evaluates to λt.xt. This elaborates on the point made in the previous example. Whenever you apply an Expression E to a function λx.E′ , we replace all free occurrences of x in E′ with E.

Normalized Lambda-Expression form:

While this isn't a formal term, the meaning is quite intuitive, once explained. When you have nested lambda functions that re-use the same variable name or symbol, it becomes important to differentiate between the intentional and unintentional uses of the same name. For e.g. in λx.(x((λx.x)yz)), the first variable x is not the same as the second variable x, in that, because the variables are bound, they do-not have any meaning outside the limited subset of the expression that the variable acts over. It is recommended to replace λx.x with say λt.t to avoid confusion in more complicated expressions. This is what I mean by normalization.


Closures

You might have heard the term closure in connection with functional programming. To be clear, closures have little to do with functional-programming other than they occur in languages that support first-class functions and allow binding with variables outside their scope. In a nutshell closures are simply functions that make use of variables defined outside their scope. Thus the "closure" is the entire function definition and the lexical environment/scope in which the 'external' (i.e. 'free') variables are defined. One term that is sometimes confused with closures is anonymous functions (or lambdas). Closures are a subset of anonymous functions.