Complete Computational Model and Functional Programming Assembly Language
Explore the Lambda Calculus, a powerful and concise computational model invented by Alonzo Church. Learn about its applications, examples, and how it serves as an assembly language for functional programming with its ability to explain various programming language features.
Download Presentation
Please find below an Image/Link to download the presentation.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author. If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
You are allowed to download the files provided on this website for personal or commercial use, subject to the condition that they are used lawfully. All files are the property of their respective owners.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.
E N D
Presentation Transcript
Lambda Calculus Mooly Sagiv (original slides by Kathleen Fisher, John Mitchell, Oded Padon, Shachar Itzhaky, S. Tanimoto , Stephen A. Edwards) Benjamin Pierce Types and Programming Languages http://www.cs.cornell.edu/courses/cs3110/2008fa/recitations/rec26.html
Computation Models Turing Machines Wang Machines Counter Programs Lambda Calculus
Alonzo Church 1903 1995 Professor at Princeton (1929 1967) and UCLA (1967 1990) Invented the Lambda Calculus Notable students: Alan Turing Stephen Cole Kleene Martin Davis Barkley Roser Dana Scott Leon Hankin Michael Rabin John Kemeny
Simple Example factorial C int fact(int x) { if (x==0) return 1; else return n * fact(n-1); } No state mutations ML fact x : int : int = if x=0 then 1 else n * fact n-1 No state mutations Expression only
Another Example Compose comp f: int int g: int int: int int = fun x g (f x) comp fun x x + 1 fun x x + 1 comp fun x x + 1 fun x x + 1 2 comp fun x 2 *x fun y 4 * y comp fun x 2 *x fun y 4 * y 3
What is calculus A complete computational model An assembly language for functional programming Powerful Concise Counterintuitive Can explain many interesting PL features
Basics Repetitive expressions can be compactly represented using functional abstraction Example: (5 * 4* 3 * 2 * 1) + (7 * 6 * 5 * 4 * 3 * 2 *1) = factorial(5) + factorial(7) factorial(n) = if n = 0 then 1 else n * factorial(n-1) factorial= n. if n = 0 then 1 else n * factorial(n-1) factorial= n. if n = 0 then 1 else n * apply (factorial (n-1))
Lambda Expressions Function application are written in prefix form Add 4 to 5 Evaluation: Select a redex and apply function (+(* 5 6) (* 8 3)) (+ 4 5) (+ 30 (* 8 3)) (+( 30 24) 54 Different evaluation orders (+(* 5 6) (* 8 3)) (+(* 5 6 ) 24) (+ 30 24) 54 Simon Peyton Jones, The Implementation of Functional Programming Languages, Prentice-Hall, 1987.
Function Application and Currying Function application written as juxtaposition f x Every function has exactly one argument Multiple arguments can be simulated by Curring (+ x) is a function which adds x to its argument (+ 4 5) = (+4) 5 9 What is +4? What is +
Lambda Abstraction The only other thing in the lambda calculus is lambda abstraction a notation for defining unnamed functions ( x. + x 1) The function of x that adds 1 to x
Boolean Expressions (if true x y) x (if false x y) y Boolean negation? Boolean conjunction Boolean disjunction
Beta Reduction Substitute formal by actual arguments ( x. + x 1) 4 ( + 4 1) 5 x can occur multiple times ( x. + x x) 4 ( + 4 4) 8 Or not at all ( x. + 1 6) 4 ( + 1 6) 7
Beta-Reduction(Cont) Fuzzy but mechanical Extra parenthesis and tree-notations can help = ( x. y. + x y) 3 4 (( x.( y. ((+ x) y))) 3) 4 ( y. ((+ 3) y)) 4 ((+ 3) 4) 7
Functions can be arguments Arbitrary functions as arguments/return ( f. f 3) ( x. + x 1) ( x. + x 1) 3 ( x. + x 1) 3 (+ 3 1) 4
Free and Bound Variables x. (+ x y) 2 x is bound y is free Determined in the enclosed context Like global variables Both x and y are free in (+ x y)
Untyped Lambda Calculus t ::= terms x variable x. t abstraction t t application Terms can be represented as abstract syntax trees apply Syntactic Conventions apply Applications associates to left e1 e2 e3 (e1 e2) e3 The body of abstraction extends as far as possible e1 e2 e3 x. y. x y x x. ( y. (x y) x)
Untyped Lambda Calculus t ::= terms x variable x. t abstraction t t application Terms can be represented as abstract syntax trees Syntactic Conventions x y Applications associates to left e1 e2 e3 (e1 e2) e3 The body of abstraction extends as far as possible apply apply x y x x. y. x y x x. ( y. (x y) x)
Untyped Lambda Calculus++ t ::= terms x variable x. t abstraction t t application number number op t1 t2 tk true built-in operator op t1, t2, , tk true false false
Lambda Calculus in Python ( x. x) y (lambda x: x) (y)
Lambda Calculus in ML ( x. x) y (fun x x) (y)
Functions on int x x. succ x apply succ x apply ( x. succ x) 0 x 0 apply 1 x succ Define a function which computes 2?
Ill-Formed Beta Reductions Sometimes beta-reductions cannot be applied Like runtime error/undefined semantics in imperative programs (1 5) (x 5 y. y) (+ true 2) (test 5 1 2) Later will refine lambda calculus to avoid such terms by the compiler
Substitution Replace a term by a term x + ((x + 2) * y)[x 3, y 7] = ? x + ((x + 2) * y)[x z + 2] = ? x + ((x + 2) * y)[t z + 2] = ? x + ((x + 2) * y)[x y] More tricky in programming languages Why?
Free vs. Bound Variables An occurrence of x is bound in t if it occurs in x. t otherwise it is free x is a binder Examples Id= x. x y. x (y z) z. x. y. x (y z) ( x. x) x FV: t 2Var is the set free variables of t FV(x) = {x} FV( x. t) = FV(t) {x} FV (t1 t2) = FV(t1) FV(t2)
Beta-Reduction ( x. t1) t2 [x t2] t1 ( -reduction) [x s] x = s if y x [x s] y = y [x s] ( x. t1) = x. t1 [x s] ( y. t1) = y. [x s] t1 [x s] (t1 t2) = ([x s] t1) ([x s] t2) if y x and y FV(s) [x s] y y [x s] t1 t1
Beta-Reduction ( x. t1) t2 [x t2] t1 ( -reduction) [x s] x = s if y x [x s] y = y [x s] ( y. t1) = y. [x s] t1 [x s] (t1 t2) = ([x s] t1) ([x s] t2) if y x and y FV(s) [x s] apply apply t2 t1 [x s] t2 [x s] t1
Example Beta-Reduction ( x. t1) t2 [x t2] t1 redex ( -reduction) ( x. x) y y apply [x y] x y y x x
Example Beta-Reduction (ex 2) ( x. t1) t2 [x t2] t1 redex ( -reduction) ( x. x ( x. x) ) (u r) apply x apply apply x apply x apply x r u apply u apply r apply u r u r x x x x x x x x x
Example Beta-Reduction (ex 2) (cont) ( x. t1) t2 [x t2] t1 redex ( -reduction) ( x. x ( x. x) ) (u r) u r ( x. x) apply apply x apply u r x apply x apply u x r u x r
Alpha- Renaming Alpha conversion: Renaming of a bound variable and its bound occurrences x. y.y x. z.z Simplifies terms 31
Example Beta-Reduction (ex 2) with renaming ( x. t1) t2 [x t2] t1 redex ( -reduction) ( x. x ( x. x) ) (u r)
Example Beta-Reduction (ex 3) ( x. t1) t2 [x t2] t1 redex ( -reduction) ( x. ( w. x w)) (y z) w. y z w x apply w apply x apply x z y apply w z y w y z apply apply apply w x w x w x
Simple Exercise Adding scopes to expressions Proposed syntax let x = t1 in t2 Informal meaning: all the occurrences of x in t2 are replaced by t1 Example: let a = x. ( w. x w) in a a = How can we simulate let?
Divergence ( x. t1) t2 [x t2] t1 ( x.y) (( x.(x x)) ( x.(x x))) ( -reduction) Apply Apply x x x y Apply Apply x x x x
Divergence ( x. t1) t2 [x t2] t1 ( x.(x x)) ( x.(x x)) ( -reduction) Apply Apply x x x x Apply Apply Apply Apply x x x x x x x x
Different Evaluation Orders ( x. t1) t2 [x t2] t1 ( x.y) (( x.(x x)) ( x.(x x))) ( -reduction) Apply Apply Apply Apply x x x x x x y y Apply Apply Apply Apply x x x x x x x x
Different Evaluation Orders ( x. t1) t2 [x t2] t1 ( x.y) (( x.(x x)) ( x.(x x))) ( -reduction) Apply Apply x x x y y Apply Apply x x x x
Different Evaluation Orders ( x. t1) t2 [x t2] t1 ( x.y) (( x.(x x)) ( x.(x x))) ( -reduction) Apply def f(): Apply x while True: pass x x y def g(x): return 2 Apply Apply x x x x print g(f())
Different Evaluation Orders ( x. t1) t2 [x t2] t1 ( -reduction) id (id ( z. id z)) ( x. x) (( x. x) ( z. ( x. x) z)) Apply Apply x z x x Apply x x z x
Order of Evaluation Full-beta-reduction All possible orders Applicative order call by value (Eager) Left to right Fully evaluate arguments before function Normal order The leftmost, outermost redex is always reduced first Call by name Evaluate arguments as needed Call by need Evaluate arguments as needed and store for subsequent usages Implemented in Haskel
Different Evaluation Orders ( x. y. ( z. z) y) (( u. u) ( w. w)) Apply x Apply u y w u Apply w z y z
Call By Value ( x. y. ( z. z) y) (( u. u) ( w. w)) y Apply Apply x w x Apply Apply z y u y y w w z u Apply Apply w z z y y z z
Call By Name (Lazy) ( x. y. ( z. z) y) (( u. u) ( w. w)) y Apply x Apply Apply z y u y w z u Apply w z y z
Normal Order ( x. y. ( z. z) y) (( u. u) ( w. w)) y Apply y x Apply Apply z y u y w y z u Apply w z y z
Call-by-value Small-step Operational Semantics terms t ::= v ::= values x variable x. t abstraction values x. t abstraction other values t t application ( x. t1) v2 [x v2] t1 (E-AppAbs) t1 t 1 t1 t2 t 1 t2 (E-APPL1) t2 t 2 (E-APPL2) v1 t2 v1t 2
Call By Value ( x. y. ( z. z) y) (( u. u) ( w. w)) y Apply Apply x w x Apply Apply z y u y y w w z u Apply Apply w z z y y z z
Call By Value OS ( x. y. ( z. z) y) (( u. u) ( w. w)) E-AppAbs Apply w u w v2 w u w t1
Call By Value OS (2) v1 t2 ( x. y. ( z. z) y) (( u. u) ( w. w)) Apply w u w w Apply u w Apply w x x Apply y w u y w E-Appl2 Apply u Apply w z y z y z z
Call By Value OS (3) ( x. y. ( z. z) y) (( u. u) ( w. w)) EAppAbs y Apply v2 t1 Apply w x z y y w z Apply z y z
