Spelunking in the Turing Tarpit

Expedition through an esoteric landscape

Hello. In this series of articles I'm going to talk through an attempted implementation of a toolchain and emulator for an obscure turing-tarpit called a tag system. Along this path some parsers were written in at least 3 frameworks, a semi-working compiler or two in a few languages, some interpreters of varrying levels of finish, and a lot of bugs. I abandoned the project before completion but this is not a tale of woe and grief, hopefully there's some interesting stuff as well.

You may be wondering why I set out on this journey in the first place. The answer is essentially "because it is awesome", as one might expect. I hope that you'll agree with me by the end of this series.

The rough outline for the journey is this introduction, including this bit describing the introduction (even this aside). Next we'll describe the tag system in pretty good detail. We will focus on Hao Wang's proof of computability as that is what I spent the most time on though other proofs will be referenced. Once we firmly understand what makes these things computable we can dive into the interpreter written in C. This part will cover the lofty dreams, goals, and necessary optimizations that were never meant to be. From there we can climb upwards to the intermediate language (termed The W-Machine by Wang). Here we'll discuss a simple interpreter, compiler, and parser which served as my introduction to rust. Nearing the end now we'll cover the elvm compiler [0] and my attempt at another backend. Finally we'll perform a meta-analysis of my failures. There is quite a bit of overlap so each article may cover some things that another will in greater detail. What can you do? In case you don't care, here's most of the code I wrote for this project.

A Map Through the Tag Toolchain

Riveting stuff. Now that we have the map laid down I can ramble a bit. Tag systems! What a ridiculous computer. These things are used in all kinds of extremely esoteric nonsense. Ever wondered how Matthew Cook proved rule-110 was turing complete? Me too, but I know it involves something about simulating a tag system, eventually. But this is not all, a bunch of computer nerds deploy these machines in all manner of nooks and crannies across the computing landscape to demonstrate just how rich in computation we are nowadays. I trust this is enough evidence to convince even the most ardent skeptic of the usefulness of this work.

When I first read the wikipedia article on tag systems I thought "how do you write a program for this?" I casually searched around but was unable to find anything giving insight. I then searched a bit less casually and asked around on the esolang IRC but the replies focused on implementing an interpreter and not programming the tag system. At this point I began to read through the proofs of turing completeness. The proofs were so good that I felt comfortable writing real tag programs. But before you can write the program, you need the emulator to test it. And before you can debug the emulator you need programs to excise the proper paths. And to get these programs you need to generate them from easier programs. Eventually you're writing an emulator for an intermediate language so that you can debug your compiler in order to debug your interpreter in order to debug your compiler.

And this is when you take stock. Eventually it was no longer interesting because the problems I was solving were so unrelated to the one I wanted to solve. I very much wanted to run "hello world" on the tag interpreter after it was transformed from C to w-machine to tag to binary but I guess not that much. The unfortunate part is that the most interesting aspects are not even implemented because the necessary frameworks are not in place yet.

But I am getting ahead of myself. Let's start from the beginning. Let's examine The Tag System.