Functional Programmingand theLambda Calculu sStephen A. EdwardsColumbia UniversityFall 2008Functional vs. ImperativeImperative programming concerned with “how.”Functional programming concerned with “what.”Based on the mathematics of the lambda calculus (Church asopposed 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 transparencyThe main (good) property of functional programming is referentialtransparency.Every expression denotes a single value.The value cannot be changed by evaluating an expression or bysharing it between different part s of the program.No references to global da ta; there is no global data.There are no side-effects, unlike in referentially opaque languages.The Lambda CalculusFancy name for rules about how to represent a nd evaluateexpressions with unnamed functions.Theoretical underpinning of functional languages. Side-effect free.Very diff erent from the Turing model of a store with evolving state.O’Caml:fun x -> 2*xThe L ambda Calculus:λx . ∗ 2 xEnglish:The function of x tha t returns the product of two and xGrammar of Lambda Expressionsexpr → constant| variable-name| expr expr| (expr)| λ variable-name . exprConstants are numbers; variable names are identifiers an doperators.Somebody asked, “does a language needs to have a large syntax tobe power ful?”Bound and Unbound VariablesIn λx . ∗ 2 x, x is a bound variable. Think of it as a formal parameterto a function.“∗ 2 x” is the body.The body can be any valid lambda expression, including anotherunnnamed function.λx . λy . ∗ (+ x y) 2“The function of x that returns the function of y that returns theproduct of t he sum of x and y and 2.”Curryingλx . λy . ∗ (+ x y) 2is equivalent to the O’Camlfun x -> fun y -> (x + y)*2All lambda calculus functions have a single argument.As in O’Caml, multiple-argument functions can be built throughsuch “currying.”Currying is named after Haskell Brooks Curry (1900–1982), whocontributed to the theory of functional programming. The Haskellfunctional language is named after him.Calling Lambda FunctionsTo invoke a Lambda function, we place it in parentheses before itsargument.Thus, calling λx . ∗ 2 x with 4 is written(λx . ∗ 2 x) 4This mean s 8.Curried functions need more parentheses:(λx . (λy . ∗ (+ x y) 2) 4) 5This binds 4 to y, 5 to x, and means 18.Evaluating Lambda ExpressionsPure lambda calculus has no built-in functions; we’ll be impure.To evaluate (+ (∗ 5 6) (∗ 8 3)), we can’t star t with + because it onlyoperates on numbers.There are two reducible expressions: (∗ 5 6) and (∗ 8 3). We canreduce either one first. For example:(+ (∗ 5 6) (∗ 8 3))(+ 30 (∗ 8 3))(+ 30 24)54Looks like deriving a sentencefrom a grammar.Evaluating Lambda ExpressionsWe need a reduction rule to handle λs:(λx . ∗ 2 x) 4(∗ 2 4)8This is called β-reduction.The formal parameter may be u sed several times:(λx . + x x) 4(+ 4 4)8Beta-reductionMay have to be repeated:((λx . (λy . − x y)) 5) 4(λy . − 5 y) 4(− 5 4)1Functions may be arguments:(λf . f 3)(λx . + x 1)(λx . + x 1)3(+ 3 1)4More Beta-reductionRepeated names can be tricky :(λx . (λ x . + (− x 1)) x 3) 9(λx . + (− x 1)) 9 3+ (− 9 1) 3+ 8 311In the first line, the inner x belongs to the inner λ, t he outer xbelongs to the outer one.Free and Bound Variab lesIn 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 fu nction of the position of each variable and itscontext.Free variables(λx . x y (λy . + y )) xBound var iablesAlpha conversionOne way to confuse yourself less is to do α-conversion.This is renaming a λ argument and its bound variables.Formal p arameters are only na mes: t hey are correct if they a reconsistent.λx . (λx . x) (+ 1 x) ←→αλx . (λy . y) (+ 1 x)Alpha ConversionAn easier way to attack the earlier exa mple:(λx . (λ x . + (− x 1)) x 3) 9(λx . (λy . + (− y 1)) x 3) 9(λy . + (− y 1)) 9 3+ (− 9 1) 3+ 8 311Reduction OrderThe order in which you reduce things can matter.(λx . λy . y) ( (λz . z z) (λz . z z) )We could choose to reduce one of t wo things, either(λz . z z) (λz . z z)or the whole thing(λx . λy . y) ( (λz . z z) (λz . z z) )Reduction OrderReducing (λz . z z) (λz . z z) effectively does nothing because(λz . z z) is the function that calls its fir st argument on its firstargument. The e xpression reduces to itself:(λz . z z) (λz . z z)So always reducing it does not t erminate.However, reducing the outermost function does terminate becauseit ignores its (nasty) argument:(λx . λy . y) ( (λz . z z) (λz . z z) )λy . yReduction OrderThe redex is a sub-expression that can be reduced.The leftmost redex is the one whose λ is to the left of all otherredexes. You can guess which is th e 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 OrderApplicative order reduction: Always reduce t he leftmost innermostredex.Normative order reduction: Always reduce the leftmostoutermostredex.For(λx . λy . y) ( (λz . z z) (λz . z z) )applicative order reduction never t erminated; normat ive order did.Applicative vs. Normal OrderApplicative:reduce leftmost innermost“evaluate arguments before thefunction itself”eager evaluation, call-by-value,usually more efficientNormative:reduce left most outermost“evaluate the function before itsarguments”lazy evaluation, call-by-name,more costly to implement,accepts a larger class of programsNormal FormA lambda expression that cannot be reduced further is in normalform.Thus,λy . yis the normal form of(λx . λy . y) ( (λz . z z) (λz . z z) )Normal FormNot 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- reducibleexpression.“Infinite loop.”The Church-Rosser TheoremsIf E1↔ E2(are interconvertable), then there exists an E such thatE1→ E and E2→ E.“Reduction in any way can eventu ally produce t he same result.”If E1→ E2, and E2is is
View Full Document
Unlocking...