Programming Languages andCompilers (CS 421)Elsa L Gunter2112 SC, UIUChttp://www.cs.uiuc.edu/class/sp07/cs421/Based in part on slides by Mattox Beckman, as updatedby Vikram Adve and Gul AghaElsa L. GunterHow to Represent (Free) DataStructures (First Pass)• Suppose τ is a type with n constructors:C1,…,Cn (no arguments)• Represent each term as an abstraction:• Ci →λ x1. … λxn. xi• Think: you give me what to return ineach case (think match statement) andI’ll apply the correct case for the i'thconstructorElsa L. GunterHow to Represent Booleans• bool = True | False• True -> λ x1 x2. x1 ≡α λ x. λ y. x• False -> λ x1 x2. x2 ≡α λ x. λ y. y• Notation– Will write λ x1 … xn. e for λ x1. … λxn. E e1 e2 … en for (…(e1 e2 )… en )Elsa L. GunterHow to Write Functions overData Structures• Write a “match” or “case” function• match c with C1 -> x1 | … | Cn -> xn → λ x1 … xn c. c x1…xn• Think: give me what to do in each caseand give me a case, and I’ll apply thatcaseElsa L. GunterHow to Write Functions overBooleans• If b then c else d• if_then_else b x1 x2 = b x1 x2• if_then_else ≡ λ b x1 x2 . b x1 x2Alternately, if_then_else b x1 x2 = match b with True -> x1 | False -> x2 = (λ x1 x2 b . b x1 x2 ) x1 x2 bif_then_else = λ b x1 x2 (matchbool x1 x2 b)Elsa L. GunterExample:not b = if b then False else True= if_then_else b False True= (λ b c d. b c d) b (λ x y. y)(λ x y. x)= b (λ x y. y)(λ x y. x)• not ≡ λ b. b (λ x y. y)(λ x y. x)• Try and, orElsa L. GunterElsa L. GunterHow to Represent (Free) DataStructures (Second Pass)• Suppose τ is a type with n constructors:C1 t11 … t1k, …,Cn tn1 … tnm,• Represent each term as an abstraction:• Ci ti1 … tij, →λ x1 … xn. xi ti1 … tij,• Ci →λ ti1 … tij, x1 … xn . xi ti1 … tij,• Think: you need to give eachconstructor its arguments fisrtElsa L. GunterHow to Represent Pairs• Pair has one constructor (comma) thattakes two arguments• (a , b) --> λ x . x a b• (_ , _) --> λ a b x . x a bElsa L. GunterFunctions over Pairs• fst ≡ λ p. p (λ x y. x)fst (u , v) -->(λ p. p (λ x y. x))((λ a b x . x a b) u v) -->(λ p. p (λ x y. x))(λ x . x u v) -->(λ x . x u v) (λ x y. x) -->(λ x y. x) u v --> (λ y. u) v --> u• snd ≡ λ p. p (λ x y. y)Elsa L. GunterHow to Represent (Free) DataStructures (Third Pass)• Suppose τ is a type with n constructors:C1 t11 … t1k, …,Cn tn1 … tnm,• Suppose tih ; τ (ie. is recursive)• In place of a value tih have a function tocompute the recursive value tih x1 … xn• Ci →λ ti1 … tij, x1 … xn . xi ti1 … (tih x1 … xn) … tij,Elsa L. GunterHow to Represent NaturalNumbers• nat = Suc nat | 0• 0 ≡ λ f x. x• Suc n = λ f x. f (n f x)• Suc ≡ λ n f x. f (n f x)• Such re presentation calledChurch NumeralsElsa L. GunterSome Church Numerals• Suc 0 = (λ n f x. f (n f x)) (λ f x. x) --> λ f x. f ((λ f x. x) f x) --> λ f x. f ((λ x. x) x) --> λ f x. f xApply a function to its argument onceElsa L. GunterSome Church Numerals• Suc(Suc 0) = (λ n f x. f (n f x)) (Suc 0) -->(λ n f x. f (n f x)) (λ f x. f x) --> λ f x. f ((λ f x. f x) f x)) --> λ f x. f ((λ x. f x) x)) --> λ f x. f (f x)Apply a function twiceIn general n = λ f x. f ( … (f x)…) with napplications of fElsa L. GunterAdding Church Numerals• n ≡ λ f x. f n x and m ≡ λ f x. f m x• n + m = λ f x. f (n+m) x = λ f x. f n (f m x )= λ f x. n f (m f x)• + ≡ λ n m f x. n f (m f x)• Subtraction is harderElsa L. GunterMultiplying Church Numerals• n ≡ λ f x. f n x and m ≡ λ f x. f m x• n ∗ m = λ f x. (f n ∗ m) x = λ f x. (f m)n x =λ f x. n (m f) x• ∗ ≡ λ n m f x. n (m f) xElsa L. GunterPrimitive Recursion over Nat• fold f z n=• match n with 0 -> z• | Suc m -> f (fold f z m)• fold ≡ λ f z n. n f z• is_zero n = fold (λ r. False) True n• = (λ f x. f n x) (λ r. False) True• = ((λ r. False) n ) True• = if n = 0 then True else FalseElsa L. GunterPredecessor• let pred_aux n =• match n with 0 -> (0,0)• | Suc m• -> (Suc(fst(pred_aux m)), fst(pred_aux m)• = fold (λ r. (Suc(fst r), fst r)) (0,0) n• pred ≡ λ n. snd (pred_aux n) n = λ n. snd (fold (λ r.(Suc(fst r), fst r)) (0,0) n)Elsa L. GunterRecursion• Want a λ-term Y such that for all term Rwe have• Y R = R (Y R)• Y needs to have replication to“remember” a copy of R• Y = λ y. (λ x. y(x x)) (λ x. y(x x))• Y R = (λ x. R(x x)) (λ x. R(x x))• = R ((λ x. R(x x)) (λ x. R(x x)))• Notice: Requires lazy evaluationElsa L. GunterFactorial• Let F = λ f n. if n = 0 then 1 else n * f(n-1)• Y F 3 = F (Y F) 3• = if 3 = 0 then 1 else 3 * ((Y F)(3 -1))• = 3 * (Y F) 2 = 3 * (F(Y F) 2)• = 3 * (if 2 = 0 then 1 else 2 * (Y F)(2-1))• = 3 * (2 * (Y F)(1)) = 3 * (2 * (F(Y F) 1)) =…• = 3 * 2 * 1 * (if 0 = 0 then 1 else 0*(Y F)(0 -1))• = 3 * 2 * 1 * 1 = 6Elsa L. GunterY in OCaml# let rec y f = f (y f);;val y : ('a -> 'a) -> 'a = <fun># let mk_fact = fun f n -> if n = 0 then 1 else n * f(n-1);;val mk_fact : (int -> int) -> int -> int =<fun># y mk_fact;;Stack overflow during evaluation (loopingrecursion?).Elsa L. GunterEager Eval Y in Ocaml# let rec y f x = f (y f) x;;val y : (('a -> …
View Full Document
Unlocking...