Proving Aargh! Turing Complete
When people come up with a new programming language, particularly an esoteric one, there are two important questions:
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 siple 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)
bf_initial contains the prefix,
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.