SKI Combinators Redux

On this page we look at the redux function for SKI Combinators. This follows on from the introduction to SKI Combinators on this page.


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:

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)


Modeling Computation


metadata block
see also:
Correspondence about this page

This site may have errors. Don't use for critical systems.

Copyright (c) 1998-2023 Martin John Baker - All rights reserved - privacy policy.