Two Turing Machines

For fun I wrote two universal Turing machines: one in Prolog, one in Mercury. This led me to some observations about type systems and their spheres of utility.

There is a seemingly never-ending argument in software development circles: are static type systems necessary for proper software development, or do they interfere with developers just getting the job done?

 

I had the opportunity to explore both sides of this question recently as I, for fun (not having to work with software gives me time to do fun things), wrote two universal Turing machines: one in Prolog (a dynamic logic language) and Mercury (a static functional logic language).  I had no idea how I'd go about writing such a Turing machine in a logic language, so this was purely exploratory programming for me.

The Prolog experience

Because I had access to a limited implementation in Prolog to guide me, I started with that.  I was exploring a problem domain here, so I found the interactive nature of development in Prolog nice.  The final code wound up looking like this (all the documentation comments, etc. stripped—you can see the full source here):

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
:- module(turing, [turing/4,
                   default_config/5]).
:- meta_predicate turing(5, 5, +, -).

:- use_module(library(lists)).

turing(Config, Rules, TapeIn, TapeOut) :-
    call(Config, IS, _, _, _, _),
    perform(Config, Rules, IS, {[], TapeIn}, {Ls, Rs}),
    reverse(Ls, Ls1),
    append(Ls1, Rs, TapeOut).

perform(Conf, Rules, Q0, TapeIn, TapeOut) :-
    call(Conf, _, FS, RS, B, S),
    ( memberchk(Q0, FS) ->
        % A stopping state has been reached.
        TapeOut = TapeIn

    ; memberchk(Q0, RS) ->
        {Lin, Rin} = TapeIn,
        symbol(Rin, Sym, RsRest, B),
        memberchk(Sym, S),      % Is this a legal symbol?
        once(call(Rules, Q0, Sym, NewSym, Action, Q1)),
        memberchk(NewSym, S),   % Is this a legal symbol?
        action(Action, {Lin, [NewSym|RsRest]}, {Ls1, Rs1}, B),
        perform(Conf, Rules, Q1, {Ls1, Rs1}, TapeOut) ).

symbol([],       B,   [], B).
symbol([Sym|Rs], Sym, Rs, _).

action(left,  {Lin, Rin},  {Lout, Rout}, B) :- left(Lin, Rin, Lout, Rout, B).
action(stay,  Tape,        Tape,         _).
action(right, {L, [S|Rs]}, {[S|L], Rs},  _).

left([],     Rs, [], [B|Rs], B).
left([L|Ls], Rs, Ls, [L|Rs], _).

rule(_, _, _, _, _).

default_config(IState, FStates, RStates, Blank, Symbols) :-
    IState  = q0,
    FStates = [qf],
    RStates = [IState],
    Blank   = b,
    Symbols = [Blank, 0, 1].

 

The code is pretty much written in a top-down style.  turing/4 (the public interface of the module) is defined first.  In line 8 it calls the user-provided configuration predicate to extract the initial state.  (You can see an example of defining a machine configuration in default_config/5 starting at line 40.)  It then calls perform/5 to do the actual work, passing in the user-provided configuration and the user-provided rules for a particular Turing machine.  It also passes down the user-provided list of symbols and places the output (in the usual state of affairs) in TapeOut.  I chose to use a pair to represent the tape state because there is a natural "left side" and "right side" of the tape based on what's to the left of the head and what's to the right.  (The current symbol was arbitrarily selected to be the head of the right side.)

 

In retrospect I think I would, if I chose to do this again, use a 3-tuple with {Left, Current, Right}.  This would get rid of the symbol/4 predicate at the expense of making the action/4 predicate a little more complex.

 

At any rate, perform/5 again calls the configuration predicate to extract the terminating states (FS), the running states (RS), the blank symbol (B) and the legal symbols (S).  It then checks if the current state (Q0) is one of the terminating states.  If it is, it unifies the input tape to the output tape and terminates the machine.

 

The rest of the predicate is where the work gets done.  The current state is checked against the legal running states.  The current symbol is extracted from the tape (symbol/4), it's checked against the legal list, the user rules are called (wrapped in once/1 because you can't be sure that the user's rules are deterministic).  The symbol to be written is checked for membership in the legal tape symbols, the returned action (left, stay, right) then executed.  The action/4 predicate is straightforward in implementation, with left-movement additionally broken out for clarity.  (One annoying feature is the requirement to pass the machine's blank symbol in to all the working predicates.  This is a requirement I was unable to think a way around.)  The predicate then loops by calling itself with the new state and input tape.

Type-based observations

Count the number of places where I call memberchk/2.  I check for terminating states and for legal running states.  I check for legal symbols.  This, my friends is type checking.  To be specific this is explicit type checking.  I also implicitly check for types in the action/4 predicate via left, stay, and right.  These are all run-time type checks.  If the types are wrong at any point, the machine aborts.  I also do determinacy checking implicitly through the use of once/1.  A more robust implementation would have to actually check the passed-in rules (through Prolog's homoiconicity) to ensure that all the states, symbols and actions are legal ones before the machine even runs.  That would be a serious pain in the ass to write, though, wouldn't it?

 

Oh, there's a bug in the code above.  See if you can spot it.  (I sure didn't!)  We'll talk about that bug later.

