Lambda-CalculusReading AssignmentLambda CalculusHistoryWhy Study Lambda-Calculus?Expressions and FunctionsHigher-Order FunctionsSame Procedure (ML)Same Procedure (JavaScript)Declarations as “Syntactic Sugar”Free and Bound VariablesReductionRenaming Bound VariablesMain Points About Lambda CalculusWhat is a Functional Language?No-Side-Effects Language TestBackus’ Turing AwardReasoning About ProgramsQuicksort in HaskellCompare: Quicksort in CCase StudyVon Neumann BottleneckEliminating VN Bottleneckslide 1Vitaly ShmatikovCS 345Lambda-Calculusslide 2Reading AssignmentMitchell, Chapter 4.2slide 3Lambda CalculusFormal system with three parts• Notation for function expressions• Proof system for equations• Calculation rules called reductionAdditional topics in lambda calculus• Mathematical semantics• Type systemsslide 4HistoryOrigins: formal theory of substitution• For first-order logic, etc.More successful for computable functions• Substitution → symbolic computation• Church/Turing thesisInfluenced design of Lisp, ML, other languagesImportant part of CS history and foundationsslide 5Why Study Lambda-Calculus?Basic syntactic notions• Free and bound variables• Functions• DeclarationsCalculation rule• Symbolic evaluation useful for discussing programs• Used in optimization (inlining), macro expansion– Correct macro processing requires variable renaming• Illustrates some ideas about scope of binding– Lisp originally departed from standard lambda calculus, returned to the fold through Scheme, Common Lispslide 6Expressions and FunctionsExpressionsx + y x + 2*y + zFunctionsλx. (x+y) λz. (x + 2*y + z)Application(λx. (x+y)) 3 = 3 + y(λz. (x + 2*y + z)) 5 = x + 2*y + 5Parsing: λx. f (f x) = λx.( f (f (x)) )slide 7Higher-Order FunctionsGiven function f, return function f ° fλf. λx. f (f x)How does this work?(λf. λx. f (f x)) (λy. y+1)= λx. (λy. y+1) ((λy. y+1) x)= λx. (λy. y+1) (x+1)= λx. (x+1)+1Same result if step 2 is alteredslide 8Same Procedure (ML)Given function f, return function f ° ffn f => fn x => f(f(x))How does this work?(fn f => fn x => f(f(x))) (fn y => y + 1)= fn x => ((fn y => y + 1) ((fn y => y + 1) x))= fn x => ((fn y => y + 1) (x + 1)) = fn x => ((x + 1) + 1)slide 9Same Procedure (JavaScript)Given function f, return function f ° ffunction (f) { return function (x) { return f(f(x)); } ; }How does this work?(function (f) { return function (x) { return f(f(x)); } ; })(function (y) { return y + 1; })function (x) { return (function (y) { return y + 1; })((function (y) { return y + 1; }) (x)); }function (x) { return (function (y) { return y +1; }) (x + 1); }function (x) { return ((x + 1) + 1); }slide 10Declarations as “Syntactic Sugar”function f(x) {return x+2;}f(5);block body declared function(λf. f(5)) (λx. x+2)slide 11Free and Bound VariablesBound variable is a “placeholder”• Variable x is bound in λx. (x+y) • Function λx. (x+y) is same function as λz. (z+y) Compare∫ x+y dx = ∫ z+y dz ∀x P(x) = ∀z P(z) Name of free (i.e., unbound) variable matters!• Variable y is free in λx. (x+y) • Function λx. (x+y) is not same as λx. (x+z)Occurrences• y is free and bound in λx. ((λy. y+2) x) + yslide 12ReductionBasic computation rule is β-reduction(λx. e1) e2→ [e2/x]e1where substitution involves renaming as needed (why?)Reduction• Apply basic computation rule to any subexpression• Repeat Confluence• Final result (if there is one) is uniquely determinedslide 13Renaming Bound VariablesFunction application(λf. λx. f (f x)) (λy. y+x)apply twice add x to argumentSubstitute “blindly” – do you see the problem?λx. [(λy. y+x) ((λy. y+x) x)] = λx. x+x+x Rename bound variables(λf. λz. f (f z)) (λy. y+x)= λz. [(λy. y+x) ((λy. y+x) z))] = λz. z+x+x Easy rule: always rename variables to be distinctslide 14Main Points About Lambda Calculus λ captures the “essence” of variable binding• Function parameters• Declarations• Bound variables can be renamedSuccinct function expressionsSimple symbolic evaluator via substitutionCan be extended with• Types, various functions, stores and side effects…slide 15What is a Functional Language?“No side effects”Pure functional language: a language with functions, but without side effects or other imperative featuresslide 16No-Side-Effects Language TestWithin the scope of specific declarations of x1,x2, …, xn, all occurrences of an expression e containing only variables x1,x2, …, xn, must have the same value.begininteger x=3; integer y=4;5*(x+y)-3 … // no new declaration of x or y //4*(x+y)+1endslide 17Backus’ Turing AwardJohn Backus: 1977 Turing Award• Designer of Fortran, BNF, etc.Turing Award lecture• Functional programming better than imperative programming• Easier to reason about functional programs• More efficient due to parallelism• Algebraic laws – Reason about programs– Optimizing compilersslide 18Reasoning About ProgramsTo prove a program correct, must consider everything a program depends onIn functional programs, dependence on any data structure is explicit (why?)Therefore, it’s easier to reason about functional programsDo you believe this?slide 19Quicksort in HaskellVery succinct programqsort [] = [] qsort (x:xs) = qsort elts_lt_x ++ [x] ++ qsort elts_greq_x where elts_lt_x = [y | y <- xs, y < x] elts_greq_x = [y | y <- xs, y >= x] This is the whole thing• No assignment – just write expression for sorted list• No array indices, no pointers, no memory management, …slide 20Compare: Quicksort in Cqsort( a, lo, hi ) int a[], hi, lo; { int h, l, p, t; if (lo < hi) { l = lo; h = hi; p = a[hi]; do { while ((l < h) && (a[l] <= p)) l = l+1; while ((h > l) && (a[h] >= p)) h = h-1;if (l < h) { t = a[l]; a[l] = a[h]; a[h] = t; } } while (l < h); t = a[l]; a[l] = a[hi]; a[hi] = t; qsort( a, lo, l-1 ); qsort( a, l+1, hi ); } }slide 21Case StudyNaval Center programming experiment• Separate teams worked on separate languagesSome programs were incomplete or did not run• Many evaluators didn’t understand, when shown the code, that the Haskell program was complete. They thought it was a high-level partial specification.[Hudak and Jones, Yale TR, 1994]slide 22Von Neumann BottleneckVon