Codementor Events

On Lambda Calculus

Published Sep 29, 2019

Lambda calculus is a simple language for expressions that supports the focused study of functions and their invocations.  It is less a programming language in the sense we know today, and more of a mathematical form: it is based on written text, and, it provides for several manipulations of the text.

Syntactic Constructs

Here are the three syntatic constructs of lambda calculus:

Name of Syntatic Construct Example
Variable x
Abstraction ( λ x . M )
Application ( M N )

In the above descriptions, we take M and N as sub expresssions, which can be any of the above forms.

Variables

Variables can have any name, but are typically single letters like x, y and sometimes ⨍ to indicate a variable that is taken as a function.

Abstraction

The abstraction form lets us define functions.  In lambda calculus, an abstraction (a function) takes one parameter — the x in ( λ x . M ) and has a body — the MM is any possible expression in lambda calculus.

Application

The application form goes to the opposite of abstraction.  In application, we provide a value for a parameter of a function — the value can be any lambda expression we can write.  Application just provides a parameter value; it does not automatically "invoke" the function as we might expect in C (that is done later).

Manipulations

There are two manipulation operations provided by lambda calculus; they manipulate lambda expressions  These are not themselves syntactic constructs, but rather transformations of equivalence — meaning that if you properly use an operation on a given expression, the resulting expression is equivalent!

So that we can talk about the steps of transformation in working with lambda calculus, the tranformations themselves have a written form — but to be clear, the written forms of these operations are not themselves lambda calculus syntax, though once a described (written) transformation is actually performed (using textual replacement), the result is once again a legal lambda calculus construction.

Operation Name Transformation Input Transformation Output Purpose
𝞪—conversion ( λ x . M[x] ) ( λ y . M[y] ) rename parameter
𝞫—reduction ( (λx. M) N ) ( M[x:=N] ) simplification

𝞪—conversion (alph conversion)

This operation is used to remove variable name conflicts.  It says that two abstractions are equivalent: one using some variable name, e.g. x, as parameter and within body M (e.g. some M in terms of variable x, written as M[x]), and another another using another variable name, e.g. y, though otherwise with the exact same M (e.g. M[y]).

𝞫—reduction (beta reduction)

This operation is used to simplify application applied to abstraction.  In some sense, an application can cancel out an abstraction (by providing a value for the parameter).  Thus, we have two equivalent expressions: one with application to an abstraction, and one where the application and abstraction pair were eliminated.  In order to have the equivalence, the latter must have the same M except with N (the supplied parameter) substituted for parameter variable x in M, written as M[x:=N].

Discussions

Application, on its own, brings together two lamba expressions, a function and a parameter value — it does not automatically invoke or execute the function.  Technically, the application construct does not even require the first of the two lambda expressions to be an abstraction construct — however, if it is, we can perform 𝞫—reduction, which allows us to remove the both the application and the abstraction, thus, eliminating the abstraction's parameter by substitution of the application-provided parameter value within the abstraction body, and that as a result we have two equivalent expressions: the former application to abstraction, and the latter, what remains after an application and an abstraction pair are eliminated.

We can define the verb "to abstract" with the following: take an expression, and replace some fixed part of it with a variable — then wrap it in a function that takes the variable as a parameter.  For the equivalent in the C programming language, let's imagine the statement
    printf ( "%d", 100 );
Now, to abstract this, we might replace the 100 with x, and then wrap that in a function:
   int printx ( int x ) { printf ( "%d", x ); };
We have "abstracted" our original printf statement!

Expressions, including variables, have no particular type, or rather are simply typed: all variables and expressions are all taken as the following type: function — taking one argument — and returning an expression (whose type is also function taking one argument).

Abstractions (i.e.functions) are anonymous — they are not named and thus cannot be referred to or invoked by name.  However, they are first class in the sense that they can both be applied to (passed as) parameters as well as be the result of (return value) of functions.  This makes lambda calculus a higher order system, and this where its power to study functions comes from.

A variable seen alone is called an unbound variable.  This equates to the notion of global variable in programming languages, like C, and to static in languages like Java and C#.  (Unlike C where a global must be declared, though, unbound variables are not declared, they are merely used.)

