Tree @develop-2023-1 (Download .tar.gz)
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
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,
-+ 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
- 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 ⟦
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 ⟦
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.
git clone https://git.catseye.tc/Burro/
- Add BSD license. Chris Pressey 1 year, 2 days ago
- Improve the exposition. Chris Pressey 1 year, 2 days ago
- Add example programs loaded initially into the HTML5 installation. Chris Pressey 1 year, 2 days ago
- Finish editing the explanation (this draft of it, anyway.) Chris Pressey 1 year, 2 days ago
- Make build.sh work with containerized hastec. Chris Pressey 1 year, 5 days ago
- Some edits, in-progress, to the README. Chris Pressey 1 year, 6 days ago
- The Turing-completeness proof is incorrect, so remove it for now. Chris Pressey 1 year, 6 days ago
- Move Language/Burro.lhs to Language/Burro/Definition.lhs. Chris Pressey 3 years ago
- Add some test cases that show that the idiom works. Chris Pressey 3 years ago