On this page we look at the redux function for SKI Combinators. This follows on from the introduction to SKI Combinators on this page.
Tutorial
If you are working with a version of FriCAS before 1.1.3 then the Ski domain needs to be installed on your system as described on this page.
On this page we will be working with 'untyped' SKI combinators so we create an instance called UNTYP to simplify notation:
(1) -> UNTYP := SKICombinators Untyped
(1) SKICombinators(Untyped)
Type: Type |
SKI Combinator Redux
We will check that the program agrees with the following known results:
- SIKx ⊳ Ix(Kx) ⊳ x(Kx)
- SSKxy ⊳ xy(Kxy) ⊳ xyx
- S(SK)xy ⊳ SKy(xy) ⊳ K(xy)(y(xy)) ⊳ xy
- S(KS)Sxyz ⊳ KSx(Sx)yz ⊳ Sxz(yz) ⊳ x(yz)(z(yz))
- S(S(KS)K)(S(KS)K)Ixy ⊳ S(KS)KI(S(KS)KI)xy ⊳ KSI(KI)(KSI(KI))xy ⊳ KIx(S(KI)x)y KIy(xy) ⊳ xy
When we do this with the program we get:
SIKx ⊳ Ix(Kx) ⊳ x(Kx)
(2) -> s1 := parseSki("SIKx")$UNTYP
(2) SIK x
Type: SKICombinators(Untyped)
(3) -> redux(s1)$UNTYP
I x(K x)
x(K x)
(3) x(K x)
Type: SKICombinators(Untyped)
|
SSKxy ⊳ xy(Kxy) ⊳ xyx
(4) -> s2 := parseSki("SSKx y")$UNTYP
(4) SSK x y
Type: SKICombinators(Untyped)
(5) -> redux(s2)$UNTYP
x y(K x y)
x y x
(5) x y x
Type: SKICombinators(Untyped)
|
S(SK)xy ⊳ SKy(xy) ⊳ K(xy)(y(xy)) ⊳ xy
(6) -> s3 := parseSki("S(SK)x y")$UNTYP
(6) S(SK) x y
Type: SKICombinators(Untyped)
(7) -> redux(s3)$UNTYP
SK y(x y)
K(x y)(y(x y))
x y
(7) x y
Type: SKICombinators(Untyped)
|
S(KS)Sxyz ⊳ KSx(Sx)yz ⊳ Sxz(yz) ⊳ x(yz)(z(yz))
(8) -> s4 := parseSki("S(KS)Sx y z")$UNTYP
(8) S(KS)S x y z
Type: SKICombinators(Untyped)
(9) -> redux(s4)$UNTYP
KS x(S x) y z
S x z(y z)
x(y z)(z(y z))
(9) x(y z)(z(y z))
Type: SKICombinators(Untyped)
|
S(S(KS)K)(S(KS)K)Ixy ⊳ S(KS)KI(S(KS)KI)xy ⊳ KSI(KI)(KSI(KI))xy ⊳ KIx(S(KI)x)y KIy(xy) ⊳ xy
(10) -> s5 := parseSki("S(S(KS)K)(S(KS)K)Ix y")$UNTYP
(10) S(S(KS)K)(S(KS)K)I x y
Type: SKICombinators(Untyped)
(11) -> redux(s5)$UNTYP
S(KS)KI(S(KS)KI) x y
KSI(KI)(KSI(KI)) x y
KI x(S(KI) x) y
KI y(x y)
x y
(11) x y
Type: SKICombinators(Untyped) |
Next
Modeling Computation