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