Functional Programming
12. The Extended Untyped lambda Calculus



12.1 The Untyped lambda Calculus

The untyped lambda calculus is a very simple yet powerful computation model. This version of the lambda calculus is referred to as untyped lambda calculus because variables can be bound to any kind of value, and functions can be applied to any kind of arguments (although they might not compute anything useful). This is in contrast to typed lambda calculus variants where a thing can be placed in only those contexts which match its type.

We are going to look at a slightly extended variant, which is no more powerful, but is more convenient to use. In this variant we will have some basic kinds of atomic values (integers and Booleans), lists, and some operations on these values. (Which, that means that we are not really purely untyped.)

The basic lambda notation consists of lambda abstractions which construct functions, and application which applies functions to arguments.

A lambda calculus term or lambda calculus expression is a well formed combination of abstractions and applications. Evaluating a term is done by rewriting the application of abstractions to arguments until no further rewriting is possible (the rewriting need not terminate). In the pure lambda calculus, there are no data values. Things like the natural numbers, strings, lists, etc. are constructed from just abstraction and application.

This is a very informal treatment, just to get you thinking about the functional style of computation. We are playing fast and loose with things like when a term is evaluated (i.e. given a value), scope of identifiers, atomic data values, and so on. We will be more precise when we get to the Haskell language.

The λ-calculus syntax is very simple. We start with a possibly infinite set of constants C, which are the atomic building blocks of our expressions. The typical constants we think of are number representations, like 0, 1, 2, 3, ..., operations like +, -, predicates like = and !=, characters and string manipulation primitives, and so on. The constants are usually chosen to model some kind of computation: operations on integers, string manipulation, trees, lists, etc.

We also have a infinite set of variables V which are names that appear in expressions. Unlike the constants, these names have no meaning on their own.

We first need to define the syntax of lambda expression. The set of all possible lambda expressions is defined as follows,

  1. Atomic Expression: Any constant from C or identifier from V is an expression.

  2. Function Definition (Lambda Abstraction): If e is an expression, and v is a free variable in e, then (λ v . e) is an expression (a function definition). Lambda abstraction introduces Suppose T1 is the set of possible values for v, and T2 is the set of possible values for expression e. (Call T1 and T2 types if you wish). Then we can write that
    (λ v . e): T1 -> T2
    meaning that the lambda expression is a function from T1 to T2.

  3. Function Application: If e1 and e2 are expressions, then (e1 e2) is an expression (a function application).
For convenience, outer parentheses can be removed. In the absence of parentheses, application associates to the left, and function application has higher precedence than definition. So for example,
(e1 e2 e3) means ((e1 e2) e3)
and
λ v . e1 e2 means (λ v.(e1 e2))


In the above definition we used the term free to refer to occurrences of a variable appearing in an expression. This must be made more precise. Note that the different occurrences of a variable v in an expression can be free, or be bound to different lambda expressions. For example, in
(x (λ x . (λ x. (f x)) (x x) ) )
The first occurrence of x is free; the second occurrence of x, in (f x), is bound to the second λ; and the third and fourth occurrences of x , in (x x), are bound to the first λ.

Note how we do not count the appearance of x in a λ (the x before the . marker) as an occurrence. It is part of the λ, as in "bind x in this e".

Evaluation of λ-calculus expressions is defined by syntactic substitution of an expression into free occurrences of a variable. In doing this substitution, it is important that variable bindings do not inadvertently change. For example, in this expression
λ v . (v w)
if we substitute the variable x for the free w, we get
λ v . (v x)
in which the new x plays the same role as the old w, that is, it remains free. But if we substitue the variable v for the free w, we get
λ v . (v v)
In which case the v we just substituted gets bound to the λ, and it no longer free. This has changed the expression in a fundamental way.

We also want to be able to substitute entire expressions for free variable occurrences, for example we might want to substitute (x w) for w in our original expression, to get
λ v . (v (x w))
Again, we need to be careful about accidental re-binding.

This leads us to the notion of proper substitution defined by these rules. The notation
[v → s] e
means substitute all free occurrences of variable v in expression e by the expression s.

Let v, w, u all be distinct variables (i.e. they have different names).

  1. If an expression is a single variable then That is, variable v gets replaced by expression s, and if there is no v then no replacement occurs.

  2. If the expression is λ v . e then

  3. If the expression is function application (e1 e2) then we substitute into both
We can now finally define the semantics of lambda calculus in terms of rewrite rules. These rules are invertible, letting the left hand side be replaced by the right hand side, and vice-versa.

