From Register Machines to Brainfuck, part 2

This is a continuation of my previous post on register machines vs. Brainfuck programs. We left off at Brainfuck's supposed Turing-completeness.

Now, the most straightforward way to prove Turing-completeness of a given language is to write a compiler that takes a program written in a language that is already known to be Turing-complete, and creates a program written in the language to be proved Turing-complete, that simulates the original program. So an obvious way to prove that Brainfuck is a Turing-complete language is to compile register machine programs into Brainfuck. This has the added advantage that a programmer having some experience in real-world assembly programming can easily write register machine programs, which can then be compiled into (horribly inefficient and over-complicated, as we'll see) Brainfuck programs.

Important note: Of course, to really prove, in a mathematical sense, that Brainfuck is Turing-complete, we would first have to define formal operational semantics for register machines and Brainfuck programs to be even able to argue about simulating one with the another. In this post, I will appeal to intuition instead.

From Register Machines to Brainfuck, part 1

The Brainfuck programming language stays a somewhat current topic at the office ever since Maya's 9-digit program, so much so, that now we've even started designing our own Brainfuck computer using first principle logic gates only. But more on that later. Today and in my next post, I'm going to write about compiling register machines to Brainfuck.

Register machines

The register machine is an abstract mathematical machine much like Turing machines or finite automata, and it can be shown to be Turing-complete. On the other hand, it models very closely how real-world computers operate. The program of a register machine (RM for short) is a labelled list of instructions, each operating on one of a finite number of memory cells called registers, holding values of natural numbers. The allowed instructions in the specific formulation that we'll be using here is:

• Increment (inc) r, Decrement (dec) r
• Clear (clr) r: Sets the value of register r to 0
• Copy (mov) r_dest r_src: Overwrite the contents of register r_dest with the contents of register r_src
• Jump to (jmp) label: Continue execution from the instruction marked with label
• Jump if (jz) r is zero to label: If the contents of register r is non-zero, continue execution as normal. If it is zero,
• Output (out) r, Input (in) r: Not strictly necessary for the theory to work out, it's convenient to include serial input/output in the model

Note that this set of operations is redundant in that both clr and mov can be easily implemented in terms of the others — they are included here only for clarity later on.

For example, to add the contents of register a to b, we can write the following program using a temporary register z:

The Haskell code for parsing register machine programs and an instantiator for a simple little macro language is available on GitHub.

Brainfuck

Brainfuck is a joke programming language, one designed to be as much of a pain to use as possible, while also being powerful enough to solve real problems with it (languages like that are commonly called Turing tar-pits). The link above explains the intentionally minimalistic syntax and the semantics of the language in detail. The sketchy version is that there is a linear array of memory cells and a pointer moving on this array, and the operations can move the pointer and change the contents of the currently pointed cell:

• Increment cell (+), Decrement cell (-)
• Move pointer left (<) or right (>)
• Loop ([]): Repeatedly execute the statements between the [ and the ], as long as the value of the pointed cell is non-zero at the start of each iteration.
• Input (,), Output (.): These modify or print the contents of the currently pointed cell.

You can find my parser, interpreter and x86 compiler for Brainfuck here.

In the next post, we will prove that Brainfuck is Turing-complete by translating register machine programs into Brainfuck. As you can see, there are two differences between RM and Brainfuck: one is that RM uses random access for the registers, whereas Brainfuck can access only one register at a time; the other, more major one is that you can't change the order of execution arbitrarily in Brainfuck. This is why we will have to use some trickery to come up with a translation scheme.

If you're feeling impatient, you can, of course, take a peek in the meantime at my RM → Brainfuck compiler in GitHub.

Efficient type-level division for Haskell

Another approach I wanted to explore to Encsé's 9-digit problem was creating a type-level solution in Haskell. First I'll describe what that would entail, and then present a solution to one of its sub-problems: testing special cases of divisibility in a more efficient way than the naïve implementation of repeating subtractions.

Type-level programming

Basically, a type-level Haskell program is to regular Haskell programs what C++ template metaprograms are to C++ proper. Conrad Parker wrote a great introduction to type-level programming using functional dependencies in issue 6 of The Monad.Reader journal, titled Type-Level Instant Insanity. You encode values as types, and then construct an expression whose type, as inferred by the Haskell compiler, encodes the output of your computation. To actually implement the equivalent of a function, typeclasses are used.

For example, take the following (value-level) Haskell definition of length: (deliberately not using any builtin types, and using unary representation for simplicity):

module ValueLength where
        
data Nat = Z | S Nat      
data List a = Nil | a ::: (List a)
infixr 6 :::

length :: List a -> Nat
length Nil = Z
length (x ::: xs) = S (length xs)
      

(note that due to technical limitations, both : and :: are reserved names in Haskell, and so we have to use ::: for our cons)

To lift this definition to the level of types, we first need a way to represent actual numbers and lists as types. This is pretty straightforward using algebraic datatypes. Since we are ultimately only going to be interested in the type of expressions and not their value, no constructors are defined.

{-# LANGUAGE EmptyDataDecls, TypeOperators,
             FunctionalDependencies,
             MultiParamTypeClasses, UndecidableInstances #-}
module TypeLength where

data Z
data S n

data Nil
data x ::: xs
infixr 6 :::

– Continued below
      

Compiling Haskell into C++ template metaprograms

After Lőri posted his C++ template meta-program solution to the 9-digit problem, Encsé asked me to help him understand it, being the first real-world metaprogram he's encountered. To help both him and myself, I rewrote, function-by-function, his code into Haskell.

This rewriting process was surprisingly straightforward, and the resulting code, while being in a very strict one-to-one correspondence with the original C++ code, was immensely more readable. So this, naturally, lead to the idea of a simple functional programming language that could be compiled into C++ compile-time metaprograms.

A couple of days later, I had a small accident and had to stay in bed for a week, which gave me plenty of time to throw together a proof-of-concept compiler from a Haskell-like language into C++ TMP.

And so MetaFun was born.

MetaFun is structured into three separate modules, one for parsing and typechecking the input language called Kiff (for Keep It Fun & Functional), one for unparsing C++ metaprograms, and the third one is, of course, the compiler itself. I plan to re-use the Kiff module whenever I come up with an idea for another new throwaway functional compiler.

Unary arithmetics is even slower than you'd expect

My coworker Encsé posted a challange use the 9-digit number problem to demonstrate interesting programming techniques. So I sat down and wrote my first practical program using dependant types, in Agda. I've been playing around with Agda previously, but this seemed like a good opportunity to try to write an actual, self-contained, provably correct program with it.

I'm not going to get into details now about the resulting Agda code, because I'm planning to present it in detail in a later post. In its current form, my program is formally proven to produce only good nine-digit numbers; the only property that still needs proving is that it finds all of them.

But the sad surprise came when I tried to actually run it. It was unbearably slow to just get to all possible combinations for the first three digits. I'm talking about 12 minutes just to list them from 123 to 423 (at which point I killed the process). For comparison, the following Haskell program, which is an implementation of the same naïve algorithm, finds the (unique) solution in 4 milliseconds:

import Control.Monad.List

fromDigits = foldr shift 0
    where shift d s = 10 * s + d

p `divides` q = q `mod` p == 0

encse :: [Int]
encse = map fromDigits $ encse' 0 []
    where encse' 9 ds = return ds
          encse' n ds = do d <- [1..9]
                           let ds' = d:ds
                               n' = n + 1
                           guard $ not (d `elem` ds)
                           guard $ n' `divides` fromDigits ds'
                           encse' n' ds'
      

So where's that slowdown coming from?

The first intuition would be that the code generated by Agda is slow because in parallel to the actual computation, it is also evaluating all kinds of proofs. But the proofs exist only in the world of types, so they shouldn't matter once the program is compiled.

The real answer is that calculating in unary representation is slow. Very, very slow. Even slower than you'd imagine.