1David Evanshttp://www.cs.virginia.edu/evansCS150: Computer ScienceUniversity of VirginiaComputer ScienceClass 28: The Meaning of Truthhttp://chandra.harvard.edu/photo/2001/0094true/0094true_hand.html2CS150 Fall 2005: Lecture 28: Lambda Calculusλ-calculusAlonzo Church, 1940(LISP was developed from λ-calculus, not the other way round.)term = variable | term term | (term)| λλλλ variable . term3CS150 Fall 2005: Lecture 28: Lambda CalculusReduction (Uninteresting Rules)λy. M → λv. (M [y ↵ v])where v does not occur in M.M → MM → N ⇒ PM → PNM → N ⇒ MP → NPM → N ⇒ λx. M → λx. NM → N and N → P ⇒ M → P4CS150 Fall 2005: Lecture 28: Lambda Calculusβ-Reduction (the source of all computation)(λx. M)N → M [ x ↵ N ]5CS150 Fall 2005: Lecture 28: Lambda CalculusEvaluating Lambda Expressions•redex: Term of the form (λx. M)N Something that can be β-reduced• An expression is in normal formif it contains no redexes (redices).• To evaluate a lambda expression, keep doing reductions until you get to normal form.6CS150 Fall 2005: Lecture 28: Lambda CalculusRecall Apply in Scheme“To apply a procedure to a list of arguments, evaluate the procedure in a new environment that binds the formal parameters of the procedure to the arguments it is applied to.”• We’ve replaced environments with substitution.• We’ve replaced eval with reduction.27CS150 Fall 2005: Lecture 28: Lambda CalculusSome Simple FunctionsI ≡ λx.xC ≡ λxy.yxAbbreviation for λx.(λy. yx)CII = (λx.(λy. yx)) (λx.x) (λx.x)→β(λy. y (λx.x)) (λx.x)→βλx.x (λx.x)→βλx.x= I8CS150 Fall 2005: Lecture 28: Lambda CalculusExampleλ f. ((λ x.f (xx)) (λ x. f (xx)))Try this one at home...9CS150 Fall 2005: Lecture 28: Lambda CalculusAlyssa P. Hacker’s Answer(λ f. ((λ x.f (xx)) (λ x. f (xx)))) (λz.z)→β(λx.(λz.z)(xx)) (λ x. (λz.z)(xx))→β(λz.z) (λ x.(λz.z)(xx)) (λ x.(λz.z)(xx))→β(λx.(λz.z)(xx)) (λ x.(λz.z)(xx))→β(λz.z) (λ x.(λz.z)(xx)) (λ x.(λz.z)(xx))→β(λx.(λz.z)(xx)) (λ x.(λz.z)(xx))→β...10CS150 Fall 2005: Lecture 28: Lambda CalculusBen Bitdiddle’s Answer(λ f. ((λ x.f (xx)) (λ x. f (xx)))) (λz.z)→β(λx.(λz.z)(xx)) (λ x. (λz.z)(xx))→β(λx.xx) (λx.(λz.z)(xx))→β(λx.xx) (λx.xx)→β(λx.xx) (λx.xx)→β...11CS150 Fall 2005: Lecture 28: Lambda CalculusBe Very Afraid!• Some λ-calculus terms can be β-reduced forever!• The order in which you choose to do the reductions might change the result!12CS150 Fall 2005: Lecture 28: Lambda CalculusTake on Faith (until CS655)• All ways of choosing reductions that reduce a lambda expression to normal form will produce the same normal form (but some might never produce a normal form).• If we always apply the outermost lambda first, we will find the normal form if there is one.– This is normal order reduction– corresponds to normal order (lazy) evaluation313CS150 Fall 2005: Lecture 28: Lambda CalculusUniversal Language• Is Lambda Calculus a universal language?– Can we compute any computable algorithm using Lambda Calculus?• To prove it isn’t:– Find some Turing Machine that cannot be simulated with Lambda Calculus• To prove it is:– Show you can simulate everyTuring Machine using Lambda Calculus14CS150 Fall 2005: Lecture 28: Lambda CalculusSimulating Every Turing Machine• A Universal Turing Machine can simulate every Turing Machine• So, to show Lambda Calculus can simulate every Turing Machine, all we need to do is show it can simulate a Universal Turing Machine15CS150 Fall 2005: Lecture 28: Lambda CalculusSimulating Computationz z z z z z z z z z z z z z z zz z z z1StartHALT), X, L2: look for (#, 1, -¬), #, R¬(, #, L(, X, R#, 0, -Finite State Machine• Lambda expression corresponds to a computation: input on the tape is transformed into a lambda expression• Normal form is that value of that computation: output is the normal form• How do we simulate the FSM?16CS150 Fall 2005: Lecture 28: Lambda CalculusSimulating Computationz z z z z z z z z z z z z z z zz z z z1StartHALT), X, L2: look for (#, 1, -¬), #, R¬(, #, L(, X, R#, 0, -Finite State MachineRead/Write Infinite TapeMutable ListsFinite State MachineNumbers to keep track of stateProcessingWay of making decisions (if)Way to keep going17CS150 Fall 2005: Lecture 28: Lambda CalculusMaking “Primitives”from Only Glue (λ)18CS150 Fall 2005: Lecture 28: Lambda CalculusIn search of the truth?• What does true mean?• True is something that when used as the first operand of if, makes the value of the if the value of its second operand:if TM N→M419CS150 Fall 2005: Lecture 28: Lambda CalculusDon’t search for T, search for ifT ≡ λx (λy. x)≡ λxy. xF ≡ λx (λ y. y))if ≡ λpca . pca20CS150 Fall 2005: Lecture 28: Lambda CalculusFinding the TruthT ≡ λx . (λy. x)F ≡ λx . (λy. y)if ≡ λp . (λc . (λa . pca)))if T M N((λpca . pca) (λxy. x)) M N→β(λca . (λx.(λy. x)) ca)) M N→β→β(λx.(λy. x)) M N→β(λy. M )) N →βMIs the if necessary?21CS150 Fall 2005: Lecture 28: Lambda Calculusand and or?and ≡ λx (λy. if x y F))or ≡ λx (λy. if x T y))22CS150 Fall 2005: Lecture 28: Lambda CalculusLambda Calculus is a Universal Computer?z z z z z z z z z z z z z z z zz z z z1StartHALT), X, L2: look for (#, 1, -¬), #, R¬(, #, L(, X, R#, 0, -Finite State Machine• Read/Write Infinite Tape? Mutable Lists• Finite State Machine? Numbers to keep track of state• Processing Way of making decisions (if)? Way to keep going23CS150 Fall 2005: Lecture 28: Lambda CalculusCharge• PS6 Due Monday• Start thinking about web application ideas for PS8– If you find a team and idea quickly (by Nov 2), you can negotiate what you need to do for PS7• Week after: we will finish this proof– How to make the other things we need to simulate a Turing machine using only Lambda
View Full Document
Unlocking...