λ Calculus & ComputabilityReview of the Turing MachineCalculusReal Definitionλ Calculus Formalism (Grammar)λ Calculus Formalism (rules)Free and Bound variablesBe careful about -ReductionSlide 9Another exercisePossible AnswerAlternate AnswerBe Very Afraid!Take on FaithAlonzo Church (1903~1995)Alan M. Turing (1912~1954)Equivalence in ComputabilitySimulate λ Calculus with TMWPI hacker implemented it on Z8 microcontroller Calculus in a CanSlide 21Simulate TM with λ CalculusMaking DecisionsFinding the Truthand and or?Slide 26What is 11?NumbersDefining NumbersDefining succ and predSlide 31Defining Listnull, null?, pair, first, restnull and null?Defining PairDefining predSlide 37Simulate RecursionSlide 39Introducing SchemeA Turing simulator in SchemeTM Simulator demonstrationSummary: TM and λ CalculusLecture 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; ¡; §; ±; qstar t; qaccept; qr ej ect)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 ]Replace all x’s in Mwith NTry Example 1, 2, & 3 on the notes now!7Lecture 20: λ CalculusFree and Bound variables•In λ Calculus all variables are local to function definitions•Examples–λx.xy x 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 ]Replace 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) ...13Lecture 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.19Lecture 20: λ CalculusWPI hacker implemented it on Z8 microcontrollerOn Zilog Z8 Encore20Lecture 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