Design a One Instruction Set Computer!
XOISC

This OISC is based on Fokker's X-combinator which is defined as follows:

$$ X = \lambda f\ . f\ (\lambda g\ h\ x\ . g\ x\ (h\ x))\ (\lambda a\ b\ c\ . a) $$

If we acknowledge the fact that the SKI-calculus is Turing complete the above \$X\$-combinator is Turing complete as well. This is because \$S\$, \$K\$ and \$I\$ can be written in terms of \$X\$, like this:

$$
  \begin{align}
      S &amp;= X\ (X\ X) \\
      K &amp;= X\ X \\
      I = S\ K\ K &amp;= X\ (X\ X)\ (X\ X)\ (X\ X)
  \end{align}
$$

How XOISC works

Internally XOISC has an (initially empty) stack, from there the instruction taking \$n\$ as an argument does the following:


Pop \$n\$ elements (functions \$ f_1 \dots f_N\$) from the stack, push \$f_1\ (f_2\ (\dots (f_N\ X) \dots ))\$


Once there are no more instructions left XOISC will push all command-line arguments (if any) to the stack, for example:

$$
  [ \underbrace{s_1, \dots,\ s_M}_{\text{stack before}}
  ,\ \underbrace{a_1, \dots,\ a_N}_{\text{arguments}}
  ]
$$

The final computation will be \$(\dots ((\dots (s_1\ s_2) \dots)\ s_M)\ a_1) \dots) a_N \$.



Since the one instruction in XOISC takes only one argument (memory offset) there is no reason to even use a name for that instruction. So a valid source file will constitute solely of integers separated by newlines or whitespaces, like for example:

0 0 2 0 1 0 1


Try it online!

Example

Let's take the above example (stack growing to the right):

$$
  \begin{align}
&amp; \texttt{0} &amp; \text{pop 0 and apply (ie. push single } X \text{)}:
  &amp; \quad [X] \\
&amp; \texttt{0} &amp; \text{again simply push } X:
  &amp; \quad [X,\ X] \\
&amp; \texttt{2} &amp; \text{pop 2 (} a,b \text{) and push } a\ (b\ X):
  &amp; \quad [X\ (X\ X)] \\
&amp; \texttt{0} &amp; \text{simply push } X:
  &amp; \quad [X\ (X\ X),\ X] \\
&amp; \texttt{1} &amp; \text{pop 1 (} a \text{) and push } a\ X:
  &amp; \quad [X\ (X\ X),\ X\ X] \\
&amp; \texttt{0} &amp; \text{simply push } X:
  &amp; \quad [X\ (X\ X),\ X\ X,\ X] \\
&amp; \texttt{1} &amp; \text{pop 1 (} a \text{) and push } a\ X:
  &amp; \quad [X\ (X\ X),\ X\ X,\ X\ X]
  \end{align}
$$

Finally evaluate the stack: \$((X\ (X\ X))\ (X\ X))\ (X\ X)\$ or with less parentheses \$X\ (X\ X)\ (X\ X)\ (X\ X)\$ which we recognize as the good old \$S\ K\ K\$ identity function.

Turing completeness

Proof idea

For XOISC to be Turing complete we need to be able to translate any (valid) interleaving of parentheses and \$X\$ combinators. This is possible because when popping, applying and pushing it does so in a right-associative manner (function application is left-associative).

To translate any such \$X\$ expression there is an easy way to do so: Always pop as many elements such that from the beginning of the current level of parentheses there will only be one element left.

As an example, the previously used expression: \$((X\ (X\ X))\ (X\ X))\ (X\ X)\$


to get \$X\$, we simply need a 0
next we're in a new level of parentheses, so we again only need a 0
now two parentheses close, so we need to pop 2 elements: 2
again we're in a new level of parentheses, so we need a 0
two parentheses, close so again a 2
and the same again


So we end up with a different (yet semantically equivalent) XOISC-program:

0 0 2 0 2 0 2  Try it online!

If we stay with this strategy we can easily transform any expression consisting of \$X\$ combinators to an XOISC program which only leaves a single function on the stack.

Formal proof

Given that the SKI-calculus is Turing complete, we need to show two things:


the \$X\$-combinator is a basis for the SKI-calculus
XOISC is able to represent any expression formed with the \$X\$ combinator


The first part - proving the three equalities in the introduction - is very tedious and space consuming, it's also not very interesting. So instead of putting it in this post, you can find here*.



The second part can be proven by structural induction, though it's easier to prove a slightly stronger statement: Namely, for any expression formed by \$X\$-combinators there is a program that will leave that expression as a single expression on the stack:

There are two ways of constructing such an \$X\$ expression, either it's \$X\$ itself or it's \$f\ g\$ for some expressions \$f\$ and \$g\$:

The former one is trivial as 0 will leave \$X\$ on the stack as a single expression. Now we suppose that there are two programs (\$\texttt{F}_1 \dots \texttt{F}_N\$ and \$\texttt{G}_1 … \texttt{G}_K\$) that will leave \$f\$ and \$g\$ as a single expression on the stack and prove that the statement holds for \$f\ g\$ as well:

The program \$\texttt{F}_1 \dots \texttt{F}_N\ \texttt{G}_1 \dots \texttt{G}_{K-1}\ (\texttt{G}_K + 1)\$ will first generate \$f\$ on the stack and then it will generate \$g\$ but instead of only popping parts of \$g\$ it will also pop \$f\$ and apply it, such that it leaves the single expression \$f\ g\$ on the stack. ∎

Interpreter

Inputs

Since the untyped lambda calculus requires us to define our own data types for everything we want and this is cumbersome the interpreter is aware of Church numerals - this means when you supply inputs it will automatically transform numbers to their corresponding Church numeral.

As an example here's a program that multiplies two numbers: Try it online!

You can also supply functions as arguments by using De Bruijn indices, for example the S combinator \\\(3 1 (2 1)) (or λλλ(3 1 (2 1))). However it also recognizes the S, K, I and of course X combinator.

Output

By default the interpreter checks if the output encodes an integer, if it does it will output the corresponding number (in addition to the result). For convenience there's the -b flag which tells the interpreter to try matching a boolean instead (see the last example).

Assembler

Of course any low-level language needs an assembler that converts a high-level language to it, you can simply use any input (see above) and translate it to a XOISC-program by using the -a flag, try it online!**



* In case the link is down, there's a copy as HTML comment in this post. 

** This results in a program that tests for primality, try it online!