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