git @ Cat's Eye Technologies Burro / 7c8ac3c
Attempt more conventional description of how a group is involved. Chris Pressey 5 years ago
1 changed file(s) with 37 addition(s) and 1 deletion(s). Raw diff Collapse all Expand all
+37
-1
README.md less more
11 =====
22
33 This is the reference distribution for Burro, a formal programming language
4 whose programs form a group under concatenation of their program texts.
4 whose denoted programs form a group under concatenation of their program texts.
55
66 For the definition of the Burro language version 1.0, which was the
77 first attempt to do this but does not actually succeed in forming a group,
1111 form a group, see the Literate Haskell file `Burro.lhs` in the `src`
1212 directory. This also serves as a reference implementation of the language,
1313 and includes a sketch of a proof that Burro is Turing-complete.
14
15 The sense in which Burro programs form a group
16 ----------------------------------------------
17
18 The language version 1.0 and 2.0 documents don't do a great job of explaining
19 what is meant by the set of Burro programs forming a group — 1.0 tries
20 to explain by defining a new concept, a "group over an equivalence relation",
21 and 2.0 just carries on with the idea without elucidating it. This new
22 concept is not necessary and I'll try to briefly provide a more conventional
23 description here.
24
25 Let B be the set of Burro program texts. Burro program texts are just
26 strings of symbols, so B is a monoid under concatenation.
27
28 Every Burro program text _t_ represents some Burro program ⟦_t_⟧.
29 But because we typically ignore some operational aspects of execution,
30 multiple program texts can represent the same program. For example,
31 `+-` and `-+` represent the same program.
32
33 In other words, ⟦⟧ is not injective, and because it is not injective,
34 it induces an equivalence relation. If, for Burro program texts _s_ and _t_,
35 ⟦_s_⟧ = ⟦_t_⟧, we say _s_ ~ _t_.
36
37 We can take the quotient of B by this equivalence relation
38 to obtain the quotient semigroup B/~. This is the set of all representable
39 Burro programs. And in fact B/~ is not only a semigroup, it is also a group.
40
41 Because B/~ is a group, for every program _a_ in B/~ there exists a
42 unique program _b_ in B/~ such that _a_ * _b_ = e, where * is program composition
43 and e is the null program.
44
45 From this we infer that for every program text _s_ in B there exists a program
46 text _t_ in B such that ⟦_s_⟧ * ⟦_t_⟧ = ⟦_s_ _t_⟧ = e.
47
48 This is the sense in which Burro programs form a group, and in which every
49 Burro program text has an annihilator (in fact, it has infinitely many.)