The abstraction construct introduces a lexical scope for the parameter variable.  A scope is a section of text in which variables need to be understood as to whether they are bound or unbound.  Within the body of the abstraction, an occurance of the parameter of the abstraction is called a bound variable, and this equates to the concept of a formal parameter in a function or method in C, Java, and C#.  The parameter introduced by the abstraction construct can only be referred to within the scope of the abstraction, e.g. within the abstraction body (M).  (Past the body of abstraction, the parameter is no longer in scope!)

Scope introduces the possibility for variable name conflicts!  The same variable name may be bound to one function, or to another, or be unbound — hence, we must be aware of scope, and, during manipulation of expressions, we might have to rename variables (using 𝞪—conversion) to avoid naming conflicts and keep the expressions we're working with as being equivalent, i.e. having the same meaning!  If we fall prey to a naming conflict during a transformation, the resulting expression is will not be equivalent to the former, which makes the transformation erroneous.

The lambda calculus abstraction construct allows for exactly one parameter.  If we want to make a function that takes two parameters, we nest one abstraction construct within another:
    ( λ x . ( λ y . (x y) ) )
This says that we have a function that takes x as a parameter, and the body of the function is another function that takes y as a parameter.  Let's note that the use of x within the body of the nested, inner abstraction refers to the x introduced by the outer abstraction. 

Just as one abstraction only allows a single parameter, one application only provides a single parameter value.  Just as we need to use two abstractions (one nested within the other) for the idea of a two-parameter function, we need to use two applications (one nested within the other) for the idea of a two-parameter function call.  In lambda calculus, because of this nesting, there is an intermediate form, in which only one of the parameters is provided.  In those terms, the applying once (using application once) to the outer function returns the inner function, though of course, with the parameter substituted.

Let's apply to this nested function:
    ( ( λ x . ( λ y . (x y) ) ) y)
Here, the final y is an unbound variable, whereas the preceeding ys are bound.  We can see the beginnings of a name conflict here.  Let's do 𝞫—reduction, and see what happens.  First, let's recall that the reduction works when we have application applied to abstraction of the form:   ( (λx. M) N )
Here, M is ( λ y . (x y) ), and N is the unbound variable y, so the beta reduction of
M[x:=N] is ( λ y . (x y) )[x:=y], which is: ( ( λ y . (y y) ) — yet this is incorrect because in this expression, all ys are bound, while one of the y should be not be bound (it should refer to the unbound (global) y).  We accidentally converted an unbound y into a bound y, and the result not equivalent.  When we perform beta reduction, we need to first check if this can happen: if we would change the binding of a variable, as this is improper to do.  If this would happen, then we first use 𝞪—conversion, to rename the abstraction's variable and any uses within its body, here M is ( λ y . (x y) ) we will rename y to z, so now M is ( λ z . (x z) ) .  Now, we can introduce the unbound y into this in place of x so that
M[x:=N] is ( λ z . (x z) )[x:=y], which results in the proper equivalent expression:
    ( ( λ z . (y z) ) , in which the y remains unbound.


Technically speaking, the parenthesis are not optional in lambda calculus — they are a required part of the various syntactic constructs.  However, if we see similar to the above without parenthesis as in:
    λ x . λ y . x y
no matter how complex M is, I believe that we should take it as this as:
    ( λ x . ( λ y . (x y) ) )
rather than as:
    ( λ x . ( λ y . x ) y)
because if that was intended, parenthesis would absolutely have been required to separate the part of the expression into one abstraction and the rest for the other.

Similarly, if we have
    x y z
It is ambiguous, and technically invalid lambda calculus, though if we have to work with it we should take that as ( ( x y ) z ) rather than ( x ( y z ) )

Lambda calculus does not even define numbers or other numeric operations, such as addition; however, it is popular to pretend they are available.  Numbers, and numeric operations like addition, can indeed be represented in the minimal lambda calculus, so it is reasonable to extend the calculus with numeric constants and operators.

Discover and read more posts from Erik Eidt
get started