CSC302 2006S, Class 8: The Lambda Calculus

Admin:
* Homework due date extended one week.  Do not wait until next week to begin.
* Time for questions on the homework.
* Reading homework (both linked from today's outline):
  * Section 20.1 of Paul Graham's "On Lisp"
  * The part of R5RS on continuations

Overview:
* Why discuss the lambda calculus?
* Historical issues
* Basics
* Currying

Questions on the Homework:
* Can you explain more about what we should do in Java/C?
  + (a) Implement the core operations (cons, car, cdr, etc.)
  + (b) Implement a non-user-callable "eval" that interprets
    S-expressions built from those core operations.
  + (c) Build the S-expression for "eval."
  + (d) Show that it works by calling "eval" on 
    (cons eval. some-expression)
  + (e) Your life will be easier if you write the read-eval-print loop
* Can the parser be stupid and only accept correct input
  + Yes.
* Can I define my own syntax?
  + Yes, but why?

Why Study The Lambda Calculus
* McCarthy incorporated ideas from Church's lambda calc. in Lisp
* Helps to understand some of the key issues
* Denotational Semantics uses the lambda calculus

History
* Developed by Alonzo Church in early 20th century
* Current trend at the time: Mathematical Logic
  + How do formalize how mathematicians "reason"
  + Formalize notions of computation
* Important conclusion by both Church and Turing
  + Any function computable by a "reasonable" method of computation is computable by "my model of computation"
    + Substitute "lambda calculus" or "Turing machine"
    + Corollary: The lambda calculus and Turing machines are *equivalent* models of computation
    + Implied: Any reasonable and sufficiently powerful method of computation is equivalent to any other model

What is the Lambda Calculus?
* Based on a reflection that mathematicians regularly speak of functions anonymously "a function that, given an input x, computes ..."
* Notation: \ x . whatever
  + Read "lambda" for the backslash
  + McCarthy: (lambda (x) whatever)
* We apply functions by writing the function before the params
  (\ x . x) y => y
* We can name functions
  id = \x . x
* The body of a lambda can be
  * a lambda expression
  * a symbol bound by the lambda
  * a symbol not bound by the lambda
  * the application of one of the above to one of the above (and so on and so forth recursively)
* In the lambda calculus, things you and I think of as values are, instead, functions
* In the lambda calculus, we can express a Boolean as a function of two parameters, x and y
  * Define true = \ x y . x
  * Define false = \ x y . y
  * Define if = \ c t f . c t f
    * Parameters: Condition, True-Result, False-Result
    * if true t f => true t f => t
    * if false t f => false t f => f
* Implied computation: When you apply a lambda function to some parameteters, you substitute the actuals for the formals in the body
  * With sensitivity to scoping issues
* We also might want boolean connectivies
  * Define or = \ b1 b2 . (\ x y . b1 x (b2 x y))
        if (or (false true)) t f
        => (or (false true)) t f
        => (\ x y . false x (true x y)) t f
        => false t (true t f)
        => true t f
        => t
  * Define not = \ b . (\ x y . b y x)
        if (not true) t f
        => (not true) t f
        => (\ x y . true y x) t f
        => true f t
        => f
* Church defined a host of other things, including numbers
  * 0 is defined as \s \z . z
  * 1 is defined as \s \z . s z
  * 2 is defined as \s \z . s (s z)
* You can therefore use numbers as functions
  5 square 2
  100 not false
* Church also defined the Y combinator, a way to define recursive functions without explicit recursion

Other important notational idea: Currying
* Idea: \ x y . whatever is essentially the same as \x . \y . whatever
* Treat them as equivalent

Example: Suppose we have plus as a built-in operation

; Curried
(map (plus 2) lst)
; Non-curried
(map (left-section plus 2) lsta)

add:

\ n m . \ s z . n s m