Lambda Calculus Principles of Programming Languages
Explore the foundational concepts of Lambda Calculus in Principles of Programming Languages at Arizona State University. Understand Function Application, Anonymous Functions, and more derived from Lambda Calculus.
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 CSE 340 Principles of Programming Languages Spring 2016 Adam Doup Arizona State University http://adamdoupe.com
Lambda Calculus Language to express function application Ability to define anonymous functions Ability to "apply" functions Functional programming derives from lambda calculus ML Haskell F# Clojure 2 Adam Doup , Principles of Programming Languages
History Frege in 1893 studied the use of functions in logic Sch nfinkel, in the 1920s, studied how combinators, a specific type of function, could be applied to formal logic Church introduced lambda calculus in the 1930s Original system was shown to be logically inconsistent in 1935 by Kleene and Rosser In 1936, Church published the lambda calculus that is relevant to computation Refined further Type systems, Adapted from Jesse Alama: http://plato.stanford.edu/entries/lambda-calculus/#BriHisLCal 3 Adam Doup , Principles of Programming Languages
Syntax Everything in lambda calculus is an expression (E) E ID E ID . E E E E E (E) 4 Adam Doup , Principles of Programming Languages
Examples E ID E ID . E E E E E (E) x x . x x y x . y x . y z foo bar . (foo (bar baz)) 5 Adam Doup , Principles of Programming Languages
Ambiguous Syntax How to parse x y z Exp Exp x Exp z Exp z y x y 6 Adam Doup , Principles of Programming Languages
Ambiguous Syntax How to parse x . x y Exp Exp Exp Exp x Exp y x Exp Exp Exp x x y 7 Adam Doup , Principles of Programming Languages
Disambiguation Rules E E E is left associative x y z is (x y) z w x y z is ((w x) y) z ID . E extends as far to the right as possible, starting with the ID . x . x y is x . (x y) x . x . x is x. ( x . x) 8 Adam Doup , Principles of Programming Languages
Examples ( x . y) x is the same as x . y x No! ( x . y) x x . (x) y is the same as x . ((x) y) a . b . c . a b c a . ( b . ( c . ((a b) c))) 9 Adam Doup , Principles of Programming Languages
Semantics Every ID that we see in lambda calculus is called a variable E ID . E is called an abstraction The ID is the variable of the abstraction (also metavariable) E is called the body of the abstraction E E E This is called an application 10 Adam Doup , Principles of Programming Languages
Semantics ID . E defines a new anonymous function This is the reason why anonymous functions are called "Lambda Expressions" in Java 8 (and other languages) ID is the formal parameter of the function Body is the body of the function E E1 E2, function application, is similar to calling function E1 and setting its formal parameter to be E2 11 Adam Doup , Principles of Programming Languages
Example Assume that we have the function + defined and the constant 1 x . + x 1 Represents a function that adds one to its argument ( x . + x 1) 2 Represents calling the original function by supplying 2 for x and it would "reduce" to (+ 2 1) = 3 How can + function be defined if abstractions only accept 1 parameter? 12 Adam Doup , Principles of Programming Languages
Currying Technique to translate the evaluation of a function that takes multiple arguments into a sequence of functions that each take a single argument Define adding two parameters together with functions that only take one parameter: x . y . ((+ x) y) ( x . y . ((+ x) y)) 1 y . ((+ 1) y) ( x . y . ((+ x) y)) 10 20 ( y . ((+ 10) y)) 20 ((+ 10) 20) = 30 13 Adam Doup , Principles of Programming Languages
Free Variables A variable is free if it does not appear within the body of an abstraction with a metavariable of the same name x free in x . x y z? y free in x . x y z? x free in ( x . (+ x 1)) x? z free in x . y . z . z y x? x free in ( x . z foo) ( y . y x)? 14 Adam Doup , Principles of Programming Languages
Free Variables x is free in E if: E = x E = y . E1, where y != x and x is free in E1 E = E1 E2, where x is free in E1 E = E1 E2, where x is free in E2 15 Adam Doup , Principles of Programming Languages
Examples x free in x x . x ? x free in ( x . x y) x ? x free in x . y x ? 16 Adam Doup , Principles of Programming Languages
Combinators An expression is a combinator if it does not have any free variables x . y . x y x combinator? x . x combinator? z . x . x y z combinator? 17 Adam Doup , Principles of Programming Languages
Bound Variables If a variable is not free, it is bound Bound by what abstraction? What is the scope of a metavariable? 18 Adam Doup , Principles of Programming Languages
Bound Variable Rules If an occurrence of x is free in E, then it is bound by x . in x . E If an occurrence of x is bound by a particular x . in E, then x is bound by the same x . in z . E Even if z == x x . x . x Which lambda expression binds x? If an occurrence of x is bound by a particular x . in E1, then that occurrence in E1 is tied by the same abstraction x . in E1 E2 and E2 E1 19 Adam Doup , Principles of Programming Languages
Examples ( x . x ( y . x y z y) x) x y ( x . x ( y . xy z y) x) x y ( x . y . x y) ( z . x z) ( x . y . xy) ( z . x z) ( x . x x . z x) ( x . x x . z x) 20 Adam Doup , Principles of Programming Languages
Equivalence What does it mean for two functions to be equivalent? y . y = x . x ? x . x y = y . y x ? x . x = x . x ? 21 Adam Doup , Principles of Programming Languages
-equivalence -equivalence is when two functions vary only by the names of the bound variables E1 = E2 We need a way to rename variables in an expression Simple find and replace? x . x y . x y z Can we rename x to foo? Can we rename y to bar? Can we rename y to x? Can we rename x to z? 22 Adam Doup , Principles of Programming Languages
Renaming Operation E {y/x} x {y/x} = y z {y/x} = z, if x z (E1 E2) {y/x} = (E1 {y/x}) (E2 {y/x}) ( x . E) {y/x} = ( y . E {y/x}) ( z . E) {y/x} = ( z . E {y/x}), if x z Material courtesy of Peter Selinger http://www.mathstat.dal.ca/~selinger/papers/lambdanotes.pdf 23 Adam Doup , Principles of Programming Languages
Examples ( x . x) {foo/x} ( foo . (x) {foo/x}) ( foo . (foo)) (( x . x ( y . x y z y) x) x y) {bar/x} ( x . x ( y . x y z y) x) {bar/x} (x) {bar/x} (y) {bar/x} ( x . x ( y . x y z y) x) {bar/x} (x) {bar/x} y ( x . x ( y . x y z y) x) {bar/x} bar y ( bar . (x ( y . x y z y) x) {bar/x}) bar y ( bar . (bar ( y . x y z y) {bar/x} bar)) bar y ( bar . (bar ( y . (x y z y) {bar/x} ) bar)) bar y ( bar . (bar ( y . (bar y z y)) bar)) bar y 24 Adam Doup , Principles of Programming Languages
-equivalence For all expressions E and all variables y that do not occur in E x . E = y . (E {y/x}) y . y = x . x ? (( x . x ( y . x y z y) x) x y) = (( y . y ( z . y z w z) y) y x) ? 25 Adam Doup , Principles of Programming Languages
Substitution Renaming allows us to replace one variable name with another However, our goal is to reduce ( x . + x 1) 2 to (+ 1 2), which replaces x with the expression 2 Can we use renaming? We need another operator, called substitution, to replace a variable by a lambda expression E[x N], where E and N are lambda expressions and x is a name 26 Adam Doup , Principles of Programming Languages
Substitution Seems simple, right? (+ x 1) [x 2] (+ 2 1) ( x . + x 1) [x 2] ( x . + x 1) ( x . y x) [y z . x z] ( x . ( z . x z) x) ( w . ( z . x z) w) 27 Adam Doup , Principles of Programming Languages
Substitution Operation E [x N] x [x N] = N y [x N] = y, if x y (E1 E2) [x N] = (E1 [x N]) (E2 [x N]) ( x . E) [x N] = ( x . E) ( y . E) [x N] = ( y . E [x N]) if x y and y is not a free variable in N ( y . E) [x N] = ( y' . E {y'/y} [x N]) if x y, y is a free variable in N, and y' is a fresh variable name 28 Adam Doup , Principles of Programming Languages
Examples ( x . x) [x foo] ( x . x) (+ 1 x) [x 2] (+[x 2] 1[x 2] x[x 2]) (+ 1 2) ( x . y x) [y z . x z] ( w . (y x){w/x} [y z . x z]) ( w . (y w) [y z . x z]) ( w . (y [y z . x z] w [y z . x z]) ( w . ( z . x z) w) 29 Adam Doup , Principles of Programming Languages
Examples (x ( y . x y)) [x y z] (x [x y z] ( y . x y) [x y z]) ((y z) ( y . x y) [x y z]) (y z) ( q . (x y){q/y}[x y z]) (y z) ( q . (x q)[x y z]) (y z) ( q . ((y z) q)) 30 Adam Doup , Principles of Programming Languages
Execution Execution will be a sequence of terms, resulting from calling/invoking functions Each step in this sequence is called a -reduction We can only -reduce a -redux (expressions in the application form) ( x . E) N -reduction is defined as: ( x . E) N -reduces to E[x N] -normal form is an expression with no reduxes Full -reduction is reducing all reduxes regardless of where they appear 31 Adam Doup , Principles of Programming Languages
Examples ( x . x) y x[x y] y ( x . x ( x . x)) (u r) (x ( x . x))[x (u r)] (u r) ( x . x) 32 Adam Doup , Principles of Programming Languages
Examples ( x . y) (( z . z z) ( w . w)) ( x . y) (z z)[z ( w . w)] ( x . y) (( w . w) ( w . w)) ( x . y) (w)[w ( w . w)] ( x . y) ( w . w) y[x ( w . w)] y 33 Adam Doup , Principles of Programming Languages
Examples ( x . x x) ( x . x x) (x x)[x ( x . x x)] ( x . x x) ( x . x x) (x x)[x ( x . x x)] ( x . x x) ( x . x x) 34 Adam Doup , Principles of Programming Languages
Boolean Logic T = ( x . y . x) F = ( x . y . y) and = ( a . b . a b F) and T T ( a . b . a b ( x . y . y)) 35 Adam Doup , Principles of Programming Languages
and T T ( a . b . a b ( x . y . y)) ( x . y . x) ( x . y . x) ( b . a b ( x . y . y))[a ( x . y . x)] ( x . y . x) ( b . ( x . y . x) b ( x . y . y)) ( x . y . x) (( x . y . x) b ( x . y . y))[b ( x . y . x)] ( x . y . x) ( x . y . x) ( x . y . y) ( y . x)[x ( x . y . x)] ( x . y . y) ( y . ( x . y . x)) ( x . y . y) ( x . y . x)[y ( x . y . y)] ( x . y . x) T 36 Adam Doup , Principles of Programming Languages
and T F ( a . b . a b F) T F ( b . a b F)[a T] F ( b . T b F) F (T b F)[b F] (T F F) ( x . y . x) F F ( y . x)[x F] F ( y . F) F F[y F] F 37 Adam Doup , Principles of Programming Languages
and F T ( a . b . a b F) F T F T F F 38 Adam Doup , Principles of Programming Languages
and F F ( a . b . a b F) F F F F F F 39 Adam Doup , Principles of Programming Languages
not not T = F not F = T not = ( a . a F T) not T ( a . a F T) T T F T F not F ( a . a F T) F F F T T 40 Adam Doup , Principles of Programming Languages
If Branches if c then a else b if c a b if T a b = a if F a b = b if = ( a . a) 41 Adam Doup , Principles of Programming Languages
Examples if T a b ( a . a) T a b T a b a if F a b ( a . a) F a b F a b b 42 Adam Doup , Principles of Programming Languages
Church's Numerals 0 = f . x . x 1 = f . x . f x 2 = f . x . f (f x) 3 = f . x . f (f (f x)) 4 = f . x . f (f (f (f x))) f . x . (f (f (f (f x)))) 4 a b a (a (a (a b))) 43 Adam Doup , Principles of Programming Languages
Successor Function succ = n . f . x . f (n f x) 0 = f . x . x succ 0 ( n . f . x . f (n f x)) 0 f . x . f (0 f x) f . x . f (( f . x . x) f x) f . x . f x 1 = f . x . f x succ 0 = 1 44 Adam Doup , Principles of Programming Languages
Successor Function succ = n . f . x . f (n f x) 1 = f . x . f x succ 1 ( n . f . x . f (n f x)) 1 f . x . f (1 f x) f . x . f (( f . x . f x) f x) f . x . f (f x) 2 = f . x . f (f x) succ 1 = 2 succ n = n + 1 45 Adam Doup , Principles of Programming Languages
Addition add 0 1 = 1 add 1 2 = 3 add = n . m . f . x . n f (m f x) add 0 1 ( n . m . f . x . n f (m f x)) 0 1 ( m . f . x . 0 f (m f x)) 1 f . x . 0 f (1 f x) f . x . 0 f (f x) f . x . f x 46 Adam Doup , Principles of Programming Languages
Addition add = n . m . f . x . n f (m f x) add 1 2 ( n . m . f . x . n f (m f x)) 1 2 ( m . f . x . 1 f (m f x)) 2 f . x . 1 f (2 f x) f . x . 1 f (f (f x)) f . x . (f (f (f x))) 3 47 Adam Doup , Principles of Programming Languages
Multiplication mult 0 1 = 0 mult 1 2 = 2 mult 2 5 = 10 mult = n . m . m (add n) 0 mult 0 1 ( n . m . m (add n) 0) 0 1 ( m . m (add 0) 0) 1 1 (add 0) 0 add 0 0 0 48 Adam Doup , Principles of Programming Languages
Multiplication mult 1 2 ( n . m . m (add n) 0) 1 2 ( m . m (add 1) 0) 2 2 (add 1) 0 (add 1) ((add 1) 0) (add 1) (add 1 0) (add 1) (1) (add 1 1) 2 49 Adam Doup , Principles of Programming Languages
Turing Complete? We have Boolean logic Including true/false branches We have arithmetic What does it mean for lambda calculus to be Turing complete? 50 Adam Doup , Principles of Programming Languages
