Algebraic Brainfuck
Algebraic Brainfuck is the semantics of a Brainfuck program upon a tape of cells.
Motivation
Brainfuck has many documented derivatives, variants, and alternate grammars when considered as syntax. However, they often have one single semantics. By isolating this semantics, we can study it without worrying about any syntactic details.
As a Data Type
A semantics is a collection of actions. We can imagine that this collection is a set or a type and characterize it in terms of which actions can be built from syntax. Following mathematical tradition, we'll introduce a common metasyntax which specifies the actions directly without counting characters, to avoid the standard questions brought up by languages like Unary. Consider Brainfuck programs which add to the current cell:
+ ++ +++
We may directly denote the actions that they have upon that cell and forget the number of machine instructions required. For this purpose, we will adopt a blend of syntax from Faase and Couch which adheres to Zephyr ASDL:
plus(1) plus(2) plus(3)
So far, this looks like yet another Brainfuck equivalent, as it should. However, notice how we encode subtraction:
plus(-1) plus(-2) plus(-3)
Semantically, there is no separate symbol for subtraction. The subset of subtractions still exists; it is a subset of all `plus(j)` operations where the parameter `j` is negative. A similar situation arises for moving the head. Also, loops should probably always be paired and matched, so we'll represent loops with a recursive type: a type of actions whose components are themselves actions. Here is Zephyr ASDL for the complete semantics of Brainfuck:
bf = plus(int) | right(int) | input | output | loop(bf*)
Alternatively, here is wikipedia:Haskell-style syntax for an wikipedia:algebraic data type:
data BF = Plus Integer | Right Integer | Input | Output | Loop [BF]
In contrast to bfmacro, where the head's location is usually known, the full semantics of Brainfuck does not know where the head is. Instead, to evaluate an action, we must specify a tape and a location on that tape.
As Idioms
Many short Brainfuck programs form idioms by synthesizing the functionality traditionally associated with rich instruction sets for physical hardware. For example, this program sets a register to zero:
[-]
We can give a name to this program by giving a name to the action associated with it, like "zero". Similarly, we will give a name to the semantic action:
zero = loop([plus(-1)])
This is almost the same as Faase and Couch's "zero" macro, except that the pointer head is not located. Let's try to encode another simple program from Faase and Couch, "move", which zeros out the current cell while adding its current value to another cell at a fixed offset. We'll use an integer to encode that offset and then write out:
move(j) = loop([plus(-1), right(j), plus(1), right(-j)])
This is the expansion that Faase gives, and Couch implements it in exactly this way. However, note that the two actions performed by this idiom are writes to two different cells, and so they should commute. Indeed, we can also write:
move(j) = loop([right(j), plus(1), right(-j), plus(-1)])
This shows us that, in a certain sense, the semantics can deduplicate equivalent programs. It also explains a well-known frustration to Brainfuck compiler authors, who often have efficient primitive operations for actions like `zero` or `move()`; the former is easier to recognize than the latter, because it only has one form instead of two. Of course, a thoughtful Brainfuck veteran will usually counter that there is another way to express `zero`:
zero = loop([plus(1)])
And that we usually don't use it because it is more expensive when cell values are small, but also that compilers tend to not recognize it because it is not used often.
Listing of Idioms
Where possible, names follow Faase and Couch. Equations are not exhaustive; `scalemove` can appear as either of two patterns, `scalemove2` has four patterns, etc.
zero = loop([plus(-1)]) = loop([plus(1)]) scalemove(j,s) = loop([plus(-1), right(j), plus(s), right(-j)]) move(j) = scalemove(j,1) scalemove2(j,s,k,t) = loop([plus(-1), right(j), plus(s), right(k-j), plus(t), right(-k)]) move2(j,k) = scalemove2(j,1,k,1) set(k) = [zero; plus(k)] omega(k) = [set(k); loop([])]
As a Monoid
The semantics has a standard wikipedia:monoid where the identity corresponds to the empty Brainfuck program. To unpack that, a monoid is like a list of objects where some lists are equivalent to other lists. The main operation in a monoid is list concatenation, taking two lists and putting one before the other. The identity in a monoid is like the empty list; concatenation with the identity returns the other argument unchanged. We will call the identity `id`.
With simpler words: let us consider lists of actions rather than individual actions. There are several reasons for this. One is to answer the question: what is `plus(0)`? It should be zero `+` or zero `-` instructions, but how should we denote that? We use `id`:
id = plus(0) = right(0)
Those aren't written as lists, but we'll say that they're like singletons (lists of length one.) A second motivation is to consider optimizations. The following programs are equivalent:
+ ++ +++
So their semantics should reflect that:
[plus(j), plus(k)] = plus(j + k)
This enables a form of wikipedia:strength reduction. Here are two more rules from standard Brainfuck folklore:
[right(j), right(k)] = right(j + k) [loop(xs), loop(ys)] = loop(xs)
So the reader is invited to check that the following Brainfuck expression optimizes to `zero` despite the undecidability of (the Halting of) the second loop:
[-]><++--[>+]
For comparison, the traditional way to prove this sort of result involves wikipedia:abstract interpretation over the tape and pointer head. The algebraic manipulation of a monoid is much neater!
There is a cost, though. There are no non-trivial equations involving input or output; the algebra is detached from the tape and also from any input data, so the effect of input is unpredictable. Input and output actions can be added or removed from loops which provably won't execute, but that's the limit of what this monoid can handle.
Listing of Strength Reductions
Listings are generally given from stronger to weaker.
plus(0) = right(0) = id [plus(j), plus(k)] = plus(j + k) [right(j), right(k)] = right(j + k) [loop(xs), loop(ys)] = loop(xs) [loop([loop(xs)]) = loop(xs) [plus(j), zero] = zero
Models of Generalized Brainfuck
This section considers the behavior of the cells under increment and the tape under navigation.
Generalized Cells
So far, we have required that there be one increment operation per integer. We could imagine that increment is the lone generator for a wikipedia:free group (with decrement as its inverse) and ask for the possible other models. It turns out that there is only one such free group, the integers themselves! (See Rijke, Bakke, & Prieto-Cubides 2022 for a proof in Agda.) However, when Böhm specified P", they fixed an arbitrary modulus m for each cell, which is equivalent to specifying a free group with one generator and one equality. Without loss of generality, we take that equality to be m=0. When m=256 we recover traditional semantics.
Not all of our algebraic rules hold over integer cells. In particular, it's not known how to zero a cell; the zero idiom given earlier will enter an infinite loop if the current cell is negative.
Generalized Tapes
Similarly, our tape of cells has to support a single head moving left and right, and traditionally the only possibilities are as above: tape addresses are either integers or natural numbers (mod m). However, because the tape is parameterized over a choice of cells, we may consider other topologies which "twist" those cells so that some addresses are "twisted" views.
For a basic example, consider a wikipedia:Möbius strip. Take a tape of finite length with cells that have power-of-two sizing, so that each cell may be expressed as a bitstring, and imagine gluing the ends together with a "twist" of bitwise negation: when the head navigates across the glue, all cells are bitwise negated. This trick can be repeated with any cellwise wikipedia:involution.
Another basic example involves reflecting the tape. Let the tape again be of finite length, with any cells, and consider gluing each end to itself. When the head navigates across either end of the tape, its sense of left and right is switched.
Are there other possibilities? There are a few, but a major limitation is the 1D address space: we can only move the head in one dimension, so it's pointless to consider embeddings in higher dimensions because we can't reach them. The second example exhibits what GPU and DSP programmers call "mirrored" memory layout, as opposed to "tiled" memory layout in classic Brainfuck; other possibilities include adding "border" or "padding" cells with special values, or "port" cells which trigger I/O. The first example generalizes to any group of finite order which acts neatly on cells. These can be mixed and matched as desired, too.
Not all of our algebraic rules hold over generalized tapes, either. Even the basic idiom for copying a cell may go wrong if it crosses a twisted glued edge.
Formalizing the Semantics
The above algebraic work is syntactic and thus might not be fully convincing to the careful mathematician. Please imagine that this section contains an implementation of the semantics in terms of a serialized stream of messages exchanged between an interpreter and a tape, along with an analogy for how this is like the communication between a CPU and a memory controller.
Examples
- [1] an interpreter by User:Corbin demonstrating a tagless final encoding of the algebra