PowerPoint PresentationMenuWhat is Calculus?Real DefinitionLambda CalculusWhy?Evaluation RulesDefining Substitution (|)Slide 9Slide 10Reduction (Uninteresting Rules)-Reduction (the source of all computation)Recall Apply in SchemeSome Simple FunctionsEvaluating Lambda ExpressionsExampleAlyssa P. Hacker’s AnswerBen Bitdiddle’s AnswerBe Very Afraid!Take on Faith (for now)Who needs primitives?EvaluationSlide 23CouplingTuplingWhat are numbers?Adding for Post-DocsCountingArithmeticFactorialSummaryChargeLecture 7: Lambda Calculus RevisitedDavid Evanshttp://www.cs.virginia.edu/~evansCS655: Programming LanguagesUniversity of VirginiaComputer Science6 Feb 2001 CS 655: Lecture 6 2Menu•Review last time–Real reason for Lambda Calculus–Substitution Rules•Building Primitives6 Feb 2001 CS 655: Lecture 6 3What is Calculus?•In High School:d/dx xn = nxn-1 [Power Rule]d/dx (f + g) = d/dx f + d/dx g [Sum Rule]Calculus is a branch of mathematics that deals with limits and the differentiation and integration of functions of one or more variables...6 Feb 2001 CS 655: Lecture 6 4Real Definition•A 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, slopes, etc.6 Feb 2001 CS 655: Lecture 6 5Lambda Calculus•Rules for manipulating strings of symbols in the language: term = variable | term term | (term) |  variable . term •Humans can give meaning to those symbols in a way that corresponds to computations.6 Feb 2001 CS 655: Lecture 6 6Why?•Once we have precise and formal rules for manipulating symbols, we can use it to reason with.•Since we can interpret the symbols as representing computations, we can use it to reason about programs.6 Feb 2001 CS 655: Lecture 6 7Evaluation Rules-reduction (renaming) y. M  v. (M [y v])where v does not occur in M.-reduction (substitution) (x. M)N   M [ x N ] 6 Feb 2001 CS 655: Lecture 6 8Defining Substitution (|) 1. y [x | N] = N where x  y2. y [x | N] = y where x  y3. M1 M2 [x | N] = M1 [x | N] M2 [x | N]4. (x. M) [x | N] = x. M6 Feb 2001 CS 655: Lecture 6 9Defining Substitution (|) 5a. (y. M) [x | N] = y. (M [x | N])where x  y and y does not appear free inN and x appears free in M.5b. (y. M) [x | N] = y. Mwhere x  y and y does or does not appear free in N and x does not appear free in M.6 Feb 2001 CS 655: Lecture 6 10Defining Substitution (|) 5. (y. M) [x | N] =  y. (M [x | N])where x  y and y does not appear free inN or x does not appear free in M.6. (y. M) [x | N] = z. (M [y | z]) [x | N]where x  y, z  x and z  y and z does not appear in M or N, x does occur free in M and y does occur free in N.6 Feb 2001 CS 655: Lecture 6 11Reduction (Uninteresting Rules) y. M  v. (M [y v])where v does not occur in M. M  M M  N  PM  PN M  N  MP  NP M  N  x. M  x. N M  N and N  P  M  P6 Feb 2001 CS 655: Lecture 6 12-Reduction (the source of all computation) (x. M)N  M [ x N ]6 Feb 2001 CS 655: Lecture 6 13Recall 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.6 Feb 2001 CS 655: Lecture 6 14Some Simple FunctionsI  x.xC  xy.yx Abbreviation for x.(y. yx)CII = (x.( y. yx)) (x.x) (x.x)  (y. y (x.x)) (x.x)  x.x ( x.x)  x.x= I6 Feb 2001 CS 655: Lecture 6 15Evaluating Lambda Expressions•redex: 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.6 Feb 2001 CS 655: Lecture 6 16Example f. (( x.f (xx)) ( x. f (xx)))6 Feb 2001 CS 655: Lecture 6 17Alyssa 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)) ...6 Feb 2001 CS 655: Lecture 6 18Ben 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) ...6 Feb 2001 CS 655: Lecture 6 19Be Very Afraid!•Some -calculus terms can be  -reduced forever!•The order in which you choose to do the reductions might change the result!6 Feb 2001 CS 655: Lecture 6 20Take on Faith (for now)•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 is there is one.–This is normal order reduction – corresponds to normal order (lazy) evaluation6 Feb 2001 CS 655: Lecture 6 21Who needs primitives?T   xy. x F  xy. y if  pca . pca6 Feb 2001 CS 655: Lecture 6 22EvaluationT  xy. x F  xy. y if  pca . 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   M6 Feb 2001 CS 655: Lecture 6 23Who needs primitives?and  xy. if x y For  xy. if x T y6 Feb 2001 CS 655: Lecture 6 24Coupling[M, N]  z.z M N first  p.p Tsecond  p.p Ffirst [M, N]=  p.p T (z.z M N)   (z.z M N) T = (z.z M N) xy. x   (xy. x) M N   M6 Feb 2001 CS 655: Lecture 6 25Tuplingn-tuple: [M] = M[M0,..., Mn-1, Mn] = [M0, [M1 ,..., [Mn-1, Mn ]... ]n-tuple direct: [M0,..., Mn-1, Mn] = z.z M0,..., Mn-1, MnPi,n = x.x Ui,nUi,n = x0... xn. xiWhat is P1,2?6 Feb 2001 CS 655: Lecture 6 26What are numbers?•We need three (?) functions:succ: n  n + 1pred: n  n – 1zero?: n  (n = 0)•Is that enough to define