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 &= X\ (X\ X) \\
K &= X\ X \\
I = S\ K\ K &= 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}
& \texttt{0} & \text{pop 0 and apply (ie. push single } X \text{)}:
& \quad [X] \\
& \texttt{0} & \text{again simply push } X:
& \quad [X,\ X] \\
& \texttt{2} & \text{pop 2 (} a,b \text{) and push } a\ (b\ X):
& \quad [X\ (X\ X)] \\
& \texttt{0} & \text{simply push } X:
& \quad [X\ (X\ X),\ X] \\
& \texttt{1} & \text{pop 1 (} a \text{) and push } a\ X:
& \quad [X\ (X\ X),\ X\ X] \\
& \texttt{0} & \text{simply push } X:
& \quad [X\ (X\ X),\ X\ X,\ X] \\
& \texttt{1} & \text{pop 1 (} a \text{) and push } a\ X:
& \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!
