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