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