WIXLIB

Lambda Calculus

What is l-calculus Programming language Invented in 1930s, by Alonzo Church and Stephen ColeKleene Model for computation Alan Turing, 1937: Turing machines equal l-calculus inexpressiveness

Why learn l-calculus Foundations of functional programming Lisp, ML, Haskell, Often used as a core language to study languagetheories Type systemint x 0;Scope and bindingfor (int i 0; i 10; i ) { x ; }Higher-order functionsx “abcd”; // bug (mistype)Denotational semanticsi ; // bug (out of scope)Program equivalence How to formally define andrule out these bugs?

Overview: l-calculus as a language Syntax How to write a program? Keyword “l” for defining functions Semantics How to describe the executions of a program? Calculation rules called reduction Others Type system (next class) Model theory (not covered)

Syntax l terms or l expressions:(Terms) M, N :: x lx. M M N Lambda abstraction (lx.M): “anonymous” functionsint f (int x) { return x; } èlx. x Lambda application (M N):int f (int x) { return x; }f(3);è (lx. x) 3 3

Syntax l terms or l expressions:(Terms) M, N :: x lx. M M N pure l-calculus Add extra operations and data types lx. (x 1) lz. (x 2*y z) (lx. (x 1)) 3 3 1 (lz. (x 2*y z)) 5 x 2*y 5

Conventions Body of l extends as far to the right as possiblelx. M N means lx. (M N), not (lx. M) N lx. f x lx. ( f x ) lx. lf. f x lx. ( lf. f x ) Function applications are left-associativeM N P means (M N) P, not M (N P) (lx. ly. x - y) 5 3 ( (lx. ly. x - y) 5 ) 3 (lf. lx. f x) (lx. x 1) 2 ( (lf. lx. f x) (lx. x 1) ) 2

Higher-order functions Functions can be returned as return valueslx. ly. x - y Functions can be passed as arguments(lf. lx. f x) (lx. x 1) 2Think about function pointers in C/C .

Higher-order functions Given function f, return function f flf. lx. f (f x) How does this work?(lf. lx. f (f x)) (ly. y 1) 5 (lx. (ly. y 1) ((ly. y 1) x)) 5 (lx. (ly. y 1) (x 1)) 5 (lx. (x 1) 1) 5 5 1 1 7

Curried functions Note difference betweenlx. ly. x - yandint f (int x, int y) { return x - y;} l abstraction is a function of 1 parameter But computationally they are the same (can betransformed into each other) Curry: transform l(x, y). x-y to lx. ly. x - y Uncurry: the reverse of Curry

Free and bound variables lx. x y x: bound variable y: free variableint y; Could be aglobal variable int add(int x) {return x y;}

