Proving Aargh! Turing Complete
When people come up with a new programming language, particularly an esoteric one, there are two important questions:
- Can you write a Quine?
- Is it Turing complete?
For Argh!, the first question was quickly answered by someone posting a quine on a mailing list for esoteric languages (distributed with Argh! as examples/quine.agh
). The Turing completeness proof took a bit longer.
Strictly speaking, Argh! has not yet been proven Turing complete, to my knowledge, but Aargh! has. The reason is that the constructive proof requires the unlimited number of lines that only Aargh! allows. This post gives an outline of that proof.
A fun way to prove that Aargh! is Turing complete is to show that some other programming language that is known to be Turing complete can be compiled to Aargh!. That shows that Aargh! is at least as powerful as that other language since for every possible program in that language there’s an Aargh! program that performs the same computation.
A very simple Turing complete language is Brainfuck, and it turns out to be very simple to translate it to Aargh!: Write out a prefix (a bunch of lines of Aargh! code), iterate over the Brainfuck code and for each of the eight commands write a fixed block (a bunch of lines of Aargh! code) and finally write a postfix (a bunch of lines of Aargh! code).
The prefix is just some simple plumbing. The postfix is the most complex of the blocks because it implements the array of bytes that forms the storage of the Brainfuck program. It’s smart enough to grow dynamically as needed.
The prefix, postfix and the blocks for the commands are all constants. This makes for a very simple compiler core which basically just iterates over the bytes in the input file and writes an output file (this is from an early version of bf2aargh):
def bf2argh(infile, outfile, debug_prints=False):
outfile.write(bf_initial)
while 1:
c = infile.read(1)
if not c:
break
command = command_map.get(c)
if command is not None:
if debug_prints:
command = insert_debug_print(command, c)
outfile.write(command)
outfile.write(bf_endofprogram)
outfile.write(bf_dynarray)
Here, bf_initial
contains the prefix, bf_endofprogram
and bf_dynarray
contain the postfix (the latter implements the array of bytes used by Brainfuck) and command_map
is a dictionary mapping the Brainfuck commands to their Aargh! code blocks.
The Brainfuck program consisting of just two “+” commands turns into this Aargh! program (the comments on the right were added for this post):
#! /usr/bin/env aargh
s Prefix
a lDllllj
j ^ j
j lslj ------------------------
j llj F@jS
j JsshDdfdhhhhShaaahh
jg *. D lkVUUUk +-Command
lRadFjllSLSj kFDRRRXj
jhhhhh jh khhhhhhh
j lslj ------------------------
j llj F@jS
j JsshDdfdhhhhShaaahh
jg *. D lkVUUUk +-Command
lRadFjllSLSj kFDRRRXj
jhhhhh jh khhhhhhh
lDslK q ------------------------
^
Jhhhhhhhhshhah
* Tk Postfix
lllDflllsdfFllRXj
. z 03 ya
KhSDhjFdAhARXRh
llllllkd khhh
kD= + lflrxsH
. zD=
lSdFSDlllllllllllllllllllllllllllfllsj
khhDh =j
jssssssssssssssssssssssssssssSsssh
jhffffffkfFjD hhffffffkfFjl K
lssssssssssssssssssssssssssssssssj
hK ljFfkffffffhhs+GRjFfkffffffhj
jssssssssssssssssssssssssssssssssh
jhffffffkfFjD lhhhffffffkfFjXDlhh
lssssssssssssssssssssssssssssssssj
hhl0AjFfkffffffhhhs0FjFfkffffffhj
Jssssssssssssssssssssssssssssssssh
,ffffffkfF,kkkhhhffffffkfFjl0rhh
Kshhhhhh
+lllsrk
z GD 000k
lDlRXDAFlk
jjjjjjjjj,
FFFFFFFFFF
ffffffffff
This concludes the outline of the Turing completeness proof of Aargh!.
Obviously, the generated code is not very efficient, but then, efficiency is not important for Turing completeness. However, there are a lot of interesting Brainfuck programs out there, and making them available for Aargh! can be worthwhile. Therefore it’s interesting to create a more efficient compiler. How this can be done will likely be the topic of some future posts.