Notes on Lambda Calculus

copyright Gunnar Gotshalks

Last updated 1999 March 23

Lambda calculus was developed by Alonso Church during the 1930's and 40's. During mid to late 1950's John McCarthy developed the programming language Lisp; a LISt Processing language based on lambda calculus. A fundamental goal was to describe a means of defining what can be computed. The full definition of lambda calculus is equivalent in computing power to a Turing machine. Turing machines and lambda calculus are alternate descriptions of our understanding of what is computable.

The basis for lambda calculus is a mathematical theory and notation for 'anonymous' functions -- functions that have not been bound to names. What is presented here is a subset of the full definition to present the flavour of lambda calculus. Lisp is an implementation of lambda calculus that includes syntactic sugar -- functions and forms that do not add to the power of what we can compute but make the descriptions simpler and easier to understand.

Lambda calculus is a notation and interpretation scheme that clearly defines functions and their application to operands -- argument-parameter binding. It also clearly indicates which variables are free and which are bound.

A bound variable is similar to a local variable or parameter of a function. Changing the name of a bound variable (consistently throughout a function) will not change the meaning of the function.

A free variable is similar to a global variable in a function. It is "bound" by the enclosing environments (functions). Changing a free name within a function will normally change the meaning of the function. In the following the Greek lower case character is substituted for lambda when handwritten or using symbolic fonts.

  1. (u+1)(u+2) is denoted by the following where it is explicitly stated that u is bound within the definition.
            (lambda u . (u+1)(u+2))
                   ^^^  ^^^^^^^^^^
       bound variables   defining form
    
  2. (u+a)(u+b) is denoted by (lambda u . (u+a)(u+b))

    u is bound within the definition, but a and b are free (they are defined by an enclosing context.

Functions are applied to arguments in a list immediately following the lambda expression. Different types of parenthesis can be used to make it easier to read the expression. Other than visual impact, it doesn't matter which type of parenthesis is used, provided they are correctly matched.

  1. {lambda u . (u+1)(u+2)}[3] ==> (3+1)(3+2) ==> 20

  2. {lambda u . (u+a)(u+b)}[7-1] ==> (6+a)(6+b) and no further in this context

  3. We can pass expressions to a variable.
    {lambda u, v . (u-v)(u+v)}[ 2p+q , 2p - q ] ==> ((2p+q)-(2p-q))((2p+q)+(2p-q))

One builds up longer expressions using nested auxiliary definitions.

    Define  u/(u+5)
        where u = a(a+1)
             where a = 7-3
Is defined with {lambda u . u/(u+5)} [ {lambda a . a(a+1)} [ 7-3 ] ]

Arguments are evaluated first.
      {lambda u . u/(u+5)} [ {lambda a . a(a+1)} [ 7-3 ] ]
      ==> {lambda u . u/(u+5)} [ 4(4+1) ] ==> {lambda u . u/(u+5)} [ 20 ]
      ==> 20 / (20 + 5) ==> 0.8

What is interesting and extremely important about lambda calculus is that function names are also variables. After all we need to have a definition to associate with them. The following is an example of using auxiliary definitions to assign a meaning to a function name.

    Define f(3) + f(5)
        where f(x) = ax(a+x)
            where a = 7-3
Is defined with {lambda f . f(3) + f(5)} [ {lambda a . {lambda x . ax(a+x)}} [7-3] ]

Working from the inside out, and right to left as arguments must be evaluated first, we get the following.
     {lambda f . f(3) + f(5)} [ {lambda a . {lambda x . ax(a+x)}} [7-3] ]
      ==> {lambda f . f(3) + f(5)} [ {lambda x . 4x(4+x)} ]
      ==> {lamda x . 4x(4+x)}(3) + {lambda x . 4x(4+x)}(5)
      ==> 4*3(4+3) + 4*5(4+5) ==> 12*7 + 20*9 ==> 364

We can have recursion by using labels to temporarily name a function. The general template is the following. The name is in scope within the entire body but is out of scope outside of the lambda expression.

        {label name (lambda arguments . ... body references name ... }

In Lisp we can use labels to define a mutually recursive set of functions. A general template is the following.

   (labels ( list of "named" lambda-like expressions )
           sequence of forms using the temporarily named functions
   )

For example a recursive multiply function that uses only addition. The temporary function is called mult.

    (eval  '(labels ((mult (k n)
                           (cond ((zerop n) 0)
                                 (t (+ k (mult k (1- n))))
                            )
                    ))
                    (mult 2 3)   ; in this case a single form using mult
            )
    )

The following is a function rec-times -- it computes k*n -- that supplies the parameters to a unary function that is a recursive variation of the above. Notice the form (temp n) is within the labels section.

    (defun rec-times (k n)
            (labels ((temp (n) (cond ((zerop n) 0)
                                     (t (+ k (temp (1- n)))))
                    ))
                    (temp n)
         )
    )

Exercises

  1. Evaluate {lambda x . {lambda y . x**2 - y**2} [2] } [3]

  2. Evaluate {lambda p,q . {lambda u,v . u**2 + v**2} [ p+q , p-q ]} [0,1]

  3. Write the following as a lambda expression.
       f(u(1)) + f(v(2))
         where u(x) = a+x**2  and  v(x) = b-x**2
            where a = (1+z)**2  and b = (1-z)**2
    

  4. Translate each of the above to a lambda expression in Lisp and evaluate them.