Burro

This is the reference distribution for Burro, a formal programming language whose programs form a group (an algebraic structure from group theory). The precise sense of this statement is explained below, but the following can be taken as a high-level summary: For every Burro program text, there exists an "annihilator" program text which, when concatenated to the original program text, forms a "no-op" program.

For the definition of the Burro language version 1.0, which was the first attempt to do this but does not actually succeed in forming a group, see the file doc/burro-1.0.md.

For the definition of the Burro language version 2.0, whose program do indeed form a group, see the Literate Haskell file Language/Burro/Definition.lhs in the src directory. This definition also serves as a reference implementation of the language.

The sense in which Burro programs form a group

The documentation efforts for versions 1.0 and 2.0 of Burro don't do a really good job of explaining what is meant by the set of Burro programs "forming a group". Burro 1.0 tries to explain it by defining a new concept, a "group over an equivalence relation", and 2.0 just carries on with that idea without elucidating it. This new concept is not really necessary, however, and I'll try to provide a brief explanation here that is more in line with conventional mathematical exposition.

Let B be the set of syntactically valid Burro program texts (hereinafter simply "program texts"). B is defined by an inductive definition, so it can be thought of as an algebraic structure: a set accompanied by a number of operations of various arities.

Every program text t represents some Burro program, which we will denote by ⟦t⟧. The meaning of such a program is determined from t by the semantics of the Burro language, which are syntax-directed. And because, in Burro, we are happy to ignore most operational aspects of execution, we think of such a program as a function that maps inputs to outputs; and for this reason, for any given program, there may be multiple different program texts that represent it. For example, +- and -+ represent the same program. To put it in other words, the mapping ⟦∙⟧ is not injective.

Furthermore, because ⟦∙⟧ is defined in a syntax-directed fashion, it is a homomorphism between B and the set of Burro programs; for each of the operations of the algebra on B there is a corresponding operation on the functions in the set of Burro programs.

Even furthermore, because ⟦∙⟧ is a homomorphism, it induces an equivalence relation (indeed, a congruence relation) between the two sets. For any program texts s and t, if ⟦s⟧ = ⟦t⟧, we say s ~ t, or (in English) we say that s and t are congruent program texts.

We can take the quotient of B by this congruence relation to obtain the algebraic structure B/\~. This is the set of all Burro programs representable by B, which is by definition the set of all Burro programs.

We now get into what we mean by "group language". Because B/\~ "inherits" all of the operations from B, it has two properties:

• The identity function is an element of B/\~, because it is the meaning of the program text e.
• Because two program texts in B can be concatenated to form a new program text in B, two programs in B/\~ can be composed in analogous way to form a new program in B/\~.

In addition, B/\~ has the following property that B does not have:

• For every program p in B/\~, there exists another program q in B/\~ such that the composition of these two programs is the identity function ⟦e⟧.

The three properties of B/\~ given in these bullet points indicate that B/\~ is a group, for these are the group axioms.

Beyond that, there are two things that, although possibly trivial as they follow directly from the definitions, are well worth noting.

First, because the program q is in B/\~, and because B/\~ is the result of taking the quotient of the congruence relation, we know there exists at least one program text t that represents q.

Second, because ⟦∙⟧ is defined in a syntax-directed fashion, we can do the following: Given a program text s, we can find ⟦s⟧ (call it p), and then we can find the function q that when composed with p results in the identity function ⟦e⟧, and lastly we can find a program text t such that ⟦t⟧ = q.

(In fact, the reason we know we can find such a t is because we have syntax-directed rules for finding a t from any given s, and we can show that the composition of ⟦s⟧ and ⟦t⟧ always equals ⟦e⟧.)

So, that is the sense in which we say that the set of Burro programs forms a group, and in which every syntactically valid Burro program text has an annihilator.