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!
Sandboxed post and OISC Wikipedia page. – MD XF – 2018-02-02T00:48:49.310
not sure /// is an oisc still, due to its print instruction. – Destructible Lemon – 2018-02-02T04:39:09.213
@DestructibleLemon It doesn't have a
print
instruction. It only has one instruction, which prints as a side effect. – MD XF – 2018-02-02T04:39:31.14310What is an "instruction"? And how do we count them? – Post Rock Garf Hunter – 2018-02-02T05:15:30.760
I wish I knew enough to do this, it looks fun. – NoOneIsHere – 2018-02-02T06:15:13.703
1@NoOneIsHere i wish i knew enough just to vote xD – Brian H. – 2018-02-02T08:40:31.140
2I downvoted this. I think this is a very interesting idea, but you don't explain exactly what an OISC is and how to confirm something is one. I made BF an OISC, but that is clearly against the spirit of the question, but technically valid. – NoOneIsHere – 2018-02-02T18:33:36.557
1@MDXF i don't think you get ///: it has a substitution command, and it has print commands, which is not just a side effect of the substitution command – Destructible Lemon – 2018-02-03T03:38:37.953
@DestructibleLemon no it doesn't have a print command, it just prints everything left after substitution at the end of the program. – MD XF – 2018-02-03T17:52:59.550
@MDXF http://esolangs.org/wiki////#Description
– Destructible Lemon – 2018-02-04T01:46:06.5201@NoOneIsHere Because [tag:popularity-contest]. Yes, it's valid, but it has poor score (vote tally), so it won't win. – user202729 – 2018-02-05T14:46:23.883
1@user202729 Yeah, but just the fact that it is impossible to make sure a language truly has only 1 instruction makes me feel that the challenge is under-speficied. – NoOneIsHere – 2018-02-05T17:30:38.880
Can one mandate that several specific values, [0, 1, and -1], are stored in memory locations? – user230118 – 2018-02-05T18:16:48.023
@user230118 yes, that's fine. – MD XF – 2018-02-05T18:26:45.620
Since I've voted to close this as unclear, I thought it would be a good idea to make explicit why. As per my previous comment there is no explanation as to how one can count the size of the instruction set. Without this definition I don't know how we can determine if an answer is a valid one. – Post Rock Garf Hunter – 2018-02-12T03:26:30.183
@WheatWizard Can you think of an objective definition then? – MD XF – 2018-02-12T03:32:24.513
@MDXF I don't even really understand what you want out of a definition, mostly because I'm unclear as to what you think is an OISC. If had an idea for a definition I would have already suggested it, but I don't know what qualities you want out of a definition. – Post Rock Garf Hunter – 2018-02-12T03:36:13.517
Is
MOV
-like languages not real OISC? – l4m2 – 2018-04-13T07:50:41.403