BF (category)

BF is the category whose objects are each syntax for Brainfuck and whose arrows are polynomial-time reductions which preserve the underlying algebraic semantics. BF offers definitional answers to longstanding questions about Brainfuck variants and offers a unified view of Category:Brainfuck equivalents.

Motivation

Historically, wikipedia:model theory focused on the relationship between a single type theory and its term model, which is the least model that satisfies all of the entailments of the theory: if a fact is provably true in the type theory, then the term model should admit a construction via the proof which corresponds to that fact. From there, the term model serves as an initial object for a category of models, where arrows indicate that one model is structurally included in another. In the case of Brainfuck, we might study the relationship between Brainfuck's traditional syntax and the various possible semantics which can be assigned to that syntax.

However, the esoteric-languages community is fond of exploring alternate syntax as well as alternate semantics. Sometimes the transformation from one syntax to another is not reversible or efficiently computable; sometimes it denotes an expanded semantics.

Definition

Let algebraic Brainfuck be a monoid. The objects of BF are monoidal grammars along with monoid-preserving homomorphisms to algebraic Brainfuck. The arrows of BF are monoidal grammar homomorphisms which are computable in polynomial time over the number of terminals in the input, such that the resulting diagram commutes.

BF could be thought of as a slice category, particularly a category of monoids over algebraic Brainfuck. However, it's important to note that each object of BF also comes with a grammar which can give additional structure to the monoid, and this grammar must be respected. For example, loops are often designated by multiple terminals along with production rules which pair and nest them, and the pairing/nesting must be preserved by arrows.

Properties

The initial object of BF is equivalent to the algebraic syntax of algebraic Brainfuck, with an identity homomorphism. Presentations of the initial object also include the original Brainfuck syntax and all trivial substitutions, as well as any non-trivial substitutions which can be encoded as context-free grammars.