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:

(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:
http://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:

Operator What it does SKI equivalent
(normal form)
I Identity (leave unchanged) I or SKK or SKS
B Function composition S(KS)K
B' Reverse function composition  
C Swap functions S(K(SI))K
K Form constant function K
S Generalized composition S
W Doubling or diagonalizing  

So we can see in the 3 examples below :

(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:

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.


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: http://www.axiom-developer.org/axiom-website/documentation.html

 

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

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