## 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:

• To shorten the presentation we don't present in detail how the substitute operation is performed - we provide the result in one step.
• We treat `hd`, `tl`, and `null` as unary operators.
• We evaluate lists of constants (e.g. `[3, 1, 2]`) as constants.
• Each step of the evaluation is labelled. Labels express both the depth of nesting, and the rules that apply in the respective step. Consider label `[X2001] [E7.1, apply: E2]`, for example. This label identifies an evaluation step at depth 4. `X` represents the top level, i.e. the entire expression that we are trying to evaluate. Digits ```2, 0, 0, 1``` indicate that the current evaluation step has been reached by applying steps (or subrules) `2, 0, 0, 1`, respectively. Note that the labelling does not convey any information about the actual rules that have been applied, except for the last one. The expression `[E7.1, apply: E2]` declares that the current step has been reached by applying substep `1` of rule `E7` (let expression), while the next rule that will be applied to the current expression is `E2`.
```
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.