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.