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)


metadata block
see also:
Correspondence about this page

Book Shop - Further reading.

Where I can, I have put links to Amazon for books that are relevant to the subject, click on the appropriate country flag to get more details of the book or to buy it from them.

flag flag flag flag flag flag Axiom Volume 1: Tutorial. Documentation is freely availible from:


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

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