SKI Combinators

Ski combinators were introduced by Moses Schönfinkel and Haskell Curry with the aim of eliminating the need for variables in mathematical logic. It is equivalent to lambda calculus but it can be used for doing, without variables, anything that would require variables in other systems.

The structure is a self-modifing binary tree.

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, for later versions its already installed. The source code is in a file called computation.spad, which is available here:

https://github.com/martinbaker/multivector/

Download and compile in the usual way. Make sure it is exposed since Axiom/FriCAS was started.

(1) -> )library VTYP
 
   VarTyp is now explicitly exposed in frame frame1 
   VarTyp will be automatically loaded when needed from 
      /home/martin/VTYP.NRLIB/VTYP
(1) -> )library VARCAT
 
   VarCat is now explicitly exposed in frame frame1 
   VarCat will be automatically loaded when needed from 
      /home/martin/VARCAT.NRLIB/VARCAT
(1) -> )library UNTYPED
 
   Untyped is now explicitly exposed in frame frame1 
   Untyped will be automatically loaded when needed from 
      /home/martin/UNTYPED.NRLIB/UNTYPED
(1) -> )library SKICOMB
 
   Ski is now explicitly exposed in frame frame1 
   Ski will be automatically loaded when needed from 
      /home/martin/SKI.NRLIB/SKI

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

Constructing SKI combinators

SKI combinators consist of a binary tree structure where the leaves of the tree are either I, K or S combinators or variables.

The I, K and S combinators can be constructed by using the I(), K() and S() functions.

Variables (representing functions) can be constructed by var("x")$Untyped, where x is the name of the variable, we can then pass this variable to a ski constructor to create a SKI term:

(2) -> m1 := I()$UNTYP

   (2)  I
                                            Type: SKICombinators(Untyped)

(3) -> m2 := K()$UNTYP

   (3)  K
                                            Type: SKICombinators(Untyped)

(4) -> m3 := S()$UNTYP 

   (4)  S
                                            Type: SKICombinators(Untyped)

(5) -> v1 := ski(var("x")$Untyped)$UNTYP

   (5)  x
                                            Type: SKICombinators(Untyped)

Compound combinator terms can be constructed by ski(node1,node2) where node1 and node2 are other combinator terms. Internally combinators are stored as a binary tree. The notation assumes association to the left, in the absence of brackets, the term to the left binds more tightly than the one on the right. So, in the following, we can see that:

• In n2 the second term is an atom so brackets are not required.
• In n3 the second term is compound so brackets are required.

(6) -> n1 := ski(m1,m2)$UNTYP

   (6)  IK
                                            Type: SKICombinators(Untyped)

(7) -> n2 := ski(n1,m3)$UNTYP

   (7)  IKS
                                            Type: SKICombinators(Untyped)
(8) -> n3 := ski(m3,n1)$UNTYP

   (8)  S(IK)
                                            Type: SKICombinators(Untyped)

In addition, to avoid having to build up this node by node, there is a quicker way to construct SKI combinators. We can construct the whole binary tree from a single string using the parseSki constructor as follows. Again the notation assumes association to the left, in the absence of brackets, the term to the left binds more tightly than the one on the right.

When we are using parseSki and we have two variables next to each other (such as 'x y') then we must put a space between the variables, this is so that we can gave a variable a name consisting of multiple characters. So 'xy' is a single variable but 'x y' is a two variables. All variables must start with a lower case letter. The combinators I,K and S do not need to be separated with a space since they always consist of 1 character.

(9) -> n4 := parseSki("IKS")$UNTYP

   (9)  IKS
                                            Type: SKICombinators(Untyped)
(10) -> n5 := parseSki("S(IK)")$UNTYP

   (10)  S(IK)
                                            Type: SKICombinators(Untyped)

redux

Now that we have constructed our SKI combinator we can apply the combinators using the redux function. This allows us to apply the self-modifing binary tree.

The first combinator to investigate is 'I'. This is a do nothing combinator:

(11) -> s1 := parseSki("Ix")$UNTYP

   (11)  I x
                                            Type: SKICombinators(Untyped)
(12) -> redux(s1)$UNTYP
 
x

   (12)  x
                                            Type: SKICombinators(Untyped)

The next combinator to investigate is 'K'. This removes the final variable:

(13) -> s2 := parseSki("Kx y")$UNTYP
 
   (13)  K x y
                                            Type: SKICombinators(Untyped)
(14) -> redux(s2)$UNTYP
 
x

   (14)  x
                                            Type: SKICombinators(Untyped)

The next combinator to investigate is 'S' This applies the first two functions to the third:

(15) -> s3 := parseSki("Sx y z")$UNTYP

   (15)  S x y z
                                            Type: SKICombinators(Untyped)
(16) -> redux(s3)$UNTYP
 
x z(y z)

   (16)  x z(y z)
                                            Type: SKICombinators(Untyped)

To check out the redux function with more complex combinators see this page:
https://www.euclideanspace.com/maths/standards/program/mycode/computation/ski/redux/

Secondary Combinators

Any calculation can be done by some combination of K and S. However some sequences occur frequently so it is worth assigning them special letters:

So we can see in the 3 examples below :

• In 17 that "SKKx y" is equivalent to "x y", that is SKK is identity, equivalent to I
• In 19 that "S(K(SI))Kx y" is equivalent to "y x", so "S(K(SI))K" reverses its operands.

(17) -> redux(parseSki("SKKx y")$UNTYP)$UNTYP
 
K x(K x)y
x y

   (17)  x y
                                            Type: SKICombinators(Untyped)
(18) -> redux(parseSki("S(KS)x y")$UNTYP)$UNTYP

KS y(x y)
S(x y)

   (18)  S(x y)
                                            Type: SKICombinators(Untyped)
(19) -> redux(parseSki("S(K(SI))Kx y")$UNTYP)$UNTYP

K(SI) x(K x)y
I y(K x y)
y x

   (19)  y x
                                            Type: SKICombinators(Untyped)

SKI combinators can be coerced to and from λ-calculus and intuitionistic logic. For a tutorial about how to coerce to/from these algebras see this page.

To Do

These are issues to think about for longer term development of this domain.

Issue 1

Currently this only works with variables, this means that:

• redux applied to 'SKKx y' gives 'x y'
• but redux applied to 'SKK' does not give 'I'

That is, I am looking for a way to 'lift' from working in terms operators acting on variables to working in terms of operators only.

Issue 2

It would be good to be able to use these combinators to operate on Axiom/FriCAS functions.

See also

For more information about using the 'redux' operation with SKI Combinators see this page.

I also have Axiom/FriCAS coding for λ-caculus, as explained on this page, where there is explanation and tutorial.

Modeling Computation

EuclideanSpace

home

This page discusses implementing combinators using Axiom/FriCAS which is a Computer Algebra System. These are part of a series of pages (starting here) where we discuss implementing computer related structures in Axiom/FriCAS.

Computer Algebra Systems

On this page I have put some information about computer algebra systems and in particular Axiom/FriCAS.

Related Topics

Implemeting mathematical structures using Axiom/FriCAS:

• Computer related structures.
• Logic related structures.
• Graph related structures.

Other Code

This is one of a series of pages describing code that I have written for FriCAS. Some of this code has already been included with the FriCAS library and so can be used as soon as FriCAS is installed (as described here). Other code on these pages is not yet included with FriCAS and so would have to be compiled from within FriCAS. For an overview of all the code I have written, on various topics, see page here.

IDE for FriCAS

Axiom/Fricas Information on this Site

Writing Logic Code Using a CAS Program

SPAD Language