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