1Lecture 20: λ Calculusλ Calculus & ComputabilityYan HuangDept. of Comp. Sci.University of Virginia2Lecture 20: λ Calculus• Formalism • Abstract Problems• Language Problems• Computation• Computability vs. DecidabilityReview of the Turing Machine(Q; ¡; §; ±; qstart; qaccept; qreject)Today we are looking at a completely different formal computation model – the λ-Calculus!3Lecture 20: λ CalculusCalculus• What is calculus?– Calculus is a branch of mathematics that includes the study of limits, derivatives, integrals, and infinite series.• ExamplesThe product ruleThe chain rule4Lecture 20: λ CalculusReal Definition• Calculus is just a bunch of rules for manipulating symbols.• People can give meaning to those symbols, but that’s not part of the calculus.• Differential calculus is a bunch of rules for manipulating symbols. There is an interpretation of those symbols corresponds with physics, geometry, etc.5Lecture 20: λ Calculusλ Calculus Formalism (Grammar)• Key words: λ . ( ) terminals• term →variable | ( term )| λ variable . term| term termHumans can give meaning to those symbols in a way that corresponds to computations.6Lecture 20: λ Calculusλ Calculus Formalism (rules)• Rulesα-reduction (renaming)λy. M ⇒αλv. (M [y v])where v does not occur in M.β-reduction (substitution)(λx. M)N ⇒βM [ x N ]aaReplace all x’s in Mwith NTry Example 1, 2, & 3 on the notes now!27Lecture 20: λ CalculusFree and Bound variables• In λ Calculus all variables are local to function definitions• Examples– λx.xyx is bound, while y is free;– (λx.x)(λy.yx)x is bound in the first function, but free in the second function– λx.(λy.yx) x and y are both bound variables. (it can be abbreviated as λxy.yx ) 8Lecture 20: λ CalculusBe careful about β-Reduction• (λx. M)N ⇒ M [ x N ]aReplace all x’s in Mwith NIf the substitution would bring a free variable of N in an expression where this variable occurs bound, we rename the bound variable before the substitution.Try Example 4 on the notes now!9Lecture 20: λ CalculusComputing Model for λ Calculus• redex: a term of the form (λx. M)N Something that can be β-reduced• An expression is in normal form if it contains no redexes (redices).• To evaluate a lambda expression, keep doing reductions until you get to normal form.β-Reduction represents all the computation capability of Lambda calculus.10Lecture 20: λ CalculusAnother exercise(λ f. ((λ x. f (xx)) (λ x. f (xx)))) (λz.z)11Lecture 20: λ CalculusPossible 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))→β...12Lecture 20: λ CalculusAlternate 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)→β...313Lecture 20: λ CalculusBe Very Afraid!• Some λ-calculus terms can be β-reduced forever!• The order in which you choose to do the reductions might change the result!14Lecture 20: λ CalculusTake on Faith• 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) evaluation15Lecture 20: λ CalculusAlonzo Church (1903~1995)Lambda CalculusChurch-Turing thesis If an algorithm (a procedure that terminates) exists then there is an equivalent Turing Machine or applicable λ-function for that algorithm. 16Lecture 20: λ CalculusAlan M. Turing (1912~1954)• Turing Machine• Turing Test• Head of Hut 8Advisor: Alonzo Church17Lecture 20: λ CalculusEquivalence in Computability• λ Calculus ↔ Turing Machine– (1) Everything computable by λ Calculus can be computed using the Turing Machine.– (2) Everything computable by the Turing Machine can be computed with λ Calculus.18Lecture 20: λ CalculusSimulate λ Calculus with TM• The initial tape is filled with the initial λexpression• Finite number of reduction rules can be implemented by the finite state automata in the Turing Machine• Start the Turing Machine; it either stops –ending with the λ expression on tape in normal form, or continues forever – the β-reductions never ends.419Lecture 20: λ CalculusWPI hacker implemented it on Z8 microcontrollerOn ZilogZ8 Encore 20Lecture 20: λ Calculusλ Calculus in a Can• Project LambdaCanRefer to http://alum.wpi.edu/~tfraser/Software/Arduino/lambdacan.html for instructions to build your own λ-can!21Lecture 20: λ CalculusEquivalence in Computability• λ Calculus ↔ Turing Machine– (1) Everything computable by λ Calculus can be computed using the Turing Machine.– (2) Everything computable by the Turing Machine can be computed with λ Calculus.22Lecture 20: λ CalculusSimulate TM with λ Calculus• Simulating the Universal Turing Machinez 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 MachineNumbersProcessingWay to make decisions (if)Way to keep going23Lecture 20: λ CalculusMaking Decisions• What does decision mean?– Choosing different strategies depending on the predicate• 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 T M N → Mif F M N → N24Lecture 20: λ CalculusFinding the Truthif ≡ λpca . pcaT ≡ λxy. xF ≡ λxy. yif T M N((λpca . pca) (λxy. x)) M N→β(λca . (λxy. x) ca)) M N→β→β(λxy. x) M N→β(λy. M )) N →βMTry out reducing (if F T F) on your notes now!525Lecture 20: λ Calculusand and or?• and ≡ λxy.(if x y F)→βλxy.((λpca.pca) x y F)→βλxy.(x y F)→βλxy.(x y (λuv.v))• or ≡ λxy.(if x T y)much more human-readable!26Lecture 20: λ CalculusSimulate TM with λ Calculus• Simulating the Universal Turing Machinez 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