Substitution Model Examples: SKK

 val  ident =  let
   val  S = fn x => fn y => fn z => (x z) (y z)
   val  K = fn x => fn y> x
in
  ((S K) K) 312
end

[x] [-, apply: D1] ? eval_decl( val ident = let val S = fn x => fn y => fn z => (x z) (y z) val K = fn x => fn y> x in ((S K) K) 312 end)
[x0] [D1.0, apply: E7] ? eval( let val S = fn x => fn y => fn z => (x z) (y z) val K = fn x => fn y> x in ((S K) K) 312 end)
[x00] [E7.0, apply:D1] ? eval_decl( val S = fn x => fn y => fn z => (x z) (y z) ) = [S,fn x => fn y => fn z => (x z) (y z)] [x00][E7.0, apply: D1] ? eval_decl( val K = fn x => fn y => x ) = [K,fn x => fn y> x] [x01] [E7.1, apply: S(x, e, e1(e2)] ? subst([(S,fn x => fn y => fn z => (x z) (y z)) ,(K,fn x => fn y => x)], ((S K) K) 312)
[x000] [S(x, e, e1(e2), apply: S(x, e, e1(e2)] ? ((subst( [(S,fn x => fn y => fn z => (x z) (y z)) ,(K,fn x => fn y => x)], (S K))) (subst( [(S,fn x => fn y => fn z => (x z) (y z)) ,(K,fn x => fn y => x)], K)) (subst([(S,fn x => fn y => fn z => (x z) (y z)) ,(K,fn x => fn y => x)], 312) [x0001] [S(x, e, e1(e2), apply: substitution(x,e,y)] ? ((subst( [(S,fn x => fn y => fn z => (x z) (y z)) ,(K,fn x => fn y => x)], S)) (subst( [(S,fn x => fn y => fn z => (x z) (y z)) ,(K,fn x => fn y => x), K)))) (subst( [(S,fn x => fn y => fn z => (x z) (y z)) ,(K,fn x => fn y => x)], K) (subst( [(S,fn x => fn y => fn z => (x z) (y z)) ,(K,fn x => fn y => x)], 312)
[x01] subst([(S,fn x => fn y => fn z => (x z) (y z)) ,(K,fn x => fn y => x)],((S K) K) 312) = ((((fn x => fn y => fn z => (x z) (y z)) (fn x => fn y => x))(fn x => fn y => x)) 312 [x02] [E7.2, apply: E3] ? eval(((((fn x => fn y => fn z => (x z) (y z)) (fn x => fn y => x))(fn x => fn y => x)) 312)
[x020] [E3.0, apply: E3] ? eval((((fn x => fn y => fn z => (x z) (y z)) (fn x => fn y => x))(fn x => fn y => x))
[x0200] [E3.0 apply: E3] ? eval(((fn x => fn y => fn z => (x z) (y z)) (fn x => fn y => x))
[x02000] [E3.0, apply: E2] ? eval(fn x => fn y => fn z => (x z) (y z)) = fn x => fn y => fn z => ((x z) (y z)) [x02001] [E3.1, apply: E2] ? eval(fn x => fn y => x) = (fn x => fn y => x) [x02002] [E3.2, apply: substitution(x,e,y)] ? subst([x, (fn x => fn y => x)], fn y => fn z => (x z) (y z)) = fn y => fn z => ((fn x => fn y => x) z) (y z)) [x02003] [E3.3, apply: E2] ? eval(fn y => fn z => ((fn x => fn y => x) z) (y z))) = fn y => fn z => ((fn x => fn y => x) z) (y z)
[x0200] eval(((fn x => fn y => fn z => (x z) (y z)) (fn x => fn y => x)) = fn y => fn z => ((fn x => fn y => x) z) (y z) [x0201] [E3.1, apply: E2] ? eval( (fn x => fn y => x) = (fn x => fn y => x) [x0202] [E3.2, apply: S(x,e,y)] ? subst([y, (fn x => fn y => x)], fn z => ((fn x => fn y => x) z) (y z)) = fn z => (((fn x => fn y => x) z) ((fn x => fn y => x) z)) [x0203] [E3.3, apply: E2] ? eval( fn z => (((fn x => fn y => x) z) ((fn x => fn y => x) z))) = fn z => (((fn x => fn y => x) z) ((fn x => fn y => x) z))
[x020] eval((((fn x => fn y => fn z => (x z) (y z)) (fn x => fn y => x)) (fn x => fn y => x)) = fn z => (((fn x => fn y => x) z) ((fn x => fn y => x) z)) [x021][E3.1, apply: E1] ? eval(312) = 312 [x022][E3.2, apply: S(x,e,y)] ? subst([z,312],(((fn x => fn y => x) z) ((fn x => fn y => x)z))) = ((fn x => fn y => x) 312)((fn x => fn y => x) 312) [x023][E3.3, apply: E3] ? eval(((fn x => fn y => x) 312)((fn x => fn y => x) 312) )
[x0230][E3.0, apply: E3] ? eval(((fn x => fn y => x) 312)
[x02300][E3.0, apply: E2] ? eval(fn x => fn y => x) = fn x => fn y => x [x02301] [E3.1, apply: E1] ? eval(312) = 312 [x02302][E3.2, apply: S(x,e,y)] ? subst([x,312], fn y => x) = fn y => 312 [x02303][E3.3, apply: E2] ? eval(fn y => 312) = fn y=> 312
[x0230] eval(((fn x => fn y => x) 312) = fn y => 312 [x0231][E3.1, apply: E3] ? eval(((fn x => fn y => x) 312)
[x02310][E3.0, apply: E2] ? eval(fn x => fn y => x) = fn x => fn y => x [x02311] [E3.1, apply: E1] ? eval(312) = 312 [x02312][E3.2, apply: S(x,e,y)] ? subst([x,312], fn y => x) = fn y => 312 [x02313][E3.3, apply: E2] ? eval(fn y => 312) = fn y=> 312
[x0231] eval(((fn x => fn y => x) 312) = fn y => 312 [x0232][E3.2, apply: S(x,e,y)] ? subst([y,fn y=> 312],312) = 312 [x10233][E3.3, apply: E1] ? eval(312) = 312
[x023] eval(((fn x => fn y => x) 312)((fn x => fn y => x) 312) ) = 312
[x02] eval(((((fn x => fn y => fn z => (x z) (y z)) (fn x => fn y => x))(fn x => fn y => x)) 312) = 312
[x0] eval( let val S = fn x => fn y => fn z => (x z) (y z) val K = fn x => fn y> x in ((S K) K) 312 end) = 312 [x1] [D1.1, apply:match] ? match(312,ident) = [ident,312]
[x] eval_decl( val ident = let val S = fn x => fn y => fn z => (x z) (y z) val K = fn x => fn y> x in ((S K) K) 312 end) = [ident, 312]

Prepared by Jacqueline Bodine, Fall 2002.

CS312 home  2002 Cornell University Computer Science