SKI

SKI Combinator Calculus

Haskell implementation on Moses Schonfinkel's SKI-combintator calculus. It's a Turing Complete model of computation consisting purely of applying terms S, K and I.

This calculus can be used as a basis for all combinatory logic.

Prerequisites

You need Haskell, this compiles with GHC 8.2.2 at least (Stack resolver: lts-11.0).

To Build & Run

You can use cabal to build and run this, see this README, alternatively you can use vanilla ghc to build:

To compile and run do: ghc -O2 -o ski Main then run ./ski

Alternatively to use the GHCi Interpreter do: ghci Main then type main

In either case you get something like the following:

Welcome to the SKI combinator calculus REPL
Type some terms or press Enter to leave.
>

Note: When run in GHCi, you don't have the luxury of escaped characters, backspace, delete etc... Compile it using GHC if you need this.

Examples

Where you can then have some fun, try these examples:

• S K K x
• S (K S) K (known as B)
• S (S (K (S (K S) K)) S) (K K) (known as C)

You can copy and paste from the output:

Welcome to the SKI combinator calculus REPL
Type some terms or press Enter to leave.
>   S K K x
~>* x
>   x
=   x

> denotes the REPL waiting for input, = means no reductions occurred (it's the same term), ~> denotes one reduction, and ~>* denotes 0 or more reductions (although in practice this is 1 or more due to =).

There is also a reduction tracer, which should print each reduction step. prefix any string with ' in order to see the reductions:

>   'S (S (K S) (S (K K) I)) (S (S (K S) (S (K K) I)) (K I)) (S (S (K S) (S (K K) I)) (S (S (K S) (S (K K) I)) (K I)))
~>  S (K S) (S (K K) I) (S (S (K S) (S (K K) I)) (S (S (K S) (S (K K) I)) (K I))) (S (S (K S) (S (K K) I)) (K I) (S (S (K S) (S (K K) I)) (S (S (K S) (S (K K) I)) (K I))))
~>  K S (S (S (K S) (S (K K) I)) (S (S (K S) (S (K K) I)) (K I))) (S (K K) I (S (S (K S) (S (K K) I)) (S (S (K S) (S (K K) I)) (K I)))) (S (S (K S) (S (K K) I)) (K I) (S (S (K S) (S (K K) I)) (S (S (K S) (S (K K) I)) (K I))))
~>  S (S (K K) I (S (S (K S) (S (K K) I)) (S (S (K S) (S (K K) I)) (K I)))) (S (S (K S) (S (K K) I)) (K I) (S (S (K S) (S (K K) I)) (S (S (K S) (S (K K) I)) (K I))))
~>  S (K K (S (S (K S) (S (K K) I)) (S (S (K S) (S (K K) I)) (K I))) (I (S (S (K S) (S (K K) I)) (S (S (K S) (S (K K) I)) (K I))))) (S (S (K S) (S (K K) I)) (K I) (S (S (K S) (S (K K) I)) (S (S (K S) (S (K K) I)) (K I))))
~>  S (K (I (S (S (K S) (S (K K) I)) (S (S (K S) (S (K K) I)) (K I))))) (S (S (K S) (S (K K) I)) (K I) (S (S (K S) (S (K K) I)) (S (S (K S) (S (K K) I)) (K I))))
~>  S (K (S (S (K S) (S (K K) I)) (S (S (K S) (S (K K) I)) (K I)))) (S (S (K S) (S (K K) I)) (K I) (S (S (K S) (S (K K) I)) (S (S (K S) (S (K K) I)) (K I))))
~>  S (K (S (S (K S) (S (K K) I)) (S (S (K S) (S (K K) I)) (K I)))) (S (K S) (S (K K) I) (S (S (K S) (S (K K) I)) (S (S (K S) (S (K K) I)) (K I))) (K I (S (S (K S) (S (K K) I)) (S (S (K S) (S (K K) I)) (K I)))))
~>  S (K (S (S (K S) (S (K K) I)) (S (S (K S) (S (K K) I)) (K I)))) (K S (S (S (K S) (S (K K) I)) (S (S (K S) (S (K K) I)) (K I))) (S (K K) I (S (S (K S) (S (K K) I)) (S (S (K S) (S (K K) I)) (K I)))) (K I (S (S (K S) (S (K K) I)) (S (S (K S) (S (K K) I)) (K I)))))
~>  S (K (S (S (K S) (S (K K) I)) (S (S (K S) (S (K K) I)) (K I)))) (S (S (K K) I (S (S (K S) (S (K K) I)) (S (S (K S) (S (K K) I)) (K I)))) (K I (S (S (K S) (S (K K) I)) (S (S (K S) (S (K K) I)) (K I)))))
~>  S (K (S (S (K S) (S (K K) I)) (S (S (K S) (S (K K) I)) (K I)))) (S (K K (S (S (K S) (S (K K) I)) (S (S (K S) (S (K K) I)) (K I))) (I (S (S (K S) (S (K K) I)) (S (S (K S) (S (K K) I)) (K I))))) (K I (S (S (K S) (S (K K) I)) (S (S (K S) (S (K K) I)) (K I)))))
~>  S (K (S (S (K S) (S (K K) I)) (S (S (K S) (S (K K) I)) (K I)))) (S (K (I (S (S (K S) (S (K K) I)) (S (S (K S) (S (K K) I)) (K I))))) (K I (S (S (K S) (S (K K) I)) (S (S (K S) (S (K K) I)) (K I)))))
~>  S (K (S (S (K S) (S (K K) I)) (S (S (K S) (S (K K) I)) (K I)))) (S (K (S (S (K S) (S (K K) I)) (S (S (K S) (S (K K) I)) (K I)))) (K I (S (S (K S) (S (K K) I)) (S (S (K S) (S (K K) I)) (K I)))))
~>  S (K (S (S (K S) (S (K K) I)) (S (S (K S) (S (K K) I)) (K I)))) (S (K (S (S (K S) (S (K K) I)) (S (S (K S) (S (K K) I)) (K I)))) I)

Note: the above computes 2^2 in Church Numeral format.

Note: if you provide a non-normalizing term (e.g. with (S I I (S I I)) which is the same as (\x.x x)(\x.x x) in ULC), reductions will not terminate. Use STLC for termination guarantees.

You can save variables for the life of the program with a let expression. Any time a saved variable appears in a term, it will be substituted for the saved term:

>   let two = S (S (K S) (S (K K) I)) (S (S (K S) (S (K K) I)) (K I))
Saved: S (S (K S) (S (K K) I)) (S (S (K S) (S (K K) I)) (K I))
>   two two
~>* S (K (S (S (K S) (S (K K) I)) (S (S (K S) (S (K K) I)) (K I)))) (S (K (S (S (K S) (S (K K) I)) (S (S (K S) (S (K K) I)) (K I)))) I)

Note: Consequently let and = are keywords, and so you cannot name variables with these.

Syntax

We base the language on the BNF for the SKI calculus:

However we adopt the standard bracketing conventions to eliminate ambiguity in the parser. Concretely, the parser implements the non-ambiguous grammar as follows:

Some notes about the syntax:

• Symbols of SKI are the characters S, K, or I. This is isomorphic to a whiteboard treatment using characters. Some treatments of the SKI calculus omit variables, but as long as there is no notion of binding it should be ok.
• Nested terms may not require brackets and follows the convention of application being left associative where S K K 1 is the same as ((S K) K) 1, but not S (K (K 1)).
• Whitespace does not matter, except in between application where a minimumum of one space is needed.
• Non-terminating terms require you to quit with Ctrl+C or whatever your machine uses to interupt computations.
• This grammar left-recursive and non-ambiguous.

Semantics

The SKI calculus operates on combinations of S, K, and I, which can be formed with introduction and elimination rules:

combined with application:

and reduced with rules:

• This implementation follows a small-step operational semantics and has free variables for simplicity.
• Reductions include the one-step reduction (see reduce1 in SKI.hs), the many-step reduction (see reduce in SKI.hs).

Other Implementation Details

• SKI.hs contains the Haskell implementation of the calculus, including substitution, reduction, and other useful things.
• Parser.hs contains the monadic parser combinators needed to parse input strings into term ASTs for the calculus. It follows the grammar above.
• Repl.hs contains a simple read-eval-print loop which hooks into main, and into the parser.
• Main.hs is needed for GHC to compile without any flags, it also invokes the repl.
• Note this file does not have unit tests as there are no special symbols that need testing in the grammar and the untyped nature of the calculus means generative testing with QuickCheck would be more complicated that the language itself.

For contributions, see the project to-do list or submit a PR with something you think it needs.