Enter Mercury

Mercury is a functional logic programming language with a very strict type checker (and mode checker and determinism checker).  It also has a syntax that is very similar to Prolog's so it was a natural as my first port of the universal Turing machine to another language.  Here's the code (again with all explanatory comments, etc. stripped; the full source is available of course).

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
:- module turing.

:- interface.

:- import_module list.
:- import_module set.

:- type config(State, Symbol)
    ---> config( initial_state  :: State,
                 halting_states :: set(State),
                 blank          :: Symbol ).

:- type action ---> left; stay; right.

:- func turing(config(S, T), pred(S, T, T, action, S), list(T)) = list(T).
:- mode turing(in, pred(in, in, out, out, out) is semidet, in) = out is det.

:- implementation.

:- import_module pair.
:- import_module require.

turing(C@config(Start, _, _), Rules, In) = Out :-
    (L - R) = perform(C, Rules, Start, ([] - In)),
    Out = append(reverse(L), R).

:- func perform(config(S, T), pred(S, T, T, action, S), S, pair(list(T))) = pair(list(T)).
:- mode perform(in, pred(in, in, out, out, out) is semidet, in, in) = out is det.
perform(C@config(_, H, B), Rules, State, In@(LIn-RIn)) = Out :-
    symbol(RIn, B, RNew, Sym),
    ( set.member(State, H) -> Out = In
    ; Rules(State, Sym, NSym, Action, NState) ->
        NLeft = pair(LIn, [NSym|RNew]),
        NRight = action(Action, B, NLeft),
        Out = perform(C, Rules, NState, NRight)
    ;
        error("an impossible state has apparently become possible") ).

:- pred symbol(list(S)::in, S::in, list(S)::out, S::out) is det.
symbol([],    B, [], B).
symbol([H|T], _, T,  H).

:- func action(action, S, pair(list(S))) = pair(list(S)).
action(left,  B, ([]-R))      = ([]-[B|R]).
action(left,  _, ([L|Ls]-Rs)) = (Ls-[L|Rs]).
action(stay,  _, T)           = T.
action(right, B, (L-[]))      = ([B|L]-[]).
action(right, _, (L-[R|Rs]))  = ([R|L]-Rs).

 

The code is almost the same as the Prolog code.  Mercury code involves more ceremony—module, import_module, func, pred, mode as well as the type declarations—but despite all the extra ceremony the code is only three lines longer.  (It would be only two lines longer if I didn't have to fix the bug from the Prolog code.)  What's not clear from the code here is how the machine is built, so here's a 3-state busy beaver by way of example:

 

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
:- type bbst ---> a ; b ; c ; halt.
:- type bbsym ---> '0' ; '1'.
:- func bbcfg = config(bbst, bbsym).
bbcfg = config(a, set([halt]), '0').
:- pred bb(bbst::in, bbsym::in, bbsym::out, action::out, bbst::out) is semidet.
bb(a, '0', '1', right, b).
bb(a, '1', '1', left,  c).
bb(b, '0', '1', left,  a).
bb(b, '1', '1', right, b).
bb(c, '0', '1', left,  b).
bb(c, '1', '1', stay,  halt).

 

Again, despite the extra ceremony, it actually takes about as much space as the Prolog version of the same thing:

 

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
bb_config(IS, FS, RS, B, S) :-
    IS = 'A',               % initial state
    FS = ['HALT'],          % halting states
    RS = [IS, 'B', 'C'],    % running states
    B  = 0,                 % blank symbol
    S  = [B, 1].            % valid symbols
busy_beaver('A', 0, 1, right, 'B').
busy_beaver('A', 1, 1, left,  'C').
busy_beaver('B', 0, 1, left,  'A').
busy_beaver('B', 1, 1, right, 'B').
busy_beaver('C', 0, 1, left,  'B').
busy_beaver('C', 1, 1, stay,  'HALT').

 

Note that in both cases the definition of a Turing machine to run is very similar to the mathematical notation you would use to define the machine: a definition of the states and symbols permitted and a set of rules in 5-tuples with current state, current symbol, symbol to write, action to take and the following state.

More type-based observations

On the surface these two blocks of code look very similar.  There is, however, only one run-time check in the Mercury code, and that is for the terminating state.  Nowhere else in the code do I check for states or symbols.  I don't even have to use the equivalent of once/1 when calling user rules.  Instead, if my bb/5 predicates contain any states or symbols that are not permitted, the Mercury compiler will vomit at me.  (And it catches errors I don't catch.  More on this later.)

 

By parametrizing the universal Turing machine via the config/2 type constructor, the compiler can know what legal symbols are permitted (those in bbsym) and what legal states are permitted (those in bbst).  If I try to use anything not in those types, the compiler will simply not allow it.

 