12.2 Evaluation Strategies

An evaluation strategy is a set of rules for evaluating expressions. Evaluation strategies are important in expressions, for example (1-x)(1+x) when x is very close to 1 might be better evaluated as 1-2x-x*x. Where evaluation strategies are important, say in numerical computation, we need to know a lot about how the compiler works.

In a functional language, evaluation strategies focus on how the function applications are processed. An evaluation strategy asnwers the questions: What order are the arguments evaluated? When are they evaluated? What form does evaluation take?

Because there are no side-effects in a pure functional language, evaluation takes the form of rewriting expressions using the conversion rules to reduce the expression to be as "small" as possible.

Applicative order means to evaulate the arguments of a function application in left-to-right order, exactly as you would do if you were required to Curry the function.

When we compute a function we usually assume that all arguments have a value before the function evaluation begins. Strict (or eager) evaluation means to evaluate all the arguments to a function before evaluating the function. Applicative order evaluation is strict. But not all strict evaluation need be in applicative order.

In non-strict evaluation arguments need not be evaluated until they are actually required. Lazy evaluation is a form of non-strict evaluation in which arguments are not evaluated until required.

A computation that does not terminate under strict evaluation, can terminate under lazy evaluation. For example, the function that produces an infinite list of integers that is then used in a function that only requires the first 3 elements of the list.

In the λ-calculus, all reduction orders that terminate give the same result. That is, the λ-calculus is confluent, or has the Church-Rosser property. What this means is that changing the evaluation strategy only changes whether the program terminates or not, not the final result of the computation. The invariance of the final result of a terminating computation clearly need not hold in the case when we have side-effects.

Note: Scheme is dynamically typed. It's data has types (like integer and string), it's just that the types of arguments to functions are not generally known at compile time, only at evaluation time.

12.3 Y-combinator - What About Recursive Definitions?

At this point in our development of restricted Scheme we have that the only things we need for computation seem to be abstraction, application, and definition. We can build machinery, in principle, for the logical operations, and the variable number of arguments in things like and need a bit of work, but that is just more of the same programming.

