Notes on Lambda Calculus

copyright Gunnar Gotshalks

(lightly edited by P. Roosen-Runge, September 25 2005)

The 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 λ calculus. A fundamental goal was to describe a means of defining what can be computed. The full definition of λ calculus is equivalent in computing power to a Turing machine. Turing machines and the λ calculus are alternate descriptions of our understanding of what is computable.

The basis for λ 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 λ calculus. Lisp is an implementation of λ 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.

The 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.

  1. (u+1)(u+2) is denoted by the following where it is explicitly stated that u is bound within the definition.
            (λ u . (u+1)(u+2))
                   ^^^  ^^^^^^^^^^
       bound variables   defining form
    
  2. (u+a)(u+b) is denoted by (λ 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 λ 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. {λ u . (u+1)(u+2)}[3] ==> (3+1)(3+2) ==> 20

  2. {λ 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.
    {λ 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 {λ u . u/(u+5)} [ {λ a . a(a+1)} [ 7-3 ] ]

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

What is interesting and extremely important about λ 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 {λ f . f(3) + f(5)} [ {λ a . {λ 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.
     {λ f . f(3) + f(5)} [ {λ a . {λ x . ax(a+x)}} [7-3] ]
      ==> {λ f . f(3) + f(5)} [ {λ x . 4x(4+x)} ]
      ==> {λ x . 4x(4+x)}(3) + {λ 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 λ expression.

        {label name (λ 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 {λ x . {λ y . x**2 - y**2} [2] } [3]

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

  3. Write the following as a λ 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.