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.

CS312 home  © 2002 Cornell University Computer Science