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