Lecture 7 Lambda Calculus Revisited CS655 Programming Languages University of Virginia David Evans Computer Science http www cs virginia edu evans Menu Review last time Real reason for Lambda Calculus Substitution Rules Building Primitives 6 Feb 2001 CS 655 Lecture 6 2 What 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 3 Real 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 4 Lambda 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 5 Why 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 6 Evaluation 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 7 Defining Substitution 1 2 3 y x N N where x y y x N y where x y M1 M2 x N M1 x N M2 x N 4 x M x N x M 6 Feb 2001 CS 655 Lecture 6 8 Defining Substitution 5a y M x N y M x N where x y and y does not appear free in N and x appears free in M 5b y M x N y M where 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 9 Defining Substitution 5 y M x N y M x N where x y and y does not appear free in N 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 10 Reduction 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 11 Reduction the source of all computation x M N M x N 6 Feb 2001 CS 655 Lecture 6 12 Recall 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 13 Some Simple Functions I x x C 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 I 6 Feb 2001 CS 655 Lecture 6 14 Evaluating 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 15 Example f x f xx x f xx 6 Feb 2001 CS 655 Lecture 6 16 Alyssa 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 17 Ben 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 18 Be 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 19 Take 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 evaluation 6 Feb 2001 CS 655 Lecture 6 20 Who needs primitives T xy x F xy y if pca pca 6 Feb 2001 CS 655 Lecture 6 21 Evaluation T 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 M 6 Feb 2001 CS 655 Lecture 6 22 Who needs primitives and xy if x y F or xy if x T y 6 Feb 2001 CS 655 Lecture 6 23 Coupling M N z z M N first p p T second p p F first M N p p T z z M N z z M N T z z M N xy x xy x M N M 6 Feb 2001 CS 655 Lecture 6 24 Tupling n tuple M M M0 Mn 1 Mn M0 M1 Mn 1 Mn n tuple direct M0 Mn 1 Mn z z M0 Mn 1 Mn Pi n x x Ui n Ui n x0 xn xi What is P1 2 6 Feb 2001 CS 655 Lecture 6 25 What are numbers We need three functions succ n n 1 pred n n 1 zero n n 0 Is that enough to define add 6 Feb 2001 CS 655 Lecture 6 26 Adding for Post Docs add xy if zero x y add pred x succ y 6 Feb 2001 CS 655 Lecture 6 27 Counting 0 I 1 F I 2 F F I 3 F F F I n 1 F n 6 Feb 2001 CS 655 Lecture 6 28 Arithmetic Zero x x T Zero 0 x x T I T Zero 1 x x T F I F succ x F x pred x x F pred 1 x x …