Substitution Model Example: foldl

This handout illustrates the application of the substitution model for the purpose of evaluating a recursive function embedded within a let statement. The recursive function we examine is foldl, which has been implemented using the SML subset given in class.

Note that:


let
 fun foldl (f: 'a -> 'b -> 'b): 'b -> 'a list -> 'b =
  fn (b: 'b) =>
   fn (lst: 'a list) =>
    if null(lst) then b
    else ((foldl f) ((f (hd lst)) b)) (tl lst)
in
 ((foldl (fn x => fn y => x + y)) 0) [1, 3]
end


[X] [-, apply: E7] ? eval(let fun foldl f = fn b => fn lst => if null(lst) then b else ((foldl f) ((f (hd lst)) b)) (tl lst) in ((foldl (fn x => fn y => x + y)) 0) [1, 3] end)
[X0] [E7.0, apply: D2] ? eval_decl(fun foldl f = fn b => fn lst => if null(lst) then b else ((foldl f) ((f (hd lst)) b)) (tl lst)) = [(foldl, fun foldl f = fn b => fn lst => if null(lst) then b else ((foldl f) ((f (hd lst)) b)) (tl lst))] [X1] [E7.1; apply: *] substitute([(foldl, fun foldl f = fn b => fn lst => if null(lst) then b else ((foldl f) ((f (hd lst)) b)) (tl lst))], (((foldl (fn x => fn y => x + y)) 0) [1, 3])) = ((((fun foldl f = fn b => fn lst => if null(lst) then b else ((foldl f) ((f (hd lst)) b)) (tl lst)) (fn x => fn y => x + y)) 0) [1, 3]) [X2] [E7.2, apply: E3] ? eval((((fun foldl f = fn b => fn lst => if null(lst) then b else ((foldl f) ((f (hd lst)) b)) (tl lst)) (fn x => fn y => x + y)) 0) [1, 3])
[X20] [E3.0, apply: E3] ? eval(((fun foldl f = fn b => fn lst => if null(lst) then b else ((foldl f) ((f (hd lst)) b)) (tl lst)) (fn x => fn y => x + y)) 0)
[X200] [E3.0, apply: E3] ? eval((fun foldl f = fn b => fn lst => if null(lst) then b else ((foldl f) ((f (hd lst)) b)) (tl lst)) (fn x => fn y => x + y))
[X2000] [E3.0, apply: E8] eval(fun foldl f = fn b => fn lst => if null(lst) then b else ((foldl f) ((f (hd lst)) b)) (tl lst)) = fn f => fn b => fn lst => if null(lst) then b else (((fun foldl f = fn b => fn lst => if null(lst) then b else ((foldl f) ((f (hd lst)) b)) (tl lst)) f) ((f (hd lst)) b)) (tl lst) [X2001] [E3.1, apply: E2] eval(fn x => fn y => x + y) = fn x => fn y => x + y [X2002] [E3.2, apply: *] substitute([(f, fn x => fn y => x + y)], fn b => fn lst => if null(lst) then b else (((fun foldl f = fn b => fn lst => if null(lst) then b else ((foldl f) ((f (hd lst)) b)) (tl lst)) f) ((f (hd lst)) b)) (tl lst)) = fn b => fn lst => if null(lst) then b else (((fun foldl f = fn b => fn lst => if null(lst) then b else ((foldl f) ((f (hd lst)) b)) (tl lst)) (fn x => fn y => x + y)) (((fn x => fn y => x + y) (hd lst)) b)) (tl lst) [X2003] [E3.3, apply: E2] eval(fn b => fn lst => if null(lst) then b else (((fun foldl f = fn b => fn lst => if null(lst) then b else ((foldl f) ((f (hd lst)) b)) (tl lst)) (fn x => fn y => x + y)) (((fn x => fn y => x + y) (hd lst)) b)) (tl lst)) = fn b => fn lst => if null(lst) then b else (((fun foldl f = fn b => fn lst => if null(lst) then b else ((foldl f) ((f (hd lst)) b)) (tl lst)) (fn x => fn y => x + y)) (((fn x => fn y => x + y) (hd lst)) b)) (tl lst)
[X200] [E3.0, apply: E3] eval((fun foldl f = fn b => fn lst => if null(lst) then b else ((foldl f) ((f (hd lst)) b)) (tl lst)) (fn x => fn y => x + y)) = fn b => fn lst => if null(lst) then b else (((fun foldl f = fn b => fn lst => if null(lst) then b else ((foldl f) ((f (hd lst)) b)) (tl lst)) (fn x => fn y => x + y)) (((fn x => fn y => x + y) (hd lst)) b)) (tl lst) [X201] [E3.1, apply: E1] eval(0) = 0 [X202] [E3.2, apply: *] substitute([(b, 0)], fn lst => if null(lst) then b else (((fun foldl f = fn b => fn lst => if null(lst) then b else ((foldl f) ((f (hd lst)) b)) (tl lst)) (fn x => fn y => x + y)) (((fn x => fn y => x + y) (hd lst)) b)) (tl lst)) = fn lst => if null(lst) then 0 else (((fun foldl f = fn b => fn lst => if null(lst) then b else ((foldl f) ((f (hd lst)) b)) (tl lst)) (fn x => fn y => x + y)) (((fn x => fn y => x + y) (hd lst)) 0)) (tl lst) [X203] [E3.3, apply: E2] eval(fn lst => if null(lst) then 0 else (((fun foldl f = fn b => fn lst => if null(lst) then b else ((foldl f) ((f (hd lst)) b)) (tl lst)) (fn x => fn y => x + y)) (((fn x => fn y => x + y) (hd lst)) 0)) (tl lst)) = fn lst => if null(lst) then 0 else (((fun foldl f = fn b => fn lst => if null(lst) then b else ((foldl f) ((f (hd lst)) b)) (tl lst)) (fn x => fn y => x + y)) (((fn x => fn y => x + y) (hd lst)) 0)) (tl lst)
[X20] [E3.0, apply: E3] eval(((fun foldl f = fn b => fn lst => if null(lst) then b else ((foldl f) ((f (hd lst)) b)) (tl lst)) (fn x => fn y => x + y)) 0) = fn lst => if null(lst) then 0 else (((fun foldl f = fn b => fn lst => if null(lst) then b else ((foldl f) ((f (hd lst)) b)) (tl lst)) (fn x => fn y => x + y)) (((fn x => fn y => x + y) (hd lst)) 0)) (tl lst) [X21] [E3.1, apply: E1(!)] eval([1, 3]) = [1, 3] [X22] [E3.2, apply: *] substitute([(lst, [1, 3])], if null(lst) then 0 else (((fun foldl f = fn b => fn lst => if null(lst) then b else ((foldl f) ((f (hd lst)) b)) (tl lst)) (fn x => fn y => x + y)) (((fn x => fn y => x + y) (hd lst)) 0)) (tl lst)) = if null([1, 3]) then 0 else (((fun foldl f = fn b => fn lst => if null(lst) then b else ((foldl f) ((f (hd lst)) b)) (tl lst)) (fn x => fn y => x + y)) (((fn x => fn y => x + y) (hd [1, 3])) 0)) (tl [1, 3]) [X23] [E3.3, apply: E6] ? eval(if null([1, 3]) then 0 else (((fun foldl f = fn b => fn lst => if null(lst) then b else ((foldl f) ((f (hd lst)) b)) (tl lst)) (fn x => fn y => x + y)) (((fn x => fn y => x + y) (hd [1, 3])) 0)) (tl [1, 3]))
[X230] [E6.0, apply: *] eval(null([1, 3])) = false [X231] [E6.2, apply: E3] ? eval((((fun foldl f = fn b => fn lst => if null(lst) then b else ((foldl f) ((f (hd lst)) b)) (tl lst)) (fn x => fn y => x + y)) (((fn x => fn y => x + y) (hd [1, 3])) 0)) (tl [1, 3]))
[X2310] [E3.0, apply: E3] ? eval(((fun foldl f = fn b => fn lst => if null(lst) then b else ((foldl f) ((f (hd lst)) b)) (tl lst)) (fn x => fn y => x + y)) (((fn x => fn y => x + y) (hd [1, 3])) 0))
[X23100] [E3.0, apply: E3] ? eval((fun foldl f = fn b => fn lst => if null(lst) then b else ((foldl f) ((f (hd lst)) b)) (tl lst)) (fn x => fn y => x + y))
[X231000] [E3.0, apply: E8] eval(fun foldl f = fn b => fn lst => if null(lst) then b else ((foldl f) ((f (hd lst)) b)) (tl lst)) = fn f => fn b => fn lst => if null(lst) then b else (((fun foldl f = fn b => fn lst => if null(lst) then b else ((foldl f) ((f (hd lst)) b)) (tl lst)) f) ((f (hd lst)) b)) (tl lst) [X231001] [E3.1, apply: E2] eval(fn x => fn y => x + y) = fn x => fn y => x + y [X231002] [E3.2, apply: *] substitute([(f, fn x => fn y => x + y)], fn b => fn lst => if null(lst) then b else (((fun foldl f = fn b => fn lst => if null(lst) then b else ((foldl f) ((f (hd lst)) b)) (tl lst)) f) ((f (hd lst)) b)) (tl lst)) = fn b => fn lst => if null(lst) then b else (((fun foldl f = fn b => fn lst => if null(lst) then b else ((foldl f) ((f (hd lst)) b)) (tl lst)) (fn x => fn y => x + y)) (((fn x => fn y => x + y) (hd lst)) b)) (tl lst) [X231003] [E3.3, apply: E2] eval(fn b => fn lst => if null(lst) then b else (((fun foldl f = fn b => fn lst => if null(lst) then b else ((foldl f) ((f (hd lst)) b)) (tl lst)) (fn x => fn y => x + y)) (((fn x => fn y => x + y) (hd lst)) b)) (tl lst)) = fn b => fn lst => if null(lst) then b else (((fun foldl f = fn b => fn lst => if null(lst) then b else ((foldl f) ((f (hd lst)) b)) (tl lst)) (fn x => fn y => x + y)) (((fn x => fn y => x + y) (hd lst)) b)) (tl lst)
[X23100] [E3.0, apply: E3] eval((fun foldl f = fn b => fn lst => if null(lst) then b else ((foldl f) ((f (hd lst)) b)) (tl lst)) (fn x => fn y => x + y)) = fn b => fn lst => if null(lst) then b else (((fun foldl f = fn b => fn lst => if null(lst) then b else ((foldl f) ((f (hd lst)) b)) (tl lst)) (fn x => fn y => x + y)) (((fn x => fn y => x + y) (hd lst)) b)) (tl lst) [X23101] [E3.1, apply: E3] ? eval((((fn x => fn y => x + y) (hd [1, 3])) 0))
[X231010] [E3.0, apply: E3] ? eval((fn x => fn y => x + y) (hd [1, 3]))
[X2310100] [E3.0, apply: E2] eval(fn x => fn y => x + y) = fn x => fn y => x + y [X2310101] [E3.1, apply: E4] ? eval(hd [1, 3])
[X23101010] [E4.0, apply: E1] eval([1, 2]) = [1, 2] [X23101011] [E4.1, apply: -] apply_unop(hd, [1, 3]) = 1
[X2310101] [E3.1, apply: E4] eval(hd [1, 3]) = 1 [X2310102] [E3.2, apply: *] substitute([(x, 1)], fn y => x + y) = fn y => 1 + y
[X231010] [E3.0, apply: E3] eval((fn x => fn y => x + y) (hd [1, 3])) = fn y => 1 + y [X231011] [E3.1, apply: E1] eval(0) = 0 [X231012] [E3.2, apply: *] substitute([(y, 0)], 1 + y) = 1 + 0 [X231013] [E3.3, apply: E5] ? eval(1 + 0)
[X2310130] [E5.0, apply: E1] eval(1) = 1 [X2310131] [E5.1, apply: E1] eval(0) = 0 [X2310132] [E5.2, apply: -] apply_binop(+, 1, 0) = 1
[X231013] [E3.3, apply: E5] eval(1 + 0) = 1
[X23101] [E3.1, apply: E3] eval((((fn x => fn y => x + y) (hd [1, 3])) 0)) = 1 [X23102] [E3.2, apply: *] substitute([(b, 1)], fn lst => if null(lst) then 1 else (((fun foldl f = fn b => fn lst => if null(lst) then b else ((foldl f) ((f (hd lst)) b)) (tl lst)) (fn x => fn y => x + y)) (((fn x => fn y => x + y) (hd lst)) 1)) (tl lst)) [X23103] [E3.3, apply: E2] eval(fn lst => if null(lst) then 1 else (((fun foldl f = fn b => fn lst => if null(lst) then b else ((foldl f) ((f (hd lst)) b)) (tl lst)) (fn x => fn y => x + y)) (((fn x => fn y => x + y) (hd lst)) 1)) (tl lst)) = fn lst => if null(lst) then 1 else (((fun foldl f = fn b => fn lst => if null(lst) then b else ((foldl f) ((f (hd lst)) b)) (tl lst)) (fn x => fn y => x + y)) (((fn x => fn y => x + y) (hd lst)) 1)) (tl lst)
[X2310] [E3.0, apply: E3] eval(((fun foldl f = fn b => fn lst => if null(lst) then b else ((foldl f) ((f (hd lst)) b)) (tl lst)) (fn x => fn y => x + y)) (((fn x => fn y => x + y) (hd [1, 3])) 0)) = fn lst => if null(lst) then 1 else (((fun foldl f = fn b => fn lst => if null(lst) then b else ((foldl f) ((f (hd lst)) b)) (tl lst)) (fn x => fn y => x + y)) (((fn x => fn y => x + y) (hd lst)) 1)) (tl lst) [X2311] [E3.1, apply: E4] ? eval(tl [1, 3])
[X23110] [E4.0, apply: E1] eval([1, 3]) = [1, 3] [X23111] [E4.1, apply: -] apply_unop(tl, [1, 3]) = [3]
[X2311] [E3.1, apply: E4] eval(tl [1, 3]) = [3] [X2312] [E3.2, apply: *] substitute([(lst, [3])], if null(lst) then 1 else (((fun foldl f = fn b => fn lst => if null(lst) then b else ((foldl f) ((f (hd lst)) b)) (tl lst)) (fn x => fn y => x + y)) (((fn x => fn y => x + y) (hd lst)) 1)) (tl lst)) = if null([3]) then 1 else (((fun foldl f = fn b => fn lst => if null(lst) then b else ((foldl f) ((f (hd lst)) b)) (tl lst)) (fn x => fn y => x + y)) (((fn x => fn y => x + y) (hd [3])) 1)) (tl [3]) [X2313] [E3.3, apply: E6] ? eval(if null([3]) then 1 else (((fun foldl f = fn b => fn lst => if null(lst) then b else ((foldl f) ((f (hd lst)) b)) (tl lst)) (fn x => fn y => x + y)) (((fn x => fn y => x + y) (hd [3])) 1)) (tl [3]))
[X23130] [E6.0, apply: E4] ? eval(null([3]))
[X231300] [E4.0, apply: E1] eval([3]) = [3] [X231301] [E4.1, apply: -] apply_unop(null, [3]) = false
[X23130] [E6.0, apply: E4] eval(null([3])) = false [X23131] [E6.2, apply: E3] ? eval((((fun foldl f = fn b => fn lst => if null(lst) then b else ((foldl f) ((f (hd lst)) b)) (tl lst)) (fn x => fn y => x + y)) (((fn x => fn y => x + y) (hd [3])) 1)) (tl [3]))
[X231310] [E3.0, apply: E3] ? eval(((fun foldl f = fn b => fn lst => if null(lst) then b else ((foldl f) ((f (hd lst)) b)) (tl lst)) (fn x => fn y => x + y)) (((fn x => fn y => x + y) (hd [3])) 1))
[X2313100] [E3.0, apply: E3] ? eval((fun foldl f = fn b => fn lst => if null(lst) then b else ((foldl f) ((f (hd lst)) b)) (tl lst)) (fn x => fn y => x + y))
[X23131000] [E3.0, apply: E8] eval(fun foldl f = fn b => fn lst => if null(lst) then b else ((foldl f) ((f (hd lst)) b)) (tl lst)) = fn f => fn b => fn lst => if null(lst) then b else (((fun foldl f = fn b => fn lst => if null(lst) then b else ((foldl f) ((f (hd lst)) b)) (tl lst)) f) ((f (hd lst)) b)) (tl lst) [X23131001] [E3.1, apply: E2] eval(fn x => fn y => x + y) = fn x => fn y => x + y [X23131002] [E3.2, apply: *] substitute([(f, fn x => fn y => x + y)], fn b => fn lst => if null(lst) then b else (((fun foldl f = fn b => fn lst => if null(lst) then b else ((foldl f) ((f (hd lst)) b)) (tl lst)) f) ((f (hd lst)) b)) (tl lst)) = fn b => fn lst => if null(lst) then b else (((fun foldl f = fn b => fn lst => if null(lst) then b else ((foldl f) ((f (hd lst)) b)) (tl lst)) (fn x => fn y => x + y)) (((fn x => fn y => x + y) (hd lst)) b)) (tl lst) [X23131003] [E3.3, apply: E2] eval(fn b => fn lst => if null(lst) then b else (((fun foldl f = fn b => fn lst => if null(lst) then b else ((foldl f) ((f (hd lst)) b)) (tl lst)) (fn x => fn y => x + y)) (((fn x => fn y => x + y) (hd lst)) b)) (tl lst)) = fn b => fn lst => if null(lst) then b else (((fun foldl f = fn b => fn lst => if null(lst) then b else ((foldl f) ((f (hd lst)) b)) (tl lst)) (fn x => fn y => x + y)) (((fn x => fn y => x + y) (hd lst)) b)) (tl lst)
[X2313100] [E3.0, apply: E3] eval((fun foldl f = fn b => fn lst => if null(lst) then b else ((foldl f) ((f (hd lst)) b)) (tl lst)) (fn x => fn y => x + y)) = fn b => fn lst => if null(lst) then b else (((fun foldl f = fn b => fn lst => if null(lst) then b else ((foldl f) ((f (hd lst)) b)) (tl lst)) (fn x => fn y => x + y)) (((fn x => fn y => x + y) (hd lst)) b)) (tl lst) [X2313101] [E3.1, apply: E3] ? eval((((fn x => fn y => x + y) (hd [3])) 1))
[X23131010] [E3.0, apply: E3] ? eval((fn x => fn y => x + y) (hd [3]))
[X231310100] [E3.0, apply: E2] eval(fn x => fn y => x + y) = fn x => fn y => x + y [X231310101] [E3.1, apply: E4] ? eval(hd [3])
[X2313101010] [E4.0, apply: E1] eval([3]) = [3] [X2313101011] [E4.1, apply: -] apply_unop(hd, [3]) = 3
[X231310101] [E3.1, apply: E4] eval(hd [3]) = 3 [X231310102] [E3.2, apply: *] substitute([(x, 3)], fn y => x + y) = fn y => 3 + y
[X23131010] [E3.0, apply: E3] eval((fn x => fn y => x + y) (hd [3])) = fn y => 3 + y [X23131011] [E3.1, apply: E1] eval(1) = 1 [X23131012] [E3.2, apply: *] substitute([(y, 1)], 3 + y) = 3 + 1 [X23131013] [E3.3, apply: E5] ? eval(3 + 1)
[X231310130] [E5.0, apply: E1] eval(3) = 3 [X231310131] [E5.1, apply: E1] eval(1) = 1 [X231310132] [E5.2, apply: -] apply_binop(+, 3, 1) = 4
[X23131013] [E3.3, apply: E5] eval(3 + 1) = 4
[X2313101] [E3.1, apply: E3] eval((((fn x => fn y => x + y) (hd [3])) 1)) = 4 [X2313102] [E3.2, apply: *] substitute([(b, 4)], fn lst => if null(lst) then 4 else (((fun foldl f = fn b => fn lst => if null(lst) then b else ((foldl f) ((f (hd lst)) b)) (tl lst)) (fn x => fn y => x + y)) (((fn x => fn y => x + y) (hd lst)) 4)) (tl lst)) [X2313103] [E3.3, apply: E2] eval(fn lst => if null(lst) then 4 else (((fun foldl f = fn b => fn lst => if null(lst) then b else ((foldl f) ((f (hd lst)) b)) (tl lst)) (fn x => fn y => x + y)) (((fn x => fn y => x + y) (hd lst)) 4)) (tl lst)) = fn lst => if null(lst) then 4 else (((fun foldl f = fn b => fn lst => if null(lst) then b else ((foldl f) ((f (hd lst)) b)) (tl lst)) (fn x => fn y => x + y)) (((fn x => fn y => x + y) (hd lst)) 4)) (tl lst)
[X231310] [E3.0, apply: E3] eval(((fun foldl f = fn b => fn lst => if null(lst) then b else ((foldl f) ((f (hd lst)) b)) (tl lst)) (fn x => fn y => x + y)) (((fn x => fn y => x + y) (hd [3])) 1)) = fn lst => if null(lst) then 4 else (((fun foldl f = fn b => fn lst => if null(lst) then b else ((foldl f) ((f (hd lst)) b)) (tl lst)) (fn x => fn y => x + y)) (((fn x => fn y => x + y) (hd lst)) 4)) (tl lst) [X231311] [E3.1, apply: E4] ? eval(tl [3])
[X2313110] [E4.0, apply: E1] eval([3]) = [3] [X2313111] [E4.1, apply: -] apply_unop(tl, [3]) = []
[X231311] [E3.1, apply: E4] eval(tl [3]) = [] [X231312] [E3.2, apply: *] substitute([(lst, [])], if null(lst) then 4 else (((fun foldl f = fn b => fn lst => if null(lst) then b else ((foldl f) ((f (hd lst)) b)) (tl lst)) (fn x => fn y => x + y)) (((fn x => fn y => x + y) (hd lst)) 4)) (tl lst)) = if null([]) then 4 else (((fun foldl f = fn b => fn lst => if null(lst) then b else ((foldl f) ((f (hd lst)) b)) (tl lst)) (fn x => fn y => x + y)) (((fn x => fn y => x + y) (hd [])) 4)) (tl []) [X231313] [E3.3, apply: E6] ? eval(if null([]) then 4 else (((fun foldl f = fn b => fn lst => if null(lst) then b else ((foldl f) ((f (hd lst)) b)) (tl lst)) (fn x => fn y => x + y)) (((fn x => fn y => x + y) (hd [])) 4)) (tl []))
[X2313130] [E6.0, apply: E4] ? eval(null([]))
[X23131300] [E4.0, apply: E1] eval([]) = [] [X23131301] [E4.1, apply: -] apply_unop(null, []) = true
[X2313130] [E6.0, apply: E4] eval(null([])) = true [X2313131] [E6.1, apply: E1] eval(4) = 4
[X231313] [E6.0, apply: E6] eval(if null([]) then 4 else (((fun foldl f = fn b => fn lst => if null(lst) then b else ((foldl f) ((f (hd lst)) b)) (tl lst)) (fn x => fn y => x + y)) (((fn x => fn y => x + y) (hd [])) 4)) (tl [])) = 4
[X23131] [E6.2, apply: E3] eval((((fun foldl f = fn b => fn lst => if null(lst) then b else ((foldl f) ((f (hd lst)) b)) (tl lst)) (fn x => fn y => x + y)) (((fn x => fn y => x + y) (hd [3])) 1)) (tl [3])) = 4
[X2313] [E3.3, apply: E6] eval(if null([3]) then 1 else (((fun foldl f = fn b => fn lst => if null(lst) then b else ((foldl f) ((f (hd lst)) b)) (tl lst)) (fn x => fn y => x + y)) (((fn x => fn y => x + y) (hd [3])) 1)) (tl [3])) = 4
[X231] [E6.2, apply: E3] eval((((fun foldl f = fn b => fn lst => if null(lst) then b else ((foldl f) ((f (hd lst)) b)) (tl lst)) (fn x => fn y => x + y)) (((fn x => fn y => x + y) (hd [1, 3])) 0)) (tl [1, 3])) = 4
[X23] [E3.3, apply: E6] eval(if null([1, 3]) then 0 else (((fun foldl f = fn b => fn lst => if null(lst) then b else ((foldl f) ((f (hd lst)) b)) (tl lst)) (fn x => fn y => x + y)) (((fn x => fn y => x + y) (hd [1, 3])) 0)) (tl [1, 3])) = 4
[X2] [E7.2, apply: E3] eval((((fun foldl f = fn b => fn lst => if null(lst) then b else ((foldl f) ((f (hd lst)) b)) (tl lst)) (fn x => fn y => x + y)) 0) [1, 3]) = 4
[X] [apply: E7] ? eval(let fun foldl f = fn b => fn lst => if null(lst) then b else ((foldl f) ((f (hd lst)) b)) (tl lst) in ((foldl (fn x => fn y => x + y)) 0) [1, 3] end) = 4

Prepared by Tibor Jánosi, Fall 2002.

CS312 home  2002 Cornell University Computer Science