Introduction to the λ-calculus Part II. iszero Predicate - PDF

Introduction to the λ-calculus Part II CS209 - Functional Programming Dr. Greg Lavender Department of Computer Science Stanford University iszero Predicate Test for zero iszero = λn.n(λx.f)t iszero 0 =

Please download to get full document.

View again

of 8
All materials on our website are shared by users. If you have any questions about copyright issues, please report us to resolve them. We are always happy to assist you.

Small Business & Entrepreneurship

Publish on:

Views: 28 | Pages: 8

Extension: PDF | Download: 0

Introduction to the λ-calculus Part II CS209 - Functional Programming Dr. Greg Lavender Department of Computer Science Stanford University iszero Predicate Test for zero iszero = λn.n(λx.f)t iszero 0 = (λn.n(λx.f)t) λsz.z = (λsz.z) (λx.f)t = T iszero S0 = (λn.n(λx.f)t) λsz.s(z) = (λsz.s(z)) (λx.f)t = (λx.f)t = F convince yourself that iszero Sn always returns F 2 1 Ordered Pairs Lambda expressions for ordered pairs fst = λp.p T = λp.p (λtf.t) snd = λp.p F = λp.p (λtf.f) (E 1, E 2 ) = λf.f E 1 E 2 fst (E1, E2) = (λ (E 1, E 2 ) = (E 1, E 2 ) T = (λf.f E 1 E 2 ) T = T E 1 E 2 = (λtf.t) E 1 E 2 = E 1 Similarly for snd (E 1, E 2 ) 3 n-tuples Tuples are defined in terms of pairs (E 1,E 2,, E n ) = (E 1, (E 2, ( (E n-1, E n ) ))) E 1 = fst E E 2 = fst(snd E) E i = fst(snd(snd( (snd E) ))) if i n E n = snd(snd( (snd E) ))) n-1 applications of snd (E 1,E 2,,E n ) 2 = (E 1,(E 2,( ))) 2 = fst (snd(e 1, (E 2, ( )))) = fst (E 2,( )) = E 2 Prove that (E 1,E 2,,E n ) i = E i for 1 = i = n 4 2 Predecessor function Predecessor is subtraction by 1 BUT, pred 0 = 0 pred = λn f x. snd(n (prefn f) (T, x)) where prefn is defined as: prefn = λf p. (F, (fst p - snd p (f (snd p)))) where (E - E 1 E 2 ) is syntactic sugar for (test E E 1 E 2 ) Show that: pred (succ n) = n pred 0 = 0 5 Fixed points A fixed point is a value x in the domain of a function that is the same in the range f(x). Every value in the domain of the identity function is a fixed point λx.x = x can you think of others? factorial(1) = 1 fibonacci(0) = 0, fibonacci(1) = 1 square(0) = 0, square(1) = 1 abs(x) = x, if x = 0 sin(0) = 0 Functionals may also have fixed points D x (e x ) = e x 6 3 Some Computability Theory Godel numbering every program is represented by a finite string of symbols: P = int main() { printf ( Hello world\n ); } a general algorithm can be defined that converts any program into a unique natural number e, called the godel number of the program godel(p) = e for any Turing machine M representing a program, we can assign it a Godel number e and denote the Turing machine that computes that program by M e Let U be a Turing machine that using inputs e and x computes M e (x): call e the program and x the input to program e U = if (e is a program) then M e (x) else output 0 U is thus a universal Turing machine this is the key idea that led John von Neumann to invent the stored program concept used in modern computers 7 Godel Numbering Function How do we write a Godel numbering function? a program is just a sequence of characters from some alphabet. For example, the ASCII alphabet has 128 characters: map chr [0..127]= \NUL\SOH\STX\ETX\EOT\ENQ\ACK\a\b\t\n\v\f\r\SO\SI\DLE\DC1\DC2\DC3\DC cdefghijklmnopqrstuvwxyz{ }~\DEL define a n-degree polynomial where each coefficient is the integer value of the corresponding ascii character and x is the size of the alphabet: P(x) = a n x n + a n-1 x n a 1 x + a 0 for any given program text convert it to an array of ascii values and use those values as the coefficients a n a 0 then evaluate the polynomial with x = 128 using Horner s rule 8 4 Godel Numbering Function Here is an example in Haskell ascii :: [Char] - [Integer] ascii s = map fromintegral (map ord s) -- horner s rule for evaluating a polynomial horner :: (Num a) = a - [a] - a horner x (y:ys) = foldl (\h a - a + (x * h)) y ys godel :: String- Integer godel p = horner 128 (ascii p) godel int main() {printf(\ hello, world\n\ ); } = Kleene s Fixed Point Theorem Also known as Kleene s recursion theorem let φ e = λx.u(e,x) For every computable function f there is a number n such that φ n = φ f(n) Corollary There is a Godel number n such that φ n is the constant function with output n Hence, n is the Godel number of a self-reproducing program. i.e., a Turing machine whose program, denoted by godel number n, does nothing on any input x except print its own code, i.e., the string = ungodel(n) This is the idea behind a quine the name quine was first used by Hofstadter in his book Godel, Escher, Bach in honor of the logician W.V.O. Quine Omega = (λx.xx)(λx.xx) is an example of a self-reproducing program in the lambda calculus compare this to the following in Scheme and C: ((lambda (x) `(,x ',x)) '(lambda (x) `(,x ',x))) main(a){printf(a= main(a){printf(a=%c%s%c,34,a,34);} ,34,a,34);} godel main(a){printf(a=\ main(a){printf(a=%c%s%c,34,a,34);}\ ,34,a,34);} = Recursive Definition in the λ-calculus How do we define recursive expressions? will this work? mult λm n. (iszero m - 0 add n (mult (pred m) n)) No! There is a problem with this definition we cannot define mult in terms of itself without some way to handle the self-referential naming -- recursive self-reference introduces a challenge most programming languages do this automagically, but in the pure λ calculus, we have to come up with a syntactic way to allow recursive definitions recall that in Scheme, letrec is a special syntactic form for writing recursive definitions (ML has val rec ) we have to come up with some way in the lambda calculus to express recursion syntactically without defining a function directly in terms of itself We need a special mathematical device called a fixed point operator that works for any function defined in the lambda calculus 11 Defining Recursive Functions Fixed Point Theorem for λ calculus For all F, there exists an X such that F(X) = X Proof: let W = λx.f(xx) and let X = WW then X = WW = λx.f(xx)w = F(WW) = F(X) X = WW is called a fixed point of F Fact: we can generate a fixed point for any function F Let F = λy.y W = λx.f(xx) = λx.(λy.y)(xx) Proof that X = WW is a fixed point for λy.y X = WW = (λx.(λy.y)(xx))(λx.(λy.y)(xx)) = (λy.y)((λx.(λy.y)(xx))(λx.(λy.y)(xx))) = F(X) note that (λy.y)((λx.(λy.y)(xx))(λx.(λy.y)(xx)) = (λx.xx)(λx.xx) so (λx.xx)(λx.xx) is a fixed point for λy.y, i.e., λx.x Homework: Generate a fixed point for F = λxy.xy 12 6 Fixed Point Operators Consider a fixed point operator Fix Fix F = F (Fix F) Fix applied to any function F gives F and repeats F by applying Fix to F one more time there are many such fixed point operators The fixed point operator commonly defined in the λ- calculus is called the (lazy) Y combinator Y = (λf. (λx.f(xx)) (λx.f(xx))) Y E = (λf. (λx.f(xx)) (λx.f(xx))) E = (λx.e(xx)) (λx.e(xx)) = E ((λx.e(xx)) (λx.e(xx))) = E (Y E) since Y E = E (Y E) = E (E (Y E)) = E (E (E (Y E))..) i.e., Y is a fixed point operator that when applied to any expression E applies E to a copy of itself repeatedly (i.e., recursively) the recursion only terminates if E has a terminating condition Homework: evaluate Y λx.x 13 Using the Y combinator Any expression of the form f x 1 x n = E is called recursive if f occurs free in E if you want: f x 1 x n = ~~~~ f ~~~~ then define F = Y (λf x 1 x n. ~~~~ f ~~~~) for example: mult = λm n. (iszero m - 0 add n (mult (pred m) n)) Becomes multfn = λf m n. (iszero m - 0 add n (f pred m) n)) mult = Y multfn mult x y = (Y multfn) x y = multfn (Y multfn) x y = multfn mult x y = (λf m n. (iszero m - 0 add n (f pred m) n))) mult x y = (iszero x - 0 add y (mult (pred x) y)) = (iszero x - 0 add y ((Y multfn) (pred x) y)) = 14 7 Fix in Haskell This works because of lazy evaluation. if Haskell had eager evaluation, f (fix f) would never terminate: f (fix f) = f f (fix f) = f f f (fix f) = fix f = f (fix f) fact :: Integer- Integer fact = fix (\f n - if n==0 then 1 else n*f(n-1)) fact 3 = (\f n - if n==0 then 1 else n*f(n-1)) (fix f) 3 = (if 3==0 then 1 else 3*(fix f)(3-1)) = (3*((\f n - if n==0 then 1 else n*f(n-1))(fix f)(3-1)) = = (3*(2*(1*1))) = 6 15 What about Eagerly Evaluated Scheme? We can t use the (lazy) Y combinator in Scheme because it would not terminate under applicative order (eager) evaluation: (define Y (lambda (f) ((lambda (x) (f (x x))) (lambda (x) (f (x x)))))) We need a fixed point combinator that works with applicative order evaluation. (define T (lambda (f) ((lambda (x) (f (lambda (y) ((x x) y)))) (lambda (x) (f (lambda (y) ((x x) y))))))) (define fact (T (lambda (g) (lambda (n) (if (zero? n) 1 (* n (g (- n 1)))))))) 16 8
Related Search
Similar documents
View more...
We Need Your Support
Thank you for visiting our website and your interest in our free products and services. We are nonprofit website to share and download documents. To the running of this website, we need your help to support us.

Thanks to everyone for your continued support.

No, Thanks