Free and bound variables lx. x y Bound variable can be renamed (“placeholder”) lx. (x y) is same function as lz. (z y)a-equivalence (x y) is the scope of the binding lxint add(int x) {int add(int z) {return x y;return z y;}x 0; // out of scope!}

Free and bound variables lx. x y Bound variable can be renamed (“placeholder”) lx. (x y) is same function as lz. (z y) (x y) is the scope of the binding lxa-equivalence Name of free variable does matter lx. (x y) is not the same as lx. (x z)int y 10;int y 10;int z 20;int z 20;int add(int x) { return x y; }int add(int x) { return x z; }

Free and bound variables lx. x y Bound variable can be renamed (“placeholder”) lx. (x y) is same function as lz. (z y) (x y) is the scope of the binding lxa-equivalence Name of free variable does matter lx. (x y) is not the same as lx. (x z) Occurrences (lx. x y) (x 1) : x has botha free and a bound occurrenceint x 10;int add(int x) { return x y;}add(x 1);

Formal definitions about free andbound variables Recall M, N :: x lx. M M N fv(M): the set of free variables in Mfv(x)º {x}fv(lx.M) º fv(M) \ {x}fv(M N) º fv(M) È fv(N) Examplefv((lx. x) x) {x}fv((lx. x y) x) {x, y}Defined byinduction on terms

Formal definitions about free andbound variables Recall M, N :: x lx. M M N fv(M): the set of free variables in M “x is a free variable in M”: x Î fv(M) “x is a bound variable in M”: ? a-equivalence:lx. M ly. M[y/x], where y freshSubstitution (defined later)

Main points till now Syntax: notation for defining functions(Terms) M, N :: x lx. M M N Next: semantics (reduction rules)

Overview of reduction Basic rule is b-reduction(lx. M) N M[N/x](Substitution) Repeatedly apply reduction rule to any sub-termExample(lf. lx. f (f x)) (ly. y 1) 5 (lx. (ly. y 1) ((ly. y 1) x)) 5 (lx. (ly. y 1) (x 1)) 5 (lx. (x 1) 1) 5 5 1 1 7

Substitution M[N/x]: replace x by N in M Defined by induction on termsx[N/x] º Ny[N/x] º y(M P)[N/x] º (M[N/x]) (P[N/x])(lx.M)[N/x] º lx.M (Only replace free variables!)(ly.M)[N/x] º ?Because names of boundvariables do not matter

Substitution – avoid name capture Example : (lx. x - y)[x/y]Substitute “blindly”:lx. x - xProblem: unintended name capture!!Solution: rename bound variables before substitution(lx. x - y)[x/y] (lz. z - y)[x/y] lz. z - x

Substitution – avoid name capture Example : (lx. f (f x))[(ly. y x)/f]Substitute “blindly”:lx. (ly. y x) ((ly. y x) x)Problem: x in (ly. y x) got bound – unintended namecapture!!Solution: rename bound variables before substitution(lx. f (f x))[(ly. y x)/f] (lz. f (f z))[(ly. y x)/f] lz. (ly. y x) ((ly. y x) z)

Substitution M[N/x]: replace x by N in Mx[N/x] º Ny[N/x] º y(M P)[N/x] º (M[N/x]) (P[N/x])(lx.M)[N/x] º lx.M(ly.M)[N/x] º ly.(M[N/x]), if y Ï fv(N)z is unused(ly.M)[N/x] º lz.(M[z/y][N/x]), if y Î fv(N) and z freshEasy rule: always rename variables to be distinct

Examples of substitution(lx. (ly. y z) (lw. w) z x)[y/z](lx. (ly. y y) z x)[(f x)/z]

Reduction rulesλ𝑥. 𝑀 𝑁 𝑀[𝑁/𝑥](b)𝑀 𝑀′𝑀 𝑁 𝑀! 𝑁𝑁 𝑁′𝑀 𝑁 𝑀 𝑁′𝑀 𝑀′λ𝑥. 𝑀 λ𝑥. 𝑀′Repeatedly apply(b) to any sub-term

Examples(lf. f x) (ly. y) // apply (b) (f x)[(ly. y)/f] (ly. y) x y[x/y] x// apply (b)

Examples(ly. lx. x - y) x (lx. x - y)[x/y]// apply (b) lz. ((x - y)[z/x][x/y]) lz. ((z - y)[x/y]) lz. z - x

Exampleslx. (ly. y 1) x // 4th rule(ly. y 1) x // (b) rule (y 1)[x/y] lx. x 1 x 1

Examples(lf. lz. f (f z)) (ly. y x)// apply (b) lz. (ly. y x) ((ly. y x) z) // apply (b) and the 3rd &4th rules lz. (ly. y x) (z x) lz. z x x// apply (b) and the 4th rule

Normal formreducible expression b-redex: a term of the form (lx.M) N b-normal form: a term containing no b-redex Stopping point: cannot further apply b-reduction rules(lf. lx. f (f x)) (ly. y 1) 2 ( lx. (ly. y 1) ((ly. y 1) x) ) 2 ( lx. (ly. y 1) (x 1) ) 2 ( lx. x 1 1 ) 2 2 1 1(b-normal form)Can further reduce to 4 if having reduction rules for

Normal form – examples lx. ly. x Yes (lx. ly. x) (lz. z) No lx. (ly. x) (lz. z) No

Confluence (Church-Rosser Property)Terms can be evaluated in any order.Final result (if there is one) is uniquely determined.(lf. lx. f (f x)) (ly. y 1) 2 ( lx. (ly. y 1) ((ly. y 1) x) ) 2 ( lx. (ly. y 1) (x 1) ) 2 ( lx. x 1 1 ) 2 2 1 1(lf. lx. f (f x)) (ly. y 1) 2 ( lx. (ly. y 1) ((ly. y 1) x) ) 2 ( lx. (ly. y 1) (x 1) ) 2 (ly. y 1) (2 1) 2 1 1

Formalizing Confluence Theorem M * M’ : zero-or-more steps of M 0 M’ iff M M’M k 1 M’ iff M’’. M M’’ Ù M’’ k M’M * M’ iff k. M k M’ Confluence Theorem:If M * M1 and M * M2,then there exists M’ such thatM1 * M’ and M2 * M’.inductivedefinitionMM1M2M’

Corollary of Confluence Theorem With a-equivalence, every term has at most onenormal form. Q: If a term has many b-redexes, which b-redexshould be picked? Good news: no matter which is picked, there is atmost one normal form. Bad news: some reduction strategies may fail tofind a normal form.

Non-terminating reduction(lx. x x) (lx. x x) (lx. x x) (lx. x x) (lx. x x y) (lx. x x y) (lx. x x y) (lx. x x y) y (lx. f (x x)) (lx. f (x x)) f ((lx. f (x x)) (lx. f (x x))) Some terms have no normal forms

Term may have both terminating andnon-terminating reduction sequences(lu. lv. v) ((lx. x x)(lx. x x)) lv. v(lu. lv. v) ((lx. x x)(lx. x x)) (lu. lv. v) ((lx. x x)(lx. x x)) Some reduction strategies may fail to find a normal form

Reduction strategies Normal-order reduction: choose the left-most,outer-most redex first(lu. lv. v) ((lx. x x)(lx. x x)) lv. vTheorem:Normal-order reduction willfind normal form if exists Applicative-order reduction: choose the left-most,inner-most redex first(lu. lv. v) ((lx. x x)(lx. x x)) (lu. lv. v) ((lx. x x)(lx. x x))

Reduction strategies – examplesNormal-order(lx. x x) ((ly. y) (lz. z)) ((ly. y) (lz. z)) ((ly. y) (lz. z)) (lz. z) ((ly. y) (lz. z)) (ly. y) (lz. z) lz. zApplicative-order(lx. x x) ((ly. y) (lz. z)) (lx. x x) (lz. z) (lz. z) (lz. z) lz. z

Reduction strategies – examplesNormal-orderApplicative-order(le. lf. e) ((la. lb. a) x y) ((lc. ld. c) u v)

Reduction strategies – examplesApplicative-order may not be as efficient as normal-orderwhen the argument is not used.Normal-orderApplicative-order(lx. p) ((ly. y) (lz. z)) p(lx. p) ((ly. y) (lz. z)) (lx. p) (lz. z) p

Reduction strategies Similar to (but subtly different from) evaluationstrategies in language theoriesarguments are not Call-by-name (like normal-order) ALGOL 60evaluated, butdirectly substitutedinto function body Call-by-need (“memorized version” of call-by-name) Haskell, R, called “lazy evaluation” Call-by-value (like applicative-order) C, called “eager evaluation”

Subtle difference between reductionstrategies and evaluation strategies Normal-order (or applicative-order) reduces underlambda Allow optimizations inside a function body Not always desired lx. ((ly. y y) (ly. y y)) lx. ((ly. y y) (ly. y y)) Evaluation strategies: Don’t reduce under lambda

Evaluation Only evaluate closed terms (i.e. no free variables) May not reduce all the way to a normal form Terminate as soon as a canonical form (i.e. a lambdaabstraction) is obtainedEvaluationterminateshere

Evaluation A closed normal form must be a canonical form Not every closed canonical form is a normal form Recall that normal-order reduction will find thenormal form if it exists If normal-order reduction terminates, the reductionsequence must contain a first canonical form Normal-order evaluation

Normal-order reduction & evaluation Normal-order reduction terminatesEvaluation terminates here Normal-order reduction does not terminateEvaluation terminates hereEvaluation diverges too

Normal-order evaluation rulesλ𝑥. 𝑀 λ𝑥. 𝑀(Term)𝑀 λ𝑥. 𝑀!𝑀! [𝑁/𝑥] 𝑃(b)𝑀𝑁 𝑃

Normal-order evaluation – example

Recall the reduction strategiesNormal-orderApplicative-order(lx. x x) ((ly. y) (lz. z))(lx. x x) ((ly. y) (lz. z)) ((ly. y) (lz. z)) ((ly. y) (lz. z)) (lx. x x) (lz. z) (lz. z) ((ly. y) (lz. z)) (lz. z) (lz. z) (ly. y) (lz. z) lz. z lz. zEager evaluation:Postpone the substitution untilthe argument is a canonical form.No need to reduce many copiesof the argument separately.

Eager evaluation rulesλ𝑥. 𝑀 " λ𝑥. 𝑀𝑀 " λ𝑥. 𝑀!(Term)𝑁 " 𝑁 !𝑀! [𝑁′/𝑥] " 𝑃(b)𝑀 𝑁 " 𝑃

Eager evaluation– example

Normal-order evaluation rules(small-step)(λ𝑥. 𝑀) 𝑁 𝑀[𝑁/𝑥]𝑀 𝑀!𝑀 𝑁 𝑀! 𝑁(b)

Eager evaluation rules (small-step)λ𝑥. 𝑀 (λy. 𝑁) 𝑀[(λy. 𝑁)/𝑥]𝑀 𝑀!𝑀 𝑁 𝑀! 𝑁𝑁 𝑁!λ𝑥. 𝑀 𝑁 (λ𝑥. 𝑀) 𝑁′(b)

Main points till now Syntax: notation for defining functions(Terms) M, N :: x lx. M M N Semantics (reduction rules)(lx. M) N M[N/x](b) Next: programming in l-calculus Encoding data and operators in “pure” l-calculus(without adding any additional syntax)

Programming in l-calculus Encoding Boolean values and operators True º lx. ly. x False º lx. ly. y

Programming in l-calculus Encoding Boolean values and operators True º lx. ly. x False º lx. ly. y not º

Programming in l-calculus Encoding Boolean values and operators True º lx. ly. x False º lx. ly. y not º lb. b False Truenot True True False True Falsenot False False False True True

Programming in l-calculus Encoding Boolean values and operators True º lx. ly. x False º lx. ly. y not º lb. b False True and º

Programming in l-calculus Encoding Boolean values and operators True º lx. ly. x False º lx. ly. y not º lb. b False True and º lb. lb’. b b’ Falseand True b * True b False band False b * False b False False