南京大学：高等数学微积分课程教学资源（PPT课件讲稿）拉姆达演算 Lambda Calculus（λ演算 λ-calculus）

Lambda calculus

Lambda Calculus

What is入- calculus Programming language Invented in 1930s, by alonzo Church and stephen cole Kleene Model for computation lan Turing, 1937 Turing machines equal n-calculus in expressiveness

What is -calculus • Programming language • Invented in 1930s, by Alonzo Church and Stephen Cole Kleene • Model for computation • Alan Turing, 1937: Turing machines equal -calculus in expressiveness

Why learn n-calculus Foundations of functional programming Lisp, ML, Haskell often used as a core language to study language theories ype system intx=0: Scope and binding for(inti=0;i<10;i++){x++;} Higher-order functions x="abcd"; // bug(mistype) Denotational semantics i+;∥bug( out of scope) Program equivalence How to formally define and rule out these bugs?

Why learn -calculus • Foundations of functional programming • Lisp, ML, Haskell, … • Often used as a core language to study language theories • Type system • Scope and binding • Higher-order functions • Denotational semantics • Program equivalence • … int x = 0; for (int i = 0; i < 10; i++) { x++; } x = “abcd”; // bug (mistype) i++; // bug (out of scope) How to formally define and rule out these bugs?

Overview: -calculus as a language Syntax How to write a program? Keyword ?"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

Overview: -calculus as a language • Syntax • How to write a program? • Keyword “” 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 n terms or 2 expressions (Terms)M,N: =X AX.M MN Lambda abstraction(x. M: anonymous"functions ntf(ntx){ return x;}→λx.x Lambda application (M n) int f (int x)i return x; y f(3) (xx)3=3

Syntax •  terms or  expressions: (Terms) M, N ::= x | x. M | M N • Lambda abstraction (x.M): “anonymous” functions int f (int x) { return x; } ➔ x. x • Lambda application (M N): int f (int x) { return x; } f(3); ➔ (x. x) 3 = 3

Syntax ·^ terms orλ expressions: erms)M,N:=X|λx.M|MN pure n-calculus Add extra operations and data types X.(X+1) AZ.(x+2*y+2) (入.(x+1)3=3+1 ·(2.(X+2*y+z)5=x+2*y+5

Syntax •  terms or  expressions: (Terms) M, N ::= x | x. M | M N • pure -calculus • Add extra operations and data types • x. (x+1) • z. (x+2*y+z) • (x. (x+1)) 3 = 3+1 • (z. (x+2*y+z)) 5 = x+2*y+5

Conventions Body of n extends as far to the right as possible nx MN means Ax(M N, not(x M)N 入X.fx=λx.(fx) 入X.f.fx=x.(ffx) Function applications are left-associative MNP means(M N)P, not M(N P (入X.y.X-y)53=(x.y.x-y)5)3 (fx.fx)(X.X+1)2=((千.AX.fx)(^x,X+1))2

Conventions • Body of  extends as far to the right as possible x. M N means x. (M N), not (x. M) N • x. f x = x. ( f x ) • x. f. f x = x. ( f. f x ) • Function applications are left-associative M N P means (M N) P, not M (N P) • (x. y. x - y) 5 3 = ( (x. y. x - y) 5 ) 3 • (f. x. f x) (x. x + 1) 2 = ( (f. x. f x) (x. x + 1) ) 2

Higher-order functions Functions can be returned as return values 入xyx-y Functions can be passed as arguments 06×.×)(xx+1)2 Think about function pointers in C/C++

Higher-order functions • Functions can be returned as return values • Functions can be passed as arguments Think about function pointers in C/C++. x. y. x - y (f. x. f x) (x. x + 1) 2

Higher-order functions Given function f return function fo f 入.X.f(fx) · How does this work? xf.2.f(fx)y+1)5 =(x、+)(x.y+1)×)5 (X.(y+1)(x+1)5 (入X.(x+1)+1)5 5+1+1=7

Higher-order functions • Given function f, return function f ∘ f f. x. f (f x) • How does this work? (f. x. f (f x)) (y. y+1) 5 = (x. (y. y+1) ((y. y+1) x)) 5 = (x. (y. y+1) (x+1)) 5 = (x. (x+1)+1) 5 = 5+1+1 = 7

Curried functⅰonS Note difference between 入X.xy.x-y and int f (int x, int yi return x-y; n abstraction is a function of 1 parameter But computationally they are the same(can be transformed into each other Curry: transform n(x,y). x-y to nx. ny x-y Uncurry: the reverse of curry

Curried functions • Note difference between •  abstraction is a function of 1 parameter • But computationally they are the same (can be transformed into each other) • Curry: transform (x, y). x-y to x. y. x - y • Uncurry: the reverse of Curry x. y. x - y and int f (int x, int y) { return x - y;}