Simple definitions (non-recursive) and quoting are convenient but not essential (barring the issue of side effects). The one thing that is not so clear is definitions that are self-referential, or recursive. If we can get rid of these, then all computation is essentially abstraction, application, and define and use of abbreviations. code/LambdaScheme/YCombinator.rkt

    #lang racket
     
    ; The applicative-order Y combinator
    ;
    ; Or how to define a recursive function without giving it a name
    ; before the definition is complete.
    ;
    ; One notion of "definition" is that of an abbreviation.  I.e. a
    ; a shorthand name for a piece of text.  When used, the name is simply
    ; expanded into the text it stands for.  Many languages call these
    ; macros. In general, an abbreviation is not supposed to be
    ; circular, so that a sequence of substitutions (aka macro expansions)
    ; always terminates in a constant number of steps.  
    ;
    ; If an abbreviation is a term that does not create side effects, then
    ; abbreviations can be replaced by their values.  For example, a lambda
    ; term with no free variables can be abbreviated:
     
    (define g  (lambda (x) (+ x 1)))
     
    (g (g 2)) 
    ; is the same as 
    ( (lambda (x) (+ x 1)) ((lambda (x) (+ x 1)) 2))
     
    ; But a recursive definition is different.  For example
    ; here is a typical recursive definition of f in terms of itself.  
     
    (define f 
      (lambda (x) 
        (if (> 0 x) x (f (- x 2)))
        )
      )
      
    ; Simple text substitution is not going to terminate, and furthermore
    ; we are using f before it is actually defined.  That is, f is a free
    ; term inside the text that is being used to define f.
     
    ; Of course, Scheme is perfectly happy with this:
     
    (f 2)
     
    ; and we are now going to explain why.
     
    ; Let's change our defintion a bit, so that the identifier f is bound
    ; inside the defining term:
     
    (lambda (f)
      (lambda (x) 
        (if (> 0 x) x (f (- x 2)))
        )
      )
     
    ; so now there are no free variable in the defining term.  
    ; But this thing we just defined is not f, it is the
    ; function that builds f when given f!
     
    ; (define f-builder
    ;  (lambda (f)
    ;    (lambda (x) 
    ;      (if (> 0 x) x (f (- x 2)))
    ;      )
    ;    )
    ;  )
     
    ; The function f is this:  
    ;    (f-builder f).  
    ; But we don't have f!  We need to build it.  
    ; So f is this:
    ;    (f-builder (f-builder f))
    ; That is (f-builder (f-builder (f-builder (..... f))))
    ; Arrg!!!  It doesn't look like we have accomplished anything.
     
    ; But in fact we have.  Because now we can defer some of the definition of
    ; f to run time (evaluation time).  Getting something like this
     
    ; (define f
    ;  (lambda (x) 
    ;    (if (> 0 x) x ((f-builder ?) (- x 2)))
    ;    )
    ;  )
     
    ; This new defintion has no free variables (after substituing f-builder)
    ; except is does have the unknown term ?.  But we only need the value of ?
    ; when we are in the recursion.  In the base case we never evaluate 
    ; f-builder.
     
    ; In other words, in the construction of f we have two cases driven by the
    ; input argument:
    ; The base case can compute the function result directly, without needing
    ; f and thus does not need to construct f. 
    ; The recursion needs to construct f prior to recursing, and 
    ; the recursion might need the builder.
      
    ; So the builder of f needs to be able to call itself.  
    ; Since we don't have a defined name for it (that would be cheating), 
    ; we need to pass it it's own name!
      
    ; So, now we define a new variant of f-builder, that instead of
    ; taking f as an argument, takes itself, so that it can build f.  That 
    ; is (f-builder f-builder) constructs f,
      
    ; so f-buiilder will look like this:
     
    (lambda (f-builder)
      (lambda (x)
        (if (> 0 x) x ( (f-builder f-builder) (- x 2)) )
        )
      )
     
    ; So now we just need to start this process by having the above
    ; expression call itself.
     
    ; But wait, how can you call yourself when you don't have a name?
    ; This is easily done with this kind of function
     
      (define call-yourself-with-yourself 
        (lambda (d) (d d)
        ))
     
    ; so we get something like this
     
      ( (lambda (d) (d d))  ; i.e. call yourself with yourself
        
        ; the f-builder that expects itself:
        
        (lambda (f-builder)
          (lambda (x)
            (if (> 0 x) x ( (f-builder f-builder) (- x 2)) )
            )
          )
        )
      
    ; ok, does this do what we want?
     
    (define f-version-1
      
      ( (lambda (d) (d d))
        
        (lambda (f-builder)
          (lambda (x)
            (if (> 0 x) x 
                ( (f-builder f-builder) (- x 2)) 
            )
          )
        )
    ))
     
    (f-version-1 -1)
    (f-version-1 0)
    (f-version-1 2)
     
    ; Wow, that actually works without going off the deep end of recursion!
    ; Why? Note how only in the recursion is f-builder invoked.
     
    ; So, now we have a function f-version-1 that is f, but it would be nice if 
    ; our definition of f actually look like a typical recursive one, rather 
    ; than the above which constructs f when needed.
     
    ; Let us introduce f-def as the term defining f. Then we can write things 
    ; this way (which is a simple defintion, not recursive):
     
    (define f-def
      (lambda (f) 
        (lambda (x)
          (if (> 0 x) x ( f (- x 2)) )
          )
        )
      )
      
    ; So we need to pass in the defintion of f, that is, 
    ;   (f-builder f-builder)
    ; or (call-yourself-with-yourself f-builder), 
    ; into f-def so that it can build f
     
     
    ; (define f-version-2
    ;   ( ; apply the general builder
    ;    (lambda (function-def)
    ;      
    ;      ( (lambda (d) (d d))  ; i.e. call yourself
    ;        
    ;        (lambda (function-builder)
    ;          (begin (print "Invoking function-builder") (newline) )
    ;          
    ;          ; this recursion does not terminate when evaluating:  
    ;          ;    (function-builder function-builder)
    ;          (function-def (function-builder function-builder) )
    ;          )
    ;        )
    ;      )
    ;    
    ;    ; to the defintion of f
    ;    f-def
    ;    )
    ;   )
    ; 
    ; (f-version-2 0)
    ; 
     
     
    (define f-version-3
      
      ( ; apply the builder 
       (lambda (function-def)
         
         ( (lambda (d) (d d))  ; i.e. call yourself
           
           (lambda (function-builder)
             ; (begin (print "Invoking function-builder") (newline) )
             
             ; delay the evaluation of (function-builder function-builder) until
             ; it is needed.  That is, make it a function, and this is f!
             
             (function-def 
                (lambda (y) ( (function-builder function-builder) y) ) )
             )
           )
         )
       
       ; to the definition
       f-def
       )
      )
       
     
    (map f-version-3 '(0 1 2 3))
     
    ; The general builder is completely independent of the definition of f, so we 
    ; can create the function (combinator) the converts a definition into the 
    ; actual function
     
    (define Y-comb
      (lambda (function-def)
        
        ( (lambda (d) (d d))  ; i.e. call yourself
          
          (lambda (function-builder)
            
            ; delay the evaluation of (function-builder function-builder) until
            ; it is needed.  That is, make it a function, and this is f!
            
            (function-def 
                (lambda (y) ((function-builder function-builder) y) ) )
            )
          )
        )
      )
     
    (map (Y-comb f-def) '(0 1 2 3))
     
    ; Amazing, we can now allow definitions in our restricted subset of Scheme!
     
    ( (Y-comb f-def) 3 )
     
    ; do not try this at home: (Y-comb Y-comb)
     


12.4 Examples of Typical Recursive Definitions

code/LambdaScheme/YCombExamples.rkt

    #lang racket
     
    (define Y-comb
      (lambda (function-def)
        
        ( (lambda (d) (d d))  ; i.e. call yourself
          
          (lambda (function-builder)
            (function-def 
                (lambda (y) ((function-builder function-builder) y) ) )
            )
          )
        )
      )
     
    (define fact 
      (Y-comb (lambda (fact) 
                (lambda (x) 
                  (if (<= x 0) 
                      1 
                      (* x (fact (- x 1))))))))
     
    (fact 2)
    (map fact '(0 1 2 3 4))
     
    ; a very slow version of fibonacci 
     
    (define fib
      (Y-comb (lambda (fib)
                (lambda (n) 
                  (if (<= n 0) 
                      1
                      (+ (fib (- n 1)) (fib (- n 2)))
                      )
                  )
                ))
      )
     
     
    (fib 0)
    (fib -1)
    (fib 2)
    (fib 4)
    (fib 10)
     
    ; (fib-fast n) returns a list of fib(n-1) fib(n)
     
    (define fib-fast
      (Y-comb (lambda (fib-fast)
                (lambda (n) 
                  (if (<= n 0) 
                      '(1 1)
                      ( 
                       (lambda (y) 
                         (list (second y) (+ (first y) (second y)))
                         )
                       (fib-fast (- n 1))
                       )
                      )
                  ))
              ))


12.5 Mutually Recursive Definitions

code/LambdaScheme/MutuallyRecursive.rkt

    #lang racket
     
    (define Y-comb
      (lambda (function-def)
        
        ( (lambda (d) (d d))  ; i.e. call yourself
          
          (lambda (function-builder)
            
            ; delay the evaluation of (function-builder function-builder) until
            ; it is needed.  That is, make it a function, and this is f!
            
            (function-def 
                (lambda (y) ((function-builder function-builder) y) ) )
            )
          )
        )
      )
     
    ; suppose we want to define mutually recursive functions f and g
    (define f 
      (lambda (x) (if (< x 0) "f" (g (- x 1))))
      )
     
    (define g
      (lambda (x) (if (< x 0) "g" (f (- x 1))))
      )
     
    ; since we have two names, we can't do this directly with the 
    ; Y combinator.  But we can collect both functions together under
    ; one name by having a selector function like this:
     
    (define h-select
      (lambda (s)
        (if (= 0 s) f g)
        ))
     
     
    ; (h 0 ) is f, (h 1) is g.  So we can expand the definition of f and g
    ; above, and replace the calls by the (h 0) and (h 1) to get this:
     
    (define h
      (lambda (s)
        (if (= 0 s) 
            (lambda (x) (if (< x 0) "f" ( (h 1) (- x 1)))) ; i.e. f
            (lambda (x) (if (< x 0) "g" ( (h 0) (- x 1)))) ; i.e. g
        ))
      )
     
    ; this is a simply recursive function with one argument, and so has a
    ; definition of the form the Y combinator likes.
     
    (define h-def
      (lambda (h)
        (lambda (s)
          (if (= 0 s) 
              (lambda (x) (if (< x 0) "f" ( (h 1) (- x 1)))) ; i.e. f
              (lambda (x) (if (< x 0) "g" ( (h 0) (- x 1)))) ; i.e. g
              ))
        )
      )
     
    (define h1 (Y-comb h-def))
     
     
     
12. The Extended Untyped lambda Calculus
Notes on Functional Programming / Version 2.08 2014-02-10