Commit 17fdd9d86f3929e71e9d51c2feb5d464aed25401 - Burro

Some edits, in-progress, to the README. Chris Pressey 2 years ago

1 changed file(s) with 19 addition(s) and 15 deletion(s). Raw diff Collapse all Expand all

+19

-15

README.md less more

1	1	=====
2	2
3	3	This is the reference distribution for Burro, a formal programming language
4		whose denoted programs form a group under concatenation of their program texts.
	4	whose programs form a group (in a particular sense described below). For
	5	every Burro program text, there exists an "annihilator" program text which,
	6	when concatenated to the original program text, forms a "no-op" program.
5	7
6	8	For the definition of the Burro language version 1.0, which was the
7	9	first attempt to do this but does not actually succeed in forming a group,
8	10	see the file [`doc/burro-1.0.md`](doc/burro-1.0.md).
9	11
10		For the definition of the Burro language version 2.0, which does indeed
11		form a group, see the Literate Haskell file
	12	For the definition of the Burro language version 2.0, whose program do
	13	indeed form a group, see the Literate Haskell file
12	14	[`Language/Burro/Definition.lhs`](src/Language/Burro/) in the
13		`src` directory. This also serves as a reference implementation of
14		the language, and includes a sketch of a proof that Burro is Turing-complete.
	15	`src` directory. This definition also serves as a reference implementation
	16	of the language.
15	17
16	18	The sense in which Burro programs form a group
17	19	----------------------------------------------
18	20
19		The language version 1.0 and 2.0 documents don't do a great job of explaining
20		what is meant by the set of Burro programs forming a group — 1.0 tries
21		to explain by defining a new concept, a "group over an equivalence relation",
22		and 2.0 just carries on with the idea without elucidating it. This new
23		concept is not necessary and I'll try to briefly provide a more conventional
24		description here.
	21	The documentation efforts for versions 1.0 and 2.0 of Burro don't do a
	22	really good job of explaining what is meant by the set of Burro programs
	23	"forming a group". Burro 1.0 tries to explain it by defining a new concept,
	24	a "group over an equivalence relation", and 2.0 just carries on with that idea
	25	without elucidating it. This new concept is not necessary, however, and I'll
	26	try to briefly provide a more conventional explication here.
25	27
26	28	Let B be the set of syntactically valid Burro program texts (hereinafter
27	29	simply "program texts"). B is defined by an inductive definition, so can be

29	31
30	32	Every program text _t_ represents some Burro program, which we will denote by
31	33	⟦_t_⟧. But because we typically ignore some operational aspects of execution,
32		multiple program texts can represent the same program. For example,
33		`+-` and `-+` represent the same program.
	34	for every program, there may be multiple program texts that represent it.
	35	For example, `+-` and `-+` represent the same program.
34	36
35	37	In other words, ⟦⟧ is not injective. It is a homomorphism between B and the
36		set of Burro programs, and as such it induces an equivalence relation. If,
37		for program texts _s_ and _t_, ⟦_s_⟧ = ⟦_t_⟧, we say _s_ ~ _t_.
	38	set of Burro programs, and as such it induces an equivalence relation.
	39	For any program texts _s_ and _t_, if ⟦_s_⟧ = ⟦_t_⟧, we say _s_ ~ _t_.
38	40
39	41	We can take the quotient of B by this equivalence relation to obtain the
40	42	algebraic structure B/\~. This is the set of all Burro programs representable
41	43	by B, which is by definition the set of all Burro programs.
	44
	45	- - - -
42	46
43	47	However, in [`Language/Burro/Definition.lhs`](src/Language/Burro/)
44	48	we go on to show that B/\~ is not