南京大学：《程序设计语言的形式语义》课程教学资源（课件讲稿）04_Lambda Calculus

Lambda Calculus

Lambda Calculus

What isλ-calculus Programming language Invented in 1930s,by Alonzo Church and Stephen Cole Kleene Model for computation Alan Turing,1937:Turing machines equal A-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λ-calculus Foundations of functional programming ·Lisp,ML,Haskell,. Often used as a core language to study language theories ·Type system int x=0; ·Scope and binding for (int i=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:A-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 ·入terms or入expressions: (Terms)M,N :x x.M MN Lambda abstraction(Ax.M):"anonymous"functions intf(intx){return x;}→入x.x Lambda application (M N): int f (int x){return x;} f3: →(x.x)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: (Terms)M,N:=x入x.MMN ·pure入-calculus Add extra operations and data types ·2x.(X+1) ·入z.(x+2*y+z) ·(2×.(x+1)3=3+1 ·(2z.(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 extends as far to the right as possible Ax.M N means Ax.(M N),not (x.M)N ·入x.fx=入x.(fx) ·x.入f.fx=入x.(入f.fx) Function applications are left-associative MN P means(M N)P,not M(N P) ·(2x.y.x-yW53=((x.y.x-y)5)3 ·(2f.入x.fx)(x.x+1)2=((2f.入x.fx)(2x.×+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 x(y.×-y Functions can be passed as arguments (f.2x.fx)⑦x.x+12 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 入f.2x.f(fx) ·How does this work? (2f.x.f(fx)(y.y+1)5 =(x.(y.y+1)(y.y+1)X)5 =(2x.(2y.y+1)(+1)5 =(2x.(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 functions Note difference between x.y.×-y and int f (int x,int y)return x-y;} 。入abstraction is a function of 1 parameter But computationally they are the same (can be transformed into each other) ·Curry:transform(x,y).x-yto入x.y.×-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;}