The Lambda Calculus Stephen A Edwards Columbia University Fall 2010 Lambda Expressions Function application written in prefix form Add four and five is 4 5 Evaluation select a redex and evaluate it 5 6 8 3 30 8 3 30 24 54 Often more than one way to proceed 5 6 8 3 5 6 24 30 24 54 Simon Peyton Jones The Implementation of Functional Programming Languages Prentice Hall 1987 Function Application and Currying Function application is written as juxtaposition f x Every function has exactly one argument Multiple argument functions e g are represented by currying named after Haskell Brooks Curry 1900 1982 So x is the function that adds x to its argument Function application associates left to right 3 4 3 4 7 Lambda Abstraction The only other thing in the lambda calculus is lambda abstraction a notation for defining unnamed functions x x 1 x x 1 That function of x that adds x to 1 The Syntax of the Lambda Calculus expr expr expr variable expr constant variable expr Constants are numbers and built in functions variables are identifiers Beta Reduction Evaluation of a lambda abstraction beta reduction is just substitution x x 1 4 4 1 5 The argument may appear more than once x x x 4 4 4 8 or not at all x 3 5 3 Beta Reduction Fussy but mechanical Extra parentheses may help x y x y 3 4 x y x y 3 4 y 3 y 4 3 4 7 Functions may be arguments f f 3 x x 1 x x 1 3 3 1 4 Free and Bound Variables x x y 4 Here x is like a function argument but y is like a global variable Technically x occurs bound and y occurs free in x x y However both x and y occur free in x y Beta Reduction More Formally x E F E 0 where E 0 is obtained from E by replacing every instance of x that appears free in E with F The definition of free and bound mean variables have scopes Only the rightmost x appears free in x x 1 x 3 so x x x 1 x 3 9 x x 1 9 3 9 1 3 83 11 Another Example x y x x x 3 y 5 6 y 5 x x 3 y 6 5 x x 3 6 5 6 3 53 8 Alpha Conversion One way to confuse yourself less is to do conversion renaming a argument and its bound variables Formal parameters are only names they are correct if they are consistent x x x 1 x 3 9 x y y 1 x 3 9 y y 1 9 3 9 1 3 8 3 11 Beta Abstraction and Eta Conversion Running reduction in reverse leaving the meaning of a lambda expression unchanged is called beta abstraction 4 1 x x 1 4 Eta conversion is another type of conversion that leaves meaning unchanged x 1 x 1 Formally if F is a function in which x does not occur free x F x F Reduction Order The order in which you reduce things can matter x y y z z z z z z Two things can be reduced z z z z z z x y y However z z z z z z z z z z z z x y y y y Normal Form A lambda expression that cannot be reduced is in normal form Thus y y is the normal form of x y y z z z z z z Not everything has a normal form E g z z z z z z can only be reduced to itself so it never produces an non reducible expression Normal Form Can a lambda expression have more than one normal form Church Rosser Theorem I If E1 E2 then there exists an expression E such that E1 E and E2 E Corollary No expression may have two distinct normal forms Proof Assume E1 and E2 are distinct normal forms for E E E1 and E E2 So E1 E2 and by the Church Rosser Theorem I there must exist an F such that E1 F and E2 F However since E1 and E2 are in normal form E1 F E2 a contradiction Normal Order Reduction Not all expressions have normal forms but is there a reliable way to find the normal form if it exists Church Rosser Theorem II If E1 E2 and E2 is in normal form then there exists a normal order reduction sequence from E1 to E2 Normal order reduction reduce the leftmost outermost redex Normal Order Reduction x w z w z 1 x x x x x x y y 1 2 3 leftmost outermost y x leftmost innermost x w w 3 1 1 x x x x z x z y 2 Recursion Where is recursion in the lambda calculus FAC n IF n 0 1 n FAC n 1 This does not work functions are unnamed in the lambda calculus But it is possible to express recursion as a function FAC n FAC f n f FAC H FAC That is the factorial function FAC is a fixed point of the non recursive function H H f n IF n 0 1 n f n 1 Recursion Let s invent a function Y that computes FAC from H i e FAC Y H FAC H FAC Y H H Y H FAC 1 YH1 H Y H 1 f n IF n 0 1 n f n 1 Y H 1 n IF n 0 1 n Y H n 1 1 IF 1 0 1 1 Y H 1 1 1 Y H 0 1 H Y H 0 1 f n IF n 0 1 n f n 1 Y H 0 1 n IF n 0 1 n Y H n 1 0 1 IF 0 0 1 0 Y H 0 1 11 1 The Y Combinator Here s the eye popping part Y can be a simple lambda expression Y f x f x x x f x x Y H f x f x x x f x x H x H x x x H x x H x H x x x H x x H f x f x x x f x x H H Y H Y The function that takes a function f and returns f f f f Alonzo Church 1903 1995 Professor at Princeton 1929 1967 and UCLA 1967 1990 Invented the Lambda Calculus Had a few successful graduate students including Stephen Kleene Regular expressions Michael O Rabin Nondeterministic automata Dana Scott Formal programming language semantics Alan Turing Turing machines Turing award winners Turing Machines vs Lambda Calculus In 1936 Alan Turing invented the Turing machine Alonzo Church invented the lambda calculus In 1937 Turing proved that the two models were equivalent i e that they define the same class of computable functions Modern processors are just overblown Turing machines Functional languages are just the lambda calculus with a more …
View Full Document
Unlocking...