git @ Cat's Eye Technologies Cabra / 1023199
Initial import of Cabra version 1.0 revision 2007.1101 sources. Cat's Eye Technologies 11 years ago
2 changed file(s) with 562 addition(s) and 0 deletion(s). Raw diff Collapse all Expand all
+415
-0
doc/cabra.html less more
0 <html>
1 <head>
2 <title>The Cabra Programming Language</title>
3 </head>
4 <body>
5
6 <h1>Cabra</h1>
7
8 <p>November 2007, Chris Pressey, Cat's Eye Technologies</p>
9
10 <h2>Introduction</h2>
11
12 <p>Cabra is a formal programming language whose programs form a dioid (an idempotent semiring)
13 over its semantic equivalence relation under the operations of parallel composition (additive)
14 and sequential composition (multiplicative.) (Say <em>that</em> five times fast!)</p>
15
16 <p>Cabra is the successor to <a href="/projects/burro/">Burro</a>, a programming language
17 whose programs form a simpler algebraic structure: a group.
18 Unlike Burro, however, Cabra is not derived from Brainfuck in any way.
19 And, while the word "burro" is Spanish for "donkey", the word "cabra" is Spanish for "goat."
20 (Also, in reality, you'd be hard-pressed to do any actual
21 <em>programming</em> in Cabra... but it <em>is</em> a formal language.)</p>
22
23 <p>Reading the Burro documentation is definately recommended for getting the most out of Cabra,
24 as several of the same issues are dealt with there. Notably, the notion of a <em>group over an equivalence
25 relation</em> is introduced there in order to make sense of how program texts (syntax) can be manipulated in
26 tandem with the programs (semantics) they represent. In short, many different program texts are equivalent to
27 the same (abstract) program, so the equality operator = used in the group axioms is simply replaced
28 by the equivalence operator, &equiv;. Obviously, this technique isn't restricted to groups, and the idea can be
29 extended to that of any <em>algebra over an equivalence relation</em>, and it is this notion that
30 is applied in Cabra to dioids.
31
32 <p>The original intent of Cabra was to devise a language whose programs formed a <em>ring</em>
33 under parallel and sequential composition operations. Selecting a semantics for parallel composition that
34 fulfill all the ring axioms presents a number of problems, which are discussed below.
35 As a compromise, the axioms for <em>idempotent semirings</em> were chosen instead.
36 Idempotent semirings, sometimes called <em>dioids</em>, lack the additive inverses that rings have,
37 but unlike rings, have an idempotent additive operator.</p>
38
39 <p>Let's get straight to it.</p>
40
41 <h2>Language Definition</h2>
42
43 <p>Every Cabra program takes, as input, an <em>input set</em>, which is a set of non-negative integers.
44 Every Cabra program either produces an <em>output set</em>, which is also a set of non-negative integers,
45 or it fails to terminate.</p>
46
47 <p>A Cabra program is defined inductively as follows.</p>
48
49 <p>The instruction <code>SET <var>n</var></code>, where <var>n</var> is any non-negative integer,
50 is a Cabra program. The output set of this program is the union of
51 the input set and the singleton set {<var>n</var>}. (The output set is just like the input set
52 except that it also includes <var>n</var> if it was missing from the input set.)</p>
53
54 <p>The instruction <code>UNSET <var>n</var></code>, where <var>n</var> is any non-negative integer,
55 is a Cabra program. The output set of this program is the set difference of the input set and
56 the singleton set {<var>n</var>}. (The output set is just like the input set
57 except that it never includes <var>n</var>, even if <var>n</var> was included in the input set.)</p>
58
59 <p>If <var>a</var> and <var>b</var> are Cabra programs, then <code>IFSET <var>n</var> THEN <var>a</var> ELSE <var>b</var></code>
60 is a Cabra program, where <var>n</var> is any non-negative integer. If <var>n</var> is a member of the input set of the <code>IFSET</code> program,
61 then the input set is used as the input set of <var>a</var>, and the output set of <var>a</var> is used as the output set of the <code>IFSET</code>;
62 <var>b</var> is ignored. Conversely, if <var>n</var> is not a member of the input set the <code>IFSET</code>,
63 then the input set is used as the input set of <var>b</var>, and the output set of <var>b</var> is used as the output set of the <code>IFSET</code>;
64 <var>b</var> is ignored. (<code>IFSET</code> is the conditional statement form.)</p>
65
66 <p>If <var>a</var> and <var>b</var> are Cabra programs, then <code><var>a</var>*<var>b</var></code>
67 is a Cabra program. The input set of <code><var>a</var>*<var>b</var></code> is used as the input set of <var>a</var>.
68 The output set of <var>a</var> is used as the input set of <var>b</var>. The output set of <var>b</var> is used
69 as the output set of <code><var>a</var>*<var>b</var></code>. (This is sequential composition; <var>a</var> is
70 executed, then <var>b</var>. A more usual notation might be <code><var>a</var>;<var>b</var></code>.)</p>
71
72 <p>If <var>a</var> and <var>b</var> are Cabra programs, then <code><var>a</var>+<var>b</var></code>
73 is a Cabra program. The input set of <code><var>a</var>+<var>b</var></code> is used as the input set of
74 both <var>a</var> and <var>b</var>. The output set of whichever of <var>a</var> or <var>b</var>
75 terminates first is used as the output set of <code><var>a</var>+<var>b</var></code>. See below for the
76 definition of "terminates first." (This is parallel composition, with
77 final result determined by a kind of race condition. A more usual notation might be <var>a</var>||<var>b</var>.)</p>
78
79 <p>If <var>a</var> is a Cabra program, then <code>(<var>a</var>)</code> is a Cabra program.
80 This is just the usual usage of parentheses to alter precedence. Without parentheses,
81 <code>*</code> has a higher precedence than <code>+</code>, which has a higher
82 precedence than <code>IFSET</code>. For example, this means that
83 <code>IFSET 42 THEN SET 51 ELSE SET 5 * SET 6 + SET 7</code>
84 is parsed as <code>IFSET 42 THEN (SET 51) ELSE ((SET 5 * SET 6) + SET 7)</code>.</p>
85
86 <p>The instruction <code>SKIP</code> is a Cabra program. The output set of <code>SKIP</code>
87 always equals the input set. (<code>SKIP</code> is a no-op.)</p>
88
89 <p>The instruction <code>BOTTOM</code> is a Cabra program. Regardless of the input set,
90 this program always fails to terminate. (<code>BOTTOM</code> is an infinite loop.)</p>
91
92 <p>Were I a pedantic mathematician, here's where I'd mention how nothing else is a Cabra program.
93 As if I could be <em>so</em> sure about that.</p>
94
95 <h3>Terminates First</h3>
96
97 <p>We still need to define what it means for one Cabra program to "terminate before" another, different Cabra program.
98 Execution of a Cabra program is considered to take a non-negative integral number of imaginary things
99 called <em>cycles</em>. A Cabra program <var>a</var> terminates before <var>b</var> if the number of cycles taken by <var>a</var>
100 on some input set <var>S</var> is less
101 than the number of cycles taken by <var>b</var> on <var>S</var>; or, if the number of cycles taken by <var>a</var> on <var>S</var> is the same as the number
102 of cycles taken by <var>b</var> on <var>S</var>, then <var>a</var> terminates before <var>b</var> if <var>a</var> has a smaller lexical order than <var>b</var>.
103 (If <var>a</var> and <var>b</var> have the same lexical order
104 then <var>a</var> = <var>b</var> and "terminate before" is meaningless because it only defined between
105 two different Cabra programs.)</p>
106
107 <p>The formula for calculating cycles taken in general depends on both the program and its input set, but is deterministic
108 in the sense that the same program on the same input set will always take the same number of cycles.
109 (This isn't the real world where clock speeds vary at +/-0.01% or anything like that. It is as if execution is
110 synchronous; as if, for example, on a single computer,
111 one cycle of program <var>a</var> is executed, then one cycle of <var>b</var>, and so forth, until one or the other
112 terminates.)</p>
113
114 <ul>
115 <li><code>SKIP</code> takes 0 cycles.</li>
116 <li><code>BOTTOM</code> takes an infinite number of cycles.</li>
117 <li><code><var>a</var>*<var>b</var></code> takes the sum of the number of cycles taken by <var>a</var> and the number of cycles taken by <var>b</var>.</li>
118 <li><code><var>a</var>+<var>b</var></code> takes the either the number of cycles taken by <var>a</var> or the number of cycles taken by <var>b</var>, whichever is fewer.</li>
119 <li><code>IFSET <var>n</var> THEN <var>a</var> ELSE <var>b</var></code> takes either the number of cycles taken by <var>a</var> or the number of cycles taken by <var>b</var>,
120 whichever was selected for execution.</li>
121 <li><code>SET <var>n</var></code> takes <var>n</var> cycles if <var>n</var> was not already set, but only 1 cycle if it was already set.</li>
122 <li><code>UNSET <var>n</var></code> always takes 1 cycle.</li>
123 </ul>
124
125 <p>In fact, other formulae are possible. The somewhat unusual determination of cycles in the case of <code>SET <var>n</var></code>
126 is mainly to keep things interesting by ensuring that the number of cycles is dependent upon the contents of the input set.</p>
127
128 <p>Probably goes without saying, but to state it anyway: for a program <var>a</var> which is an element of a set of programs <var>P</var>,
129 we say <var>a</var> <em>terminates first</em> (with respect to <var>P</var>) if it terminates before every other program in <var>P</var>.</p>
130
131 <h3>Lexical Order</h3>
132
133 <p>The formula for calculating lexical order depends only on the program. It acts as a "tiebreaker" when two programs take the same number of cycles.</p>
134
135 <p>For primitive programs: <code>SKIP</code> comes before <code>UNSET 0</code>
136 which comes before <code>UNSET 1</code> which comes before <code>UNSET 2</code>, etc.
137 All of these come before <code>SET 0</code>, which comes before <code>SET 1</code>, etc.
138 And all of these come before <code>BOTTOM</code>.</p>
139
140 <p>For compound programs, the ordering is <code>IFSET <var>n</var> THEN <var>a</var> ELSE <var>b</var></code>
141 comes before <code>IFSET <var>n+1</var> THEN <var>a</var> ELSE <var>b</var></code>
142 comes before <code><var>a</var>+<var>b</var></code> comes before <code><var>a</var>*<var>b</var></code>.</p>
143
144 <p>All primitive programs come before non-primitive programs, and in general, programs with shorter length
145 (measured in terms of number of subterms) come before those with longer length. In programs with the same
146 length, subterms are compared left-to-right. (This happens to be the same kind of lexical ordering as you
147 get in Haskell when you declare a data type as <code>deriving (Ord)</code>.)</p>
148
149 <h3>Comments</h3>
150
151 <p>Oh, but I can hear you objecting now: <em>Waitaminnit! This language is totally weak. You can't do hardly anything with it.</em></p>
152
153 <p>True enough. Cabra is nowhere close to being a real programming language. But I decided to design it this way anyway,
154 for a couple of reasons.</p>
155
156 <p>One reason is to demonstrate that these algebraical problems involving parallel composition occur even for what would be
157 very small subsets of a "real" programming language. You can imagine a full-fledged version of Cabra with
158 variables, arrays, <code>WHILE</code> loops, input/output, and the like, but you can readily see that these ameliorations don't make the central
159 problems any easier.</p>
160
161 <p>Another reason is that Cabra, despite almost being, say, just a kind of algebraical structure, <em>looks</em> a lot
162 like the beginnings of a programming language. It's got a conditional form, and imperative update. It almost looks like an overspecified language &mdash;
163 heck, a <em>machine</em> &mdash; because of the definition of how parallel composition works in terms of cycles and everything.</p>
164
165 <p>A third reason is that it's just a little... askew. Note that if we had a <code>WHILE</code> instruction,
166 we wouldn't need a <code>BOTTOM</code> instruction
167 because we could just do something like <code>WHILE FALSE SKIP</code>. But we don't have <code>WHILE</code>.
168 Yet it is still possible for a Cabra program to hang.
169 This is, in my opinion, pretty weird: here's this very weak language, yet it's still capable of somewhat unpleasant things
170 which are usually only associated with powerful models of computation like Turing-machines...</p>
171
172 <p>And lastly I did it to irk people who think that the goal of esolang design is to make a language that
173 is Turing-complete. Give me an interesting weak language over a boring Turing-complete language anyday.</p>
174
175 <h2>Dioid Theory</h2>
176
177 <p>Now, recall &mdash; or go look up in an abstract algebra textbook &mdash; or just take my word for it &mdash; that
178 an idempotent semiring is a triple &lang;<var>S</var>, +, *&rang; where:</p>
179
180 <ul>
181 <li><var>S</var> is a set of elements;</li>
182 <li> + : <var>S</var> &times; <var>S</var> &rarr; <var>S</var> is a binary operation on <var>S</var>; and</li>
183 <li> * : <var>S</var> &times; <var>S</var> &rarr; <var>S</var> is another binary operation on <var>S</var>,</li>
184 </ul>
185 <p>where the following axioms of dioid theory (over an equivalence relation!) hold:</p>
186
187 <ul>
188 <li> (<var>a</var> + <var>b</var>) + <var>c</var> &equiv; <var>a</var> + (<var>b</var> + <var>c</var>) (addition is associative)</li>
189 <li> <var>a</var> + <var>b</var> &equiv; <var>b</var> + <var>a</var> (addition is commutative)</li>
190 <li> <var>a</var> + 0 &equiv; 0 + <var>a</var> &equiv; <var>a</var> (existence of additive identity)</li>
191 <li> <var>a</var> + <var>a</var> &equiv; <var>a</var> (addition is idempotent)</li>
192 <li> (<var>a</var> * <var>b</var>) * <var>c</var> &equiv; <var>a</var> * (<var>b</var> * <var>c</var>) (multiplication is associative)</li>
193 <li><var>a</var> * 1 &equiv; 1 * <var>a</var> &equiv; <var>a</var> (existence of multiplicative identity)</li>
194 <li><var>a</var> * (<var>b</var> + <var>c</var>) &equiv; (<var>a</var> * <var>b</var>) + (<var>a</var> * <var>c</var>) (multiplication left-distributes over addition)</li>
195 <li>(<var>a</var> + <var>b</var>) * <var>c</var> &equiv; (<var>a</var> * <var>c</var>) + (<var>b</var> * <var>c</var>) (multiplication right-distributes over addition)</li>
196 <li><var>a</var> * 0 &equiv; 0 * <var>a</var> &equiv; 0 (additive identity is multiplicative annihiliator)</li>
197 </ul>
198
199 <p>Now I'll attempt to show that Cabra programs form an idempotent semiring, over the equivalence relation of "semantically identical", under the
200 Cabra operations <code>+</code>,
201 considered additive, and <code>*</code>, considered multiplicative. For each axiom, I'll argue informally that it holds for all Cabra programs, hoping that an appeal to your intuition will be sufficient to
202 convince you. A formal proof is also possible I'm sure, but it would be tedious, and probably not really illuminating.</p>
203
204 <p>Parallel composition is associative. The result of
205 <code>(<var>a</var>+<var>b</var>)+<var>c</var></code>
206 never differs from the result of
207 <code><var>a</var>+(<var>b</var>+<var>c</var>)</code>,
208 because all of <var>a</var>, <var>b</var>, and <var>c</var>
209 are working on the same input set, and whichever one finishes first, finishes first;
210 this is completely independent of the order in which they are considered to have been organized into a parallel arrangement.</p>
211
212 <p>Parallel composition is commutative. When running programs in parallel, one would naturally expect that the order of the programs
213 doesn't matter &mdash; in fact, the concept doesn't really make sense. In <code><var>a</var>+<var>b</var></code>, <var>a</var> and <var>b</var> aren't
214 really running in any order; they're running at the same time. The result of <code><var>a</var>+<var>b</var></code>
215 is determined by which of <var>a</var> or <var>b</var> terminates first, and this is not affected by which order they appear on either
216 side of the <code>+</code> operator. (In fact, that was why I introduced the "lexical order" tie-breaker,
217 lest a dependency on this were accidentally introduced.)</p>
218
219 <p>There is a neutral element for parallel composition. Indeed, <code>BOTTOM</code> is this neutral element.
220 Any program <var>a</var> that terminates will by definition terminate before <code>BOTTOM</code>,
221 therefore <code><var>a</var>+BOTTOM</code> &equiv; <code>BOTTOM+<var>a</var></code> &equiv; <code><var>a</var></code>.</p>
222
223 <p>Parallel composition is idempotent. Intuitively, executing two copies of the same program in parallel will have the same result as
224 executing only one copy would. Since they both have the same input set and they both
225 compute the same thing, it doesn't matter which one terminates first (and in our definition, this is undefined.)</p>
226
227 <p>Sequential composition is associative. The result of <code><var>a</var>*<var>b</var>*<var>c</var></code>
228 does not differ if one first composes <var>a</var> and <var>b</var> to obtain a new program, say <var>d</var>, then composes <var>d</var> and <var>c</var>,
229 or if one first composes <var>b</var> and <var>c</var> to get <var>e</var>, then composes <var>a</var> and <var>e</var>.
230 An analogy can be drawn in a "block-structured" language
231 like Pascal: the program <code>BEGIN A; B END; C</code> is semantically identical to <code>A; BEGIN B; C END</code>.
232
233 (Note that we are talking about <em>composition</em> here, not execution. When we put together programs to form a new program,
234 it doesn't matter what order we put them together in, we get the same new program. If we were to <em>execute</em> those component programs
235 in a different order, that would be a different story: execution is indeed non-associative.)</p>
236
237 <p>There is a neutral element for sequential composition. Indeed, <code>SKIP</code> is this neutral element.
238 Say some program <var>a</var> takes input set <var>S</var> and generates output set <var>T</var>.
239 Then the programs <code><var>a</var>*SKIP</code> and <code>SKIP*<var>a</var></code> will also, fairly obviously, produce <var>T</var> when given <var>S</var>.</p>
240
241 <p>Sequential composition left-distributes over parallel composition. This is similar to the argument that parallel composition is
242 idempotent. If you have a program <var>a</var>
243 that runs before two programs in parallel <code><var>b</var>+<var>c</var></code>, it doesn't matter if one copy of <var>a</var> runs
244 sequentially before both <var>b</var> and <var>c</var>, or if two copies of <var>a</var> run in parallel, one sequentially before <var>b</var> and one sequentially before <var>c</var>.
245 In both cases it's as if one copy of <var>a</var> ran, and in both cases both <var>b</var> and <var>c</var> get the same input set.</p>
246
247 <p>Sequential composition right-distributes over parallel composition. Consider <code><var>a</var>+<var>b</var></code>. On some input <var>S</var>,
248 <var>a</var> will take <var>x</var> cycles and
249 <var>b</var> will take <var>y</var> cycles, and the output set <var>T</var> will from be whichever of these numbers of cycles is smaller.
250 So if there was a subsequent program <var>c</var>, it would take <var>T</var> as its input set, and it itself would take <var>z</var> cycles.
251 Now suppose we sequentially compose <var>c</var> onto each of these subprograms:
252 <code><var>a</var>*<var>c</var></code> will take <var>x</var> + <var>z</var> cycles, and
253 <code><var>b</var>*<var>c</var></code> will take <var>y</var> + <var>z</var> cycles.
254 Because addition is monotonic &mdash; if x &gt; y then x + z &gt; y + z &mdash; whichever branch was the "winner" of <code><var>a</var>+<var>b</var></code>,
255 the same branch will be the winner of <code>(<var>a</var>*<var>c</var>)+(<var>b</var>*<var>c</var>)</code>.
256 Also, in this branch, the input set to <var>c</var> will still be <var>T</var>, the output set of the winning branch of <code><var>a</var>+<var>b</var></code>.
257 Thus the final result will be the same. (See below for much more on this.)</p>
258
259 <p>The neutral element for parallel composition is an annihilator for sequential composition. Indeed, if we
260 run <code><var>a</var>*BOTTOM</code>, or <code>BOTTOM*<var>a</var></code>, neither of those terminate, so we get the same result as running just <code>BOTTOM</code>.</p>
261
262 <h2>Notes</h2>
263
264 <h3>On Rings</h3>
265
266 <p>As I mentioned, the original intent was for Cabra programs to form a ring under sequential and parallel composition.
267 In a ring, the multiplicative operation need not have an inverse, and because of this,
268 I thought that designing Cabra, in comparison to designing Burro, would be easy.
269 Here, we don't need to devise something that "undoes" concatenation (sequential composition) of two programs, and
270 specifically, we don't have to worry if either program fails to terminate; the concatenated program simply
271 fails to terminate too. And parallel composition is "naturally" commutative, or so I thought.</p>
272
273 <p>But, it turned out not to be a cakewalk.</P
274
275 <p>For Cabra programs to form a full-fledged ring, every program would need to have a unique additive inverse.
276 That is, for every program <var>a</var>, there would need to be another program <var>b</var>,
277 where <code><var>a</var>+<var>b</var></code> &equiv; <code>BOTTOM</code>.
278 But there can be no such program, as Cabra has been defined: if <var>a</var> terminates, then there's nothing <var>b</var> can do to
279 stop <var>a</var> from terminating.</p>
280
281 <p>So Cabra programs do not form a ring. Further, it's unclear what would have to change to allow this.
282 A simple instruction <code>HANGOTHERS</code> could be defined as sort of throwing a monkey wrench into every other
283 currently executing program: <code><var>a</var>+HANGOTHERS</code> &equiv; <code>HANGOTHERS+<var>a</var></code> &equiv; <code>BOTTOM</code>.
284 But every element is supposed to have a <em>unique</em> additive inverse, and this doesn't do that, because <code>HANGOTHERS</code>
285 causes every other program to hang.</p>
286
287 <p>The only thing I can think of that even might work is to require programs participating in
288 <code><var>a</var>+<var>b</var></code> to perform some kind of synchronization.
289 Then for every program, find another program that "thwarts" that synchronization: arranges
290 things so that the other program waits forever for a lock that will never be released, or a
291 message that will never come.</p>
292
293 <h3>Semantics of <code>+</code></h3>
294
295 <p>The semantics Cabra ended up having for parallel composition are not those which I originally envisioned.
296 I was certainly hoping for something more interesting than a deterministic race condition. However, if one chooses
297 parallel semantics that are perhaps more commonplace, definate problems arise, whether in a ring or a semiring.</p>
298
299 <p>Take, for instance, a semantics where the output set of <code><var>a</var>+<var>b</var></code> is
300 the union of the output sets of <var>a</var> and <var>b</var> individually. This coincides with a fairly intuitive
301 notion of parallel processing where we fork different processes to compute different parts of a larger computation,
302 then when they are all finished, we merge their results back together.</p>
303
304 <p>But if we try this for Cabra, we have a problem:
305 while sequential composition happily left-distributes over parallel composition, it fails to right-distribute over it,
306 as the following counterexample indicates. The Cabra program</p>
307
308 <blockquote><code>(SET 1 + SET 2) * IFSET 1 THEN (IFSET 2 THEN SET 3 ELSE SKIP) ELSE SKIP</code></blockquote>
309
310 <p>evaluates to {1, 2, 3} on a null input set, because <code>(SET 1 + SET 2)</code> evaluates to {1, 2}, and
311 the remainder of the program tests for the presence of both 1 and 2 and, finding them, puts 3 in the output as well.
312 However, the Cabra program that would be gotten by right-distributing the
313 sequential composition in the above</p>
314
315 <blockquote><code>(SET 1 * IFSET 1 THEN (IFSET 2 THEN SET 3 ELSE SKIP) ELSE SKIP) +<br>
316 (SET 2 * IFSET 1 THEN (IFSET 2 THEN SET 3 ELSE SKIP) ELSE SKIP)</code></blockquote>
317
318 <p>evaluates to {1, 2}, because the tests for both 1 and 2 in each of the parallel programs fail, because each of those
319 programs only has one of the two values, not both. So 3 is never included.</p>
320
321 <p>Or, we could take a semantics where the output set of <code><var>a</var>+<var>b</var></code> is
322 the <em>intersection</em> of the output sets of <var>a</var> and <var>b</var> individually. While less
323 useful-seeming than union, perhaps, this still suggests a known parallel processing technique, namely, running the
324 same program (or different versions of the same program) on multiple processors to
325 ensure correctness of the processing equipment through redundancy.</p>
326
327 <p>But this, too, fails to be right-distributive. Consider</p>
328
329 <blockquote><code>(SET 4 + UNSET 4) * IFSET 4 THEN (UNSET 4 * SET 6) ELSE SET 5</code></blockquote>
330
331 <p>This evaluates to {5} on a null input set: 4 is not a member of the output set of the
332 parallel execution, so the test fails. But if we expand it,</p>
333
334 <blockquote><code>(SET 4 * IFSET 4 THEN (UNSET 4 * SET 6) ELSE SET 5) +<br>
335 (UNSET 4 * IFSET 4 THEN (UNSET 4 * SET 6) ELSE SET 5)</code></blockquote>
336
337 <p>we get a null output set, because the output set of the first parallel program is {6}, and the output set of the second is {5}.</p>
338
339 <p>Also, both of these approaches would, naturally, require both of the parallel programs to terminate before
340 their results could be merged to form the combined result (whether it be union or intersection.) This means that if either of them was <code>BOTTOM</code>,
341 the result would be <code>BOTTOM</code> &mdash; which in turn suggests that <code>BOTTOM</code>
342 would be an annihilator for addition as well as for multiplication, and that (at least in the union case) <code>SKIP</code>
343 also serves as a neutral element for both multiplication and addition.
344 This is less than swell, in terms of conforming to ring axioms, because one theorem of ring theory is that
345 the multiplicative identity and the additive identity are equal iff the ring consists of <em>only one element</em>,
346 which is clearly not the case here.</p>
347
348 <p>(I think, also, that if you do manage to have a "ring" where 1 &equiv; 0, but where there are clearly elements that aren't
349 either 0 or 1, it's that the additive operation and multiplicative operation are really the <em>same</em> operation
350 under the semantic equivalence relation. One of my very early designs for Cabra came up against this, and it's
351 somewhat intuitive once you think about
352 it: if two programs which <em>don't depend on each other at all</em> have some given result
353 when one is executed after the other, they'll have the <em>same</em> result when
354 they are executed concurrently &mdash; because they don't depend on each other at all! Thus
355 in this case <code>+</code> = <code>*</code>
356 and we're really talking about something that's a monoid or group or something, <em>not</em> a ring.)</p>
357
358 <p>Based on this, I will go so far as to conjecture that, in fact, <em>any</em> semantics for parallel composition
359 <code><var>a</var>+<var>b</var></code> (in an otherwise Cabra-like language)
360 that combines results from both <var>a</var> and <var>b</var> will not be right-distributive.
361 The only reason Cabra manages to be right-distributive is because it has a semantics which does not
362 combine the results, but picks one and discards the other.</p>
363
364 <h3>Other Algebras</h3>
365
366 <p>There are ways to address the problems of Cabra &mdash; or otherwise try to make it more interesting &mdash;
367 by formulating other algebras using other sets of axioms.</p>
368
369 <p>Take, for example, Kleene algebras.
370 A Kleene algebra is a dioid with an additional unary postfix operator *: <var>S</var> &rarr; <var>S</var>.
371 It denotes a kind of additive closure: for any element <var>a</var>,
372 <var>a</var>* &equiv; 0 + <var>a</var> + (<var>a</var> * <var>a</var>) + (<var>a</var> * <var>a</var> * <var>a</var>)
373 + (<var>a</var> * <var>a</var> * <var>a</var> * <var>a</var>) + ... Kleene algebras are used for such things
374 as the theory of regular expressions, where the Kleene star indicates "zero or more occurrences."</p>
375
376 <p>If we try to extend Cabra from a dioid to a Kleene algebra by adding a Kleene star, we appear to get a nonplussing
377 result. Since <code><var>a</var></code> always takes fewer cycles than <code><var>a</var>*<var>a</var></code>
378 (except when <var>a</var> is <code>SKIP</code>, and in that case <code><var>a</var>*<var>a</var></code> &equiv; <code><var>a</var></code>,)
379 and since any <var>a</var> takes fewer cycles than <code>BOTTOM</code>, it appears that
380 <code><var>a</var>*</code> &equiv; <code><var>a</var></code> in Cabra.</p>
381
382 <p>What does that get us? I'm not sure. I suspect nothing, unless there is some neat property of the
383 ordering induced by the Kleene algebra that shows up. But it doesn't seem worth checking, to me.</p>
384
385 <p>A perhaps more obvious "surgery" to make is to drop the requirement that semirings be right-distributive (while keeping left-distributivity.) This lets us have
386 "intuitive" semantics for parallel composition. I suppose then you get a kind of biased semiring. But I don't know what
387 can be said about biased semirings. I've not seen them mentioned elsewhere in the literature, and I suspect they are not very interesting
388 if there aren't many other examples of them, and if there are no non-trivial theorems about them.</p>
389
390 <p>Also, if it were not for <code>BOTTOM</code>, every program would have a multiplicative inverse: simply find which elements
391 of the set the program changes, and undo those changes: do a <code>SET</code> everywhere it did an <code>UNSET</code>,
392 and vice-versa. Then, I suppose, you get an idempotent semiring with multiplicative inverses, for whatever that's worth; again,
393 I've not seen these and I don't know what can be said about them.</p>
394
395 <h2>Implementation</h2>
396
397 <p>There is an implementation of Cabra in Haskell, <code>cabra.hs</code>, but it's really more of a token offering than a reference implementation.
398 There isn't even any parser: Cabra programs have to be given as Haskell terms, which syntactically only vaguely resemble
399 Cabra programs.</p>
400
401 <h2>History</h2>
402
403 <p>I came up with the idea to make a language whose programs formed a ring shortly after getting Burro basically done &mdash;
404 fall or winter of 2005. I didn't develop the idea until around the spring of 2007, when it occurred to me that parallel and sequential execution
405 could work for the operators. Developing the language itself (and compromising on a dioid) occurred in late summer and fall of 2007.</p>
406
407 <p>May the goat be with you!</p>
408
409 <p>-Chris Pressey
410 <br>November 1, 2007
411 <br>Windsor, Ontario, Canada</p>
412
413 </body>
414 </html>
+147
-0
src/cabra.hs less more
0 --
1 -- cabra.hs
2 -- Interpreter for the Cabra Programming Language
3 -- Chris Pressey, Cat's Eye Technologies
4 --
5 -- $Id$
6 --
7
8 --
9 -- Copyright (c)2007 Cat's Eye Technologies. All rights reserved.
10 --
11 -- Redistribution and use in source and binary forms, with or without
12 -- modification, are permitted provided that the following conditions
13 -- are met:
14 --
15 -- 1. Redistributions of source code must retain the above copyright
16 -- notices, this list of conditions and the following disclaimer.
17 -- 2. Redistributions in binary form must reproduce the above copyright
18 -- notices, this list of conditions, and the following disclaimer in
19 -- the documentation and/or other materials provided with the
20 -- distribution.
21 -- 3. Neither the names of the copyright holders nor the names of their
22 -- contributors may be used to endorse or promote products derived
23 -- from this software without specific prior written permission.
24 --
25 -- THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
26 -- ``AS IS'' AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
27 -- LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
28 -- FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
29 -- COPYRIGHT HOLDERS OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
30 -- INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
31 -- BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
32 -- LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
33 -- CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
34 -- LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
35 -- ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
36 -- POSSIBILITY OF SUCH DAMAGE.
37 --
38
39
40 -----------------------------------------------------------------------
41 -- ========================== Data types =========================== --
42 -----------------------------------------------------------------------
43
44 import qualified Data.Set as Set
45
46 data Cabra = Skip
47 | UnSet Integer
48 | Set Integer
49 | Bottom
50 | IfSet Integer Cabra Cabra
51 | Par Cabra Cabra
52 | Seq Cabra Cabra
53 deriving (Show, Ord, Eq)
54
55
56 -----------------------------------------------------------------------
57 -- =========================== Execution =========================== --
58 -----------------------------------------------------------------------
59
60 interpret :: Cabra -> (Set.Set Integer) -> ((Set.Set Integer), Integer)
61
62 interpret (Set x) input =
63 let
64 cycles = if (Set.member x input) then 1 else x
65 in
66 (Set.union input (Set.singleton x), cycles)
67
68 interpret (UnSet x) input = (Set.difference input (Set.singleton x), 1)
69
70 interpret (IfSet x a b) input =
71 if (Set.member x input) then
72 interpret a input
73 else
74 interpret b input
75
76 interpret (Seq a b) input =
77 let
78 (output_a, cycles_a) = interpret a input
79 (output_b, cycles_b) = interpret b output_a
80 in
81 (output_b, cycles_a + cycles_b)
82
83 interpret (Par a b) input =
84 let
85 (output_a, cycles_a) = interpret a input
86 (output_b, cycles_b) = interpret b input
87 in
88 if (cycles_a < cycles_b) then
89 (output_a, cycles_a)
90 else
91 if (cycles_b < cycles_a) then
92 (output_b, cycles_b)
93 else
94 if (a < b) then -- lexicographic tiebreaker
95 (output_a, cycles_a)
96 else
97 (output_b, cycles_b)
98
99 interpret Skip input = (input, 0)
100
101 interpret Bottom input = interpret Bottom input
102
103 run prog input =
104 let
105 (output, cycles) = interpret prog (Set.fromList input)
106 in
107 Set.elems output
108
109
110 -----------------------------------------------------------------------
111 -- =========================== Test Cases ========================== --
112 -----------------------------------------------------------------------
113
114 test 1 =
115 Seq (Set 5) (Set 23)
116
117 test 2 =
118 IfSet 5 (Seq (UnSet 5) (Set 6)) Skip
119
120 test 3 =
121 Par (IfSet 100 (Set 300) Skip)
122 (Seq (UnSet 100) (Set 10))
123
124 --
125 -- Tests for right-distributivity.
126 --
127
128 test 4 =
129 Seq
130 (Par (Set 1) (Set 2))
131 (IfSet 1 (IfSet 2 (Set 3) Skip) Skip)
132
133 test 5 =
134 Par
135 (Seq (Set 1) (IfSet 1 (IfSet 2 (Set 3) Skip) Skip))
136 (Seq (Set 2) (IfSet 1 (IfSet 2 (Set 3) Skip) Skip))
137
138 test 6 =
139 Seq
140 (Par (Set 4) (UnSet 4))
141 (IfSet 4 (Seq (UnSet 4) (Set 6)) (Set 5))
142
143 test 7 =
144 Par
145 (Seq (Set 4) (IfSet 4 (Seq (UnSet 4) (Set 6)) (Set 5)))
146 (Seq (UnSet 4) (IfSet 4 (Seq (UnSet 4) (Set 6)) (Set 5)))