git @ Cat's Eye Technologies Cabra / 738155c
Import of Cabra version 1.0 revision 2011.1214 (just HTML fixes.) Cat's Eye Technologies 11 years ago
1 changed file(s) with 35 addition(s) and 30 deletion(s). Raw diff Collapse all Expand all
+35
-30
doc/cabra.html less more
00 <!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
1 <!-- encoding: UTF-8 -->
12 <html xmlns="http://www.w3.org/1999/xhtml" lang="en">
23 <head>
34 <meta http-equiv="Content-Type" content="text/html; charset=UTF-8" />
45 <title>The Cabra Programming Language</title>
6 <!-- begin html doc dynamic markup -->
7 <script type="text/javascript" src="/contrib/jquery-1.6.4.min.js"></script>
8 <script type="text/javascript" src="/scripts/documentation.js"></script>
9 <!-- end html doc dynamic markup -->
510 </head>
611 <body>
712
2732 relation</em> is introduced there in order to make sense of how program texts (syntax) can be manipulated in
2833 tandem with the programs (semantics) they represent. In short, many different program texts are equivalent to
2934 the same (abstract) program, so the equality operator = used in the group axioms is simply replaced
30 by the equivalence operator, &equiv;. Obviously, this technique isn't restricted to groups, and the idea can be
35 by the equivalence operator, ≡. Obviously, this technique isn't restricted to groups, and the idea can be
3136 extended to that of any <em>algebra over an equivalence relation</em>, and it is this notion that
3237 is applied in Cabra to dioids.</p>
3338
161166 problems any easier.</p>
162167
163168 <p>Another reason is that Cabra, despite almost being, say, just a kind of algebraical structure, <em>looks</em> a lot
164 like the beginnings of a programming language. It's got a conditional form, and imperative update. It almost looks like an overspecified language &mdash;
165 heck, a <em>machine</em> &mdash; because of the definition of how parallel composition works in terms of cycles and everything.</p>
169 like the beginnings of a programming language. It's got a conditional form, and imperative update. It almost looks like an overspecified language —
170 heck, a <em>machine</em> — because of the definition of how parallel composition works in terms of cycles and everything.</p>
166171
167172 <p>A third reason is that it's just a little... askew. Note that if we had a <code>WHILE</code> instruction,
168173 we wouldn't need a <code>BOTTOM</code> instruction
176181
177182 <h2>Dioid Theory</h2>
178183
179 <p>Now, recall &mdash; or go look up in an abstract algebra textbook &mdash; or just take my word for it &mdash; that
180 an idempotent semiring is a triple &lang;<var>S</var>, +, *&rang; where:</p>
184 <p>Now, recall — or go look up in an abstract algebra textbook — or just take my word for it — that
185 an idempotent semiring is a triple 〈<var>S</var>, +, *〉 where:</p>
181186
182187 <ul>
183188 <li><var>S</var> is a set of elements;</li>
184 <li> + : <var>S</var> &times; <var>S</var> &rarr; <var>S</var> is a binary operation on <var>S</var>; and</li>
185 <li> * : <var>S</var> &times; <var>S</var> &rarr; <var>S</var> is another binary operation on <var>S</var>,</li>
189 <li>+ : <var>S</var> × <var>S</var> → <var>S</var> is a binary operation on <var>S</var>; and</li>
190 <li>* : <var>S</var> × <var>S</var> → <var>S</var> is another binary operation on <var>S</var>,</li>
186191 </ul>
187192 <p>where the following axioms of dioid theory (over an equivalence relation!) hold:</p>
188193
189194 <ul>
190 <li> (<var>a</var> + <var>b</var>) + <var>c</var> &equiv; <var>a</var> + (<var>b</var> + <var>c</var>) (addition is associative)</li>
191 <li> <var>a</var> + <var>b</var> &equiv; <var>b</var> + <var>a</var> (addition is commutative)</li>
192 <li> <var>a</var> + 0 &equiv; 0 + <var>a</var> &equiv; <var>a</var> (existence of additive identity)</li>
193 <li> <var>a</var> + <var>a</var> &equiv; <var>a</var> (addition is idempotent)</li>
194 <li> (<var>a</var> * <var>b</var>) * <var>c</var> &equiv; <var>a</var> * (<var>b</var> * <var>c</var>) (multiplication is associative)</li>
195 <li><var>a</var> * 1 &equiv; 1 * <var>a</var> &equiv; <var>a</var> (existence of multiplicative identity)</li>
196 <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>
197 <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>
198 <li><var>a</var> * 0 &equiv; 0 * <var>a</var> &equiv; 0 (additive identity is multiplicative annihiliator)</li>
195 <li> (<var>a</var> + <var>b</var>) + <var>c</var> ≡ <var>a</var> + (<var>b</var> + <var>c</var>) (addition is associative)</li>
196 <li> <var>a</var> + <var>b</var> ≡ <var>b</var> + <var>a</var> (addition is commutative)</li>
197 <li> <var>a</var> + 0 ≡ 0 + <var>a</var> ≡ <var>a</var> (existence of additive identity)</li>
198 <li> <var>a</var> + <var>a</var> ≡ <var>a</var> (addition is idempotent)</li>
199 <li> (<var>a</var> * <var>b</var>) * <var>c</var> ≡ <var>a</var> * (<var>b</var> * <var>c</var>) (multiplication is associative)</li>
200 <li><var>a</var> * 1 ≡ 1 * <var>a</var> ≡ <var>a</var> (existence of multiplicative identity)</li>
201 <li><var>a</var> * (<var>b</var> + <var>c</var>) ≡ (<var>a</var> * <var>b</var>) + (<var>a</var> * <var>c</var>) (multiplication left-distributes over addition)</li>
202 <li>(<var>a</var> + <var>b</var>) * <var>c</var> ≡ (<var>a</var> * <var>c</var>) + (<var>b</var> * <var>c</var>) (multiplication right-distributes over addition)</li>
203 <li><var>a</var> * 0 ≡ 0 * <var>a</var> ≡ 0 (additive identity is multiplicative annihiliator)</li>
199204 </ul>
200205
201206 <p>Now I'll attempt to show that Cabra programs form an idempotent semiring, over the equivalence relation of "semantically identical", under the
212217 this is completely independent of the order in which they are considered to have been organized into a parallel arrangement.</p>
213218
214219 <p>Parallel composition is commutative. When running programs in parallel, one would naturally expect that the order of the programs
215 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
220 doesn't matter — 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
216221 really running in any order; they're running at the same time. The result of <code><var>a</var>+<var>b</var></code>
217222 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
218223 side of the <code>+</code> operator. (In fact, that was why I introduced the "lexical order" tie-breaker,
220225
221226 <p>There is a neutral element for parallel composition. Indeed, <code>BOTTOM</code> is this neutral element.
222227 Any program <var>a</var> that terminates will by definition terminate before <code>BOTTOM</code>,
223 therefore <code><var>a</var>+BOTTOM</code> &equiv; <code>BOTTOM+<var>a</var></code> &equiv; <code><var>a</var></code>.</p>
228 therefore <code><var>a</var>+BOTTOM</code> ≡ <code>BOTTOM+<var>a</var></code> ≡ <code><var>a</var></code>.</p>
224229
225230 <p>Parallel composition is idempotent. Intuitively, executing two copies of the same program in parallel will have the same result as
226231 executing only one copy would. Since they both have the same input set and they both
253258 Now suppose we sequentially compose <var>c</var> onto each of these subprograms:
254259 <code><var>a</var>*<var>c</var></code> will take <var>x</var> + <var>z</var> cycles, and
255260 <code><var>b</var>*<var>c</var></code> will take <var>y</var> + <var>z</var> cycles.
256 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>,
261 Because addition is monotonic — if x &gt; y then x + z &gt; y + z — whichever branch was the "winner" of <code><var>a</var>+<var>b</var></code>,
257262 the same branch will be the winner of <code>(<var>a</var>*<var>c</var>)+(<var>b</var>*<var>c</var>)</code>.
258263 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>.
259264 Thus the final result will be the same. (See below for much more on this.)</p>
276281
277282 <p>For Cabra programs to form a full-fledged ring, every program would need to have a unique additive inverse.
278283 That is, for every program <var>a</var>, there would need to be another program <var>b</var>,
279 where <code><var>a</var>+<var>b</var></code> &equiv; <code>BOTTOM</code>.
284 where <code><var>a</var>+<var>b</var></code> ≡ <code>BOTTOM</code>.
280285 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
281286 stop <var>a</var> from terminating.</p>
282287
283288 <p>So Cabra programs do not form a ring. Further, it's unclear what would have to change to allow this.
284289 A simple instruction <code>HANGOTHERS</code> could be defined as sort of throwing a monkey wrench into every other
285 currently executing program: <code><var>a</var>+HANGOTHERS</code> &equiv; <code>HANGOTHERS+<var>a</var></code> &equiv; <code>BOTTOM</code>.
290 currently executing program: <code><var>a</var>+HANGOTHERS</code> ≡ <code>HANGOTHERS+<var>a</var></code> ≡ <code>BOTTOM</code>.
286291 But every element is supposed to have a <em>unique</em> additive inverse, and this doesn't do that, because <code>HANGOTHERS</code>
287292 causes every other program to hang.</p>
288293
340345
341346 <p>Also, both of these approaches would, naturally, require both of the parallel programs to terminate before
342347 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>,
343 the result would be <code>BOTTOM</code> &mdash; which in turn suggests that <code>BOTTOM</code>
348 the result would be <code>BOTTOM</code> — which in turn suggests that <code>BOTTOM</code>
344349 would be an annihilator for addition as well as for multiplication, and that (at least in the union case) <code>SKIP</code>
345350 also serves as a neutral element for both multiplication and addition.
346351 This is less than swell, in terms of conforming to ring axioms, because one theorem of ring theory is that
347352 the multiplicative identity and the additive identity are equal iff the ring consists of <em>only one element</em>,
348353 which is clearly not the case here.</p>
349354
350 <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
355 <p>(I think, also, that if you do manage to have a "ring" where 1 ≡ 0, but where there are clearly elements that aren't
351356 either 0 or 1, it's that the additive operation and multiplicative operation are really the <em>same</em> operation
352357 under the semantic equivalence relation. One of my very early designs for Cabra came up against this, and it's
353358 somewhat intuitive once you think about
354359 it: if two programs which <em>don't depend on each other at all</em> have some given result
355360 when one is executed after the other, they'll have the <em>same</em> result when
356 they are executed concurrently &mdash; because they don't depend on each other at all! Thus
361 they are executed concurrently — because they don't depend on each other at all! Thus
357362 in this case <code>+</code> = <code>*</code>
358363 and we're really talking about something that's a monoid or group or something, <em>not</em> a ring.)</p>
359364
365370
366371 <h3>Other Algebras</h3>
367372
368 <p>There are ways to address the problems of Cabra &mdash; or otherwise try to make it more interesting &mdash;
373 <p>There are ways to address the problems of Cabra — or otherwise try to make it more interesting —
369374 by formulating other algebras using other sets of axioms.</p>
370375
371376 <p>Take, for example, Kleene algebras.
372 A Kleene algebra is a dioid with an additional unary postfix operator *: <var>S</var> &rarr; <var>S</var>.
377 A Kleene algebra is a dioid with an additional unary postfix operator *: <var>S</var> → <var>S</var>.
373378 It denotes a kind of additive closure: for any element <var>a</var>,
374 <var>a</var>* &equiv; 0 + <var>a</var> + (<var>a</var> * <var>a</var>) + (<var>a</var> * <var>a</var> * <var>a</var>)
379 <var>a</var>* ≡ 0 + <var>a</var> + (<var>a</var> * <var>a</var>) + (<var>a</var> * <var>a</var> * <var>a</var>)
375380 + (<var>a</var> * <var>a</var> * <var>a</var> * <var>a</var>) + ... Kleene algebras are used for such things
376381 as the theory of regular expressions, where the Kleene star indicates "zero or more occurrences."</p>
377382
378383 <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
379384 result. Since <code><var>a</var></code> always takes fewer cycles than <code><var>a</var>*<var>a</var></code>
380 (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>,)
385 (except when <var>a</var> is <code>SKIP</code>, and in that case <code><var>a</var>*<var>a</var></code> ≡ <code><var>a</var></code>,)
381386 and since any <var>a</var> takes fewer cycles than <code>BOTTOM</code>, it appears that
382 <code><var>a</var>*</code> &equiv; <code><var>a</var></code> in Cabra.</p>
387 <code><var>a</var>*</code> ≡ <code><var>a</var></code> in Cabra.</p>
383388
384389 <p>What does that get us? I'm not sure. I suspect nothing, unless there is some neat property of the
385390 ordering induced by the Kleene algebra that shows up. But it doesn't seem worth checking, to me.</p>
402407
403408 <h2>History</h2>
404409
405 <p>I came up with the idea to make a language whose programs formed a ring shortly after getting Burro basically done &mdash;
410 <p>I came up with the idea to make a language whose programs formed a ring shortly after getting Burro basically done —
406411 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
407412 could work for the operators. Developing the language itself (and compromising on a dioid) occurred in late summer and fall of 2007.</p>
408413