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