Even more important in this case is the determinism checking that Mercury performs.  It is this subset of Mercury's static checks that caught the bug in the Prolog implementation; a bug that slipped my notice despite reading and testing this code a thousand times over.  Note that action/4 in the Prolog code has, in effect, four clauses (two for left, one each for right and stay).  Now look at the action/3 function in the Mercury code, which has five clauses: two each for left and right and one for stay.  This is because action, which should be deterministic, was spotted as actually being semi-deterministic: it could fail.  I forgot to check for an empty tape on a right move.

 

This is 45 lines (with vertical whitespace) of code that I had gone over with a fine-toothed comb repeatedly.  This rather sizable bug still managed to slip through.  Mercury, however, caught it on the first try.  (Don't worry.  I'll be fixing the bug in the Prolog version soon.)  If a 45-line toy program can have a nasty bug like this slip through, can you imagine what kind of bugs slip into code that's 10,000+ lines long that's being worked on under time pressure?

So static typing is best, right?

Well, let's not go so fast here.  True the Mercury code is going to perform far better than the Prolog code, even if you use a hot, optimizing Prolog compiler.  The need to do runtime checks on each step of the machine is going to kill performance dead.  Further, even in this trivial, toy program a major bug slipped through.  This is under 50 lines of code!  (And I promise, I really did do this stupid thing; this isn't something I just inserted gratuitously for pedagogical reasons.)  The type checker caught the bug without breaking a sweat.  So better performance, fewer bugs: it's clearly static typing for the win.

 

But…

 

No.  See, as I said, this was exploratory programming for me.  I didn't know the problem domain well so I didn't know how to construct my code.  The final form you see in the Prolog version is about the fifth rendition of the architecture.  I started from a very primitive, non-modular baseline, modified it to accept a user-provided set of rules, further modified it to accept a user-provided configuration, added type checks and blank generation until the final version was seen.  Because I could freely do things that were unsafe, I was able to experiment with approaches, see the execution live and quickly make changes and test again.

Dynamic typing for the win, then?

Well… here again I have to dither.  Yes it took me about an afternoon to get the Prolog version up and running.  Yes it took me another whole afternoon to implement the Mercury version, despite knowing the problem domain by now.  Indeed yes, were I to have explored a declarative universal Turing machine in Mercury (or Haskell or other bondage & discipline typed languages), I probably wouldn't have done it even in two afternoons.  In fact, since I was doing this for fun, I might have just moved on to another project.

 

The key problem here is that, since I didn't really know the problem domain well (or, to be specific, didn't know how to represent the problem domain well in a non-imperative form), the type system would have interfered with my experimentation with the problem domain.  Even when I, by this time, knew the problem domain, I was wrestling with how to represent the types, where to use them, etc.  This is working on the plumbing, not the problem domain.  It brought dividends (efficient coding, elimination of run-time checks, bug-catching) but it had definite costs associated.

So which one's right then, dammit!

Thesis ; Antithesis → Synthesis

 

In short: neither is right, neither is wrong.  Both approaches, in this case, brought something to the table.  When I didn't understand the problem domain yet, the dynamic typing approach let me concentrate on the problem domain without the distraction of a pesky and irritating type system.  I had no illusions until the end that the code was safe or stable, but I understood what was going on quickly and could experiment with other approaches without headaches.  Once I'd solidified the overall framework, I could then go in and do my checks (performance-killing as they might be) and be reasonably certain that my machine was stable.

 

It was clear, however, after doing the Mercury port, that my "reasonable certainty" was wrong.  The compiler caught a bad bug for me.  Further, too, all the run-time checks meant that the universal Turing machine executing the rules could fail at any time.  This fosters defensive programming and, of course, if errors aren't checked can lead to a far bigger failure were this part of a larger system.  The Mercury version eliminates the need for defensive programming; the compiler will guarantee that stupid user mistakes (like illegal states or symbols) can't happen, even if the Turing machine's implementation gets changed and some old states that have been eliminated from the types are accidentally still retained in the rules.

 

So there is no "right one".  Each has its place in the developer toolbox.  Dynamically-typed languages are absolutely great for prototyping things when you're not positive of the outcome, the structure, the data types, etc.  Exploratory programming, in brief.  They are not, however, suited to building large, serious applications.  If you look at the currently-trendy techniques for making apps (since dynamically-typed languages are the trendy thing these days), you'll see a massive focus on testing.  And when you look at the tests that are advocated, many (most?) of them are exactly the kinds of tests that a statically-typed language does for you for free.  The problem with this is that … well, look up at my Prolog code and my shameful bug.  That's 45 lines of code there.  10,000 divided by 45 is …

 

No, for serious software, once you know the problem domain, you need some kind of type checking.  It can be static and built into the language (like Mercury, Haskell, or the MLs) or it can be external tooling (like Erlang's dialyzer suite).  If you don't have this, however, your code will be riddled with bugs that will kill your system.  Or, equivalently, render it grossly insecure—ask Rubyists about YAML bugs sometime….

 

Oh, and if you have such a system and don't use it, you're a fool who shouldn't be allowed near a software project.