Tree @turing-completeness-proof (Download .tar.gz)
This is the reference distribution for Burro, a formal programming language whose denoted programs form a group under concatenation of their program texts.
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, which does indeed
form a group, see the Literate Haskell file
Language/Burro/Definition.lhs in the
src directory. This also serves as a reference implementation of
the language, and includes a sketch of a proof that Burro is Turing-complete.
The sense in which Burro programs form a group
The language version 1.0 and 2.0 documents don't do a great job of explaining what is meant by the set of Burro programs forming a group — 1.0 tries to explain by defining a new concept, a "group over an equivalence relation", and 2.0 just carries on with the idea without elucidating it. This new concept is not necessary and I'll try to briefly provide a more conventional description here.
Let B be the set of syntactically valid Burro program texts (hereinafter simply "program texts"). B is defined by an inductive definition, so can be thought of as an algebraic structure with a number of operations of various arities.
Every program text t represents some Burro program, which we will denote by
⟦t⟧. But because we typically ignore some operational aspects of execution,
multiple program texts can represent the same program. For example,
-+ represent the same program.
In other words, ⟦⟧ is not injective. It is a homomorphism between B and the set of Burro programs, and as such it induces an equivalence relation. If, for program texts s and t, ⟦s⟧ = ⟦t⟧, we say s ~ t.
We can take the quotient of B by this equivalence 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 go on to show that B/\~ is not
merely an algebraic structure, it is in fact a group. In particular, for every
Burro program a in B/\~ there exists a unique Burro program b in B/\~
such that a * b = e, where * is program composition and e is the null program.
From this, working backwards through the homomorphism (so to speak), we can infer that, for every program text s in B there exists a program text t in B such that ⟦s⟧ * ⟦t⟧ = ⟦s t⟧ = e. (In fact, for every s there are infinitely many such t's.)
This is the sense in which 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/
- Establish some of the helper functions used in the translation. Chris Pressey 2 years ago
- Markdown-README-is-link-to-Literate-Haskell-file trick. Chris Pressey 2 years ago
- Initial sketch of (new) Turing-completeness proof. Chris Pressey 2 years ago
- Move Language/Burro.lhs to Language/Burro/Definition.lhs. Chris Pressey 2 years ago
- Add some test cases that show that the idiom works. Chris Pressey 2 years ago
- Continue to work out the extensible conditional idiom. Chris Pressey 2 years ago
- Rewrite parts of the conditional idiom exposition for clarity. Chris Pressey 2 years ago
- Develop conditional idiom, rename tests to Tests.md, add driver. Chris Pressey 2 years ago
- Develop the idiom further. Chris Pressey 2 years ago