Lecture 21 Functional Programming (III) Call-By-Value (leftmost, innermost, but not under lambdas) e.g., -------- (\a.\b.a)(|(\x.x)y|)((\x.z)y) --------- ------- --------------------------- ----------- -> |(\a.\b.a)y| ((\x.z)y) ----------- ------- --------- -> (\b.y) (|(\x.z)y|) --------- ---------------- -> (\b.y)z -> y Note: redexes are underlied, the chosen redexs are boxed. Applicative order: - leftmost: MN choose redexes in M before redexes in N - innermost: (\x.M)N choose any redexes in N before choosing the overall redex => CBV: - First, evaluate the expression in the function position as far as possible - Next, evaluate the experssion in the argument position as far as possible - Finally, substitute the argument into the body and continue evaluation Note: 1. It is easy to see the correspondence b/w the rules of application order and the rules fo CBV. 2. But they are not identical. e.g., Applicative order -------- (\x.|(\y.z)x|) ((\a.a)b) -------- ------- ------------------------ -------- -> (\x.z)(|(\a.a)b|) --------- ----------------- ->(\x.z)b -> z CBV -------- (\x.(\y.z)x) (|(\a.a)b|) -------- -------- ------------------------ |--------------| -> |(\x.(\y.z)x)b | | ------- | --------------- -> (\y.z)b -> z Call-By-Name (leftmost, outermost, but not under lambdas) e.g., -------------------------- | (\x.(\y.z)x) ((\a.a)b) | | -------- ------- | -------------------------- -> ---------------- |(\y.z)((\a.a)b)| | ------- | ----------------- -> z - First, evaluate the expression in the function position until it reaches the form \x.M - Next, substitute the unevaluated argument into the body and contine evaluation An interpreter that support CBN The env no longer maps names to values, but rather names to unevaluated expressions. Just as with function closures, however, these unevaluated expressions need to be packaged with their environment (together called thunks). datatype Value = NumV of int | Fnv of Id*Exp*Env and Thunk = Thunk of Exp*Env with type Env = Thunk Dict fun eval (Var x) env = force (lookup x env) | eval (App (e1, e2)) env = let val (x, body, senv) = getFn( eval e1 env) val thunk - delay (e2, env) val senv' = insert x thunk senv in eval body senv' end and delay (arg, arg_env) = Thunk (arg, arg_env) and force (Thunk (arg, arg_env)) = eval arg arg_env Call-By-Need (Lazy evaluation) - pass the argument in unevaluated form - if any copy of the argument is ever evaluated, then all copies of the argument get updated with the same value (Therefore, CVN never evaluates an argument more than once). datatype Value = NumV of int | Fnv of Id*Exp*Env and Thunk = Value of Value | Thunk of Exp*Env with type Env = Thunk ref Dict fun eval (Var x) env = force (lookup x env) | eval (App (e1, e2)) env = let val (x, body, senv) = getFn( eval e1 env) val thunk - delay (e2, env) val senv' = insert x thunk senv in eval body senv' end and delay (arg, arg_env) = ref Thunk (arg, arg_env) and force thunkref = ( case !thunkref of Value v => v | Thunk (arg, arg_env) => let val v = eval arg arg_env thunkref := Value v in v end ) Lambda calculus is Turing complete To prove, we simply need to simulate the constructs which are necessary for Turing complete computing but not yet exist in lambda calculus. - Booleans key constructs: if, ff, and tt if tt M N = M if ff M N = N therefore, if = \p.\x.\y. p x y ("if" can be encoded as a function that takes three arguments, the first is a boolean, and the other two are expressions that will be choosen depending on boolean) tt M N = M ff M N = N therefore, tt = \x.\y.x and ff = \x.\y.y ( "tt" is a function that takes two arguments and returns the first; "ff" is a function that takes two arguments and returns the second.) e.g., if ff 3 4 = (\p.\a.\b. p a b) (\x.\y.y) 3 4 --------------------------- = (\a.\b. (\x.\y.y) a b) 3 4 -------------------------- = (\x.\y.y) 3 4 = 4 - Numbers (Church numerals) 0 = \s.\z.z 1 = \s.\z.sz 2 = \s.\z.s(sz) ... n = \s.\z. s(s(s...(sz)...))) n is an operator to apply a function n times. isZero = \n.n (\x.ff) tt e.g., isZero 0 = (\n.n(\x.ff)tt) (\s.\z.z) = (\s.\z.z) (\x.ff) tt = tt isZero 1 = (\n.n(\x.ff)tt) (\s.\z.sz) = (\s.\z.sz) (\x.ff) tt = (\x.ff) tt = ff succ = \n.(\s.\z. s(n s z)) e.g., succ 3 = (\n.(\s.\z. s(n s z))) (\s.\z. s(s(sz))) ---------------------------------------- = \s.\z. s ( (\s.\z. s(s(sz))) s z ) ------------------ = \s.\z. s ( ( \z. s(s(sz))) z ) ----------------- = \s.\z. s ( ( s(s(sz))) ) = \s.\z. s ( s ( s (sz))) = 4 - Addition add m n = m succ n add m n = \s.\z. m s (n s z) Therefore, lambda abstraction gives that add = \m.\n.(\s.\z. m s (n s z)) - Multiplication mult m n = n (add m) zero = m (add n) zero = \s.\z. m (n s) z - recursions fact = \n. if n=0 then 1 else n * fact(n-1) Fact f = \n.if n=0 then 1 else n * f (n-1) f0 = Bottom f1 = Fact f0 f2 = Fact f1 ... fi = Fact f_{i-1} = Fact(Fact(Fact ....f0)))) f_infty = Fact f_infty That is, f_infty is a fixed-point of Fact, which itself is not recursive at all Suppose a fucntion Y, such that YF = F(F(F(F...)))) = F(YF) With such a magical Y, we can define the factorial function as: fact = f_infty = Y(Fact) = Y (\f.\n. if n=0 then 1 else n * f (n-1) ) It is easy to verify that the following definition (attributed to Haskell B. Curry) Y = \h.(\x.h(xx))(\x.h(xx)) satisfies the requirement. YF = (\h.(\x.h(xx))(\x.h(xx))) F --------------------------- = (\x.F(xx))(\x.F(xx)) -------------------- = F((\x.F(xx))(\x.F(xx))) ^^^^^^^^^^^^^^^^^^^^ = F(YF) The Y function is known as the Y combinator.