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`](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`](src/Language/Burro/) 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.