Functional Programming and the Lambda Calculus Stephen A Edwards Columbia University Fall 2008 Functional vs Imperative Imperative programming concerned with how Functional programming concerned with what Based on the mathematics of the lambda calculus Church as opposed to Turing Programming without variables It is elegant and a difficult setting in which to create subtle bugs It s a cult once you catch the functional bug you never escape Referential transparency The main good property of functional programming is referential transparency Every expression denotes a single value The value cannot be changed by evaluating an expression or by sharing it between different parts of the program No references to global data there is no global data There are no side effects unlike in referentially opaque languages The Lambda Calculus Fancy name for rules about how to represent and evaluate expressions with unnamed functions Theoretical underpinning of functional languages Side effect free Very different from the Turing model of a store with evolving state O Caml fun x 2 x The Lambda Calculus x 2 x English The function of x that returns the product of two and x Grammar of Lambda Expressions expr constant variable name expr expr expr variable name expr Constants are numbers variable names are identifiers and operators Somebody asked does a language needs to have a large syntax to be powerful Bound and Unbound Variables In x 2 x x is a bound variable Think of it as a formal parameter to a function 2 x is the body The body can be any valid lambda expression including another unnnamed function x y x y 2 The function of x that returns the function of y that returns the product of the sum of x and y and 2 Currying x y x y 2 is equivalent to the O Caml fun x fun y x y 2 All lambda calculus functions have a single argument As in O Caml multiple argument functions can be built through such currying Currying is named after Haskell Brooks Curry 1900 1982 who contributed to the theory of functional programming The Haskell functional language is named after him Calling Lambda Functions To invoke a Lambda function we place it in parentheses before its argument Thus calling x 2 x with 4 is written x 2 x 4 This means 8 Curried functions need more parentheses x y x y 2 4 5 This binds 4 to y 5 to x and means 18 Evaluating Lambda Expressions Pure lambda calculus has no built in functions we ll be impure To evaluate 5 6 8 3 we can t start with because it only operates on numbers There are two reducible expressions 5 6 and 8 3 We can reduce either one first For example 5 6 8 3 30 8 3 30 24 54 Looks like deriving a sentence from a grammar Evaluating Lambda Expressions We need a reduction rule to handle s x 2 x 4 2 4 8 This is called reduction The formal parameter may be used several times x x x 4 4 4 8 Beta reduction May have to be repeated x y x y 5 4 y 5 y 4 5 4 1 Functions may be arguments f f 3 x x 1 x x 1 3 3 1 4 More Beta reduction Repeated names can be tricky x x x 1 x 3 9 x x 1 9 3 9 1 3 83 11 In the first line the inner x belongs to the inner the outer x belongs to the outer one Free and Bound Variables In an expression each appearance of a variable is either free unconnected to a or bound an argument of a reduction of x E y replaces every x that occurs free in E with y Free or bound is a function of the position of each variable and its context Free variables x x y y y x Bound variables Alpha conversion One way to confuse yourself less is to do conversion This is renaming a argument and its bound variables Formal parameters are only names they are correct if they are consistent x x x 1 x x y y 1 x Alpha Conversion An easier way to attack the earlier example x x x 1 x 3 9 x y y 1 x 3 9 y y 1 9 3 9 1 3 83 11 Reduction Order The order in which you reduce things can matter x y y z z z z z z We could choose to reduce one of two things either z z z z z z or the whole thing x y y z z z z z z Reduction Order Reducing z z z z z z effectively does nothing because z z z is the function that calls its first argument on its first argument The expression reduces to itself z z z z z z So always reducing it does not terminate However reducing the outermost function does terminate because it ignores its nasty argument x y y z z z z z z y y Reduction Order The redex is a sub expression that can be reduced The leftmost redex is the one whose is to the left of all other redexes You can guess which is the rightmost The outermost redex is not contained in any other The innermost redex does not contain any other For x y y z z z z z z z z z z z z is the leftmost innermost and x y y z z z z z z is the leftmost outermost Applicative vs Normal Order Applicative order reduction Always reduce the leftmost innermost redex Normative order reduction Always reduce the leftmost outermost redex For x y y z z z z z z applicative order reduction never terminated normative order did Applicative vs Normal Order Applicative reduce leftmost innermost Normative reduce leftmost outermost evaluate arguments before the function itself evaluate the function before its arguments eager evaluation call by value usually more efficient lazy evaluation call by name more costly to implement accepts a larger class of programs Normal Form A lambda expression that cannot be reduced further is in normal form Thus y y is the normal form of x y y z z z z z z Normal Form 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 Infinite loop The Church Rosser Theorems If E 1 E 2 are interconvertable then there exists an E such that E 1 E and E 2 E Reduction in any way can eventually produce the same result If E 1 E 2 and E 2 is is normal form then there is a normal order reduction of E 1 to E 2 Normal order reduction will always produce a normal form if one exists Church Rosser Amazing result Any way you choose to evaluate a lambda expression can produce the same result i e it is confluent Running a lambda calculus program gives a deterministic result if it terminates …
View Full Document
Unlocking...