<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<!-- encoding: UTF-8 -->
<html xmlns="http://www.w3.org/1999/xhtml" lang="en">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8" />
<title>The Cabra Programming Language</title>
</head>
<body>
<h1>Cabra</h1>
<p>November 2007, Chris Pressey, Cat's Eye Technologies</p>
<h2>Introduction</h2>
<p>Cabra is a formal programming language whose programs form a dioid (an idempotent semiring)
over its semantic equivalence relation under the operations of parallel composition (additive)
and sequential composition (multiplicative.) (Say <em>that</em> five times fast!)</p>
<p>Cabra is the successor to <a href="/projects/burro/">Burro</a>, a programming language
whose programs form a simpler algebraic structure: a group.
Unlike Burro, however, Cabra is not derived from Brainfuck in any way.
And, while the word "burro" is Spanish for "donkey", the word "cabra" is Spanish for "goat."
(Also, in reality, you'd be hard-pressed to do any actual
<em>programming</em> in Cabra... but it <em>is</em> a formal language.)</p>
<p>Reading the Burro documentation is definately recommended for getting the most out of Cabra,
as several of the same issues are dealt with there. Notably, the notion of a <em>group over an equivalence
relation</em> is introduced there in order to make sense of how program texts (syntax) can be manipulated in
tandem with the programs (semantics) they represent. In short, many different program texts are equivalent to
the same (abstract) program, so the equality operator = used in the group axioms is simply replaced
by the equivalence operator, ≡. Obviously, this technique isn't restricted to groups, and the idea can be
extended to that of any <em>algebra over an equivalence relation</em>, and it is this notion that
is applied in Cabra to dioids.</p>
<p>The original intent of Cabra was to devise a language whose programs formed a <em>ring</em>
under parallel and sequential composition operations. Selecting a semantics for parallel composition that
fulfill all the ring axioms presents a number of problems, which are discussed below.
As a compromise, the axioms for <em>idempotent semirings</em> were chosen instead.
Idempotent semirings, sometimes called <em>dioids</em>, lack the additive inverses that rings have,
but unlike rings, have an idempotent additive operator.</p>
<p>Let's get straight to it.</p>
<h2>Language Definition</h2>
<p>Every Cabra program takes, as input, an <em>input set</em>, which is a set of non-negative integers.
Every Cabra program either produces an <em>output set</em>, which is also a set of non-negative integers,
or it fails to terminate.</p>
<p>A Cabra program is defined inductively as follows.</p>
<p>The instruction <code>SET <var>n</var></code>, where <var>n</var> is any non-negative integer,
is a Cabra program. The output set of this program is the union of
the input set and the singleton set {<var>n</var>}. (The output set is just like the input set
except that it also includes <var>n</var> if it was missing from the input set.)</p>
<p>The instruction <code>UNSET <var>n</var></code>, where <var>n</var> is any non-negative integer,
is a Cabra program. The output set of this program is the set difference of the input set and
the singleton set {<var>n</var>}. (The output set is just like the input set
except that it never includes <var>n</var>, even if <var>n</var> was included in the input set.)</p>
<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>
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,
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>;
<var>b</var> is ignored. Conversely, if <var>n</var> is not a member of the input set the <code>IFSET</code>,
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>;
<var>b</var> is ignored. (<code>IFSET</code> is the conditional statement form.)</p>
<p>If <var>a</var> and <var>b</var> are Cabra programs, then <code><var>a</var>*<var>b</var></code>
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>.
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
as the output set of <code><var>a</var>*<var>b</var></code>. (This is sequential composition; <var>a</var> is
executed, then <var>b</var>. A more usual notation might be <code><var>a</var>;<var>b</var></code>.)</p>
<p>If <var>a</var> and <var>b</var> are Cabra programs, then <code><var>a</var>+<var>b</var></code>
is a Cabra program. The input set of <code><var>a</var>+<var>b</var></code> is used as the input set of
both <var>a</var> and <var>b</var>. The output set of whichever of <var>a</var> or <var>b</var>
terminates first is used as the output set of <code><var>a</var>+<var>b</var></code>. See below for the
definition of "terminates first." (This is parallel composition, with
final result determined by a kind of race condition. A more usual notation might be <var>a</var>||<var>b</var>.)</p>
<p>If <var>a</var> is a Cabra program, then <code>(<var>a</var>)</code> is a Cabra program.
This is just the usual usage of parentheses to alter precedence. Without parentheses,
<code>*</code> has a higher precedence than <code>+</code>, which has a higher
precedence than <code>IFSET</code>. For example, this means that
<code>IFSET 42 THEN SET 51 ELSE SET 5 * SET 6 + SET 7</code>
is parsed as <code>IFSET 42 THEN (SET 51) ELSE ((SET 5 * SET 6) + SET 7)</code>.</p>
<p>The instruction <code>SKIP</code> is a Cabra program. The output set of <code>SKIP</code>
always equals the input set. (<code>SKIP</code> is a no-op.)</p>
<p>The instruction <code>BOTTOM</code> is a Cabra program. Regardless of the input set,
this program always fails to terminate. (<code>BOTTOM</code> is an infinite loop.)</p>
<p>Were I a pedantic mathematician, here's where I'd mention how nothing else is a Cabra program.
As if I could be <em>so</em> sure about that.</p>
<h3>Terminates First</h3>
<p>We still need to define what it means for one Cabra program to "terminate before" another, different Cabra program.
Execution of a Cabra program is considered to take a non-negative integral number of imaginary things
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>
on some input set <var>S</var> is less
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
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>.
(If <var>a</var> and <var>b</var> have the same lexical order
then <var>a</var> = <var>b</var> and "terminate before" is meaningless because it only defined between
two different Cabra programs.)</p>
<p>The formula for calculating cycles taken in general depends on both the program and its input set, but is deterministic
in the sense that the same program on the same input set will always take the same number of cycles.
(This isn't the real world where clock speeds vary at +/-0.01% or anything like that. It is as if execution is
synchronous; as if, for example, on a single computer,
one cycle of program <var>a</var> is executed, then one cycle of <var>b</var>, and so forth, until one or the other
terminates.)</p>
<ul>
<li><code>SKIP</code> takes 0 cycles.</li>
<li><code>BOTTOM</code> takes an infinite number of cycles.</li>
<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>
<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>
<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>,
whichever was selected for execution.</li>
<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>
<li><code>UNSET <var>n</var></code> always takes 1 cycle.</li>
</ul>
<p>In fact, other formulae are possible. The somewhat unusual determination of cycles in the case of <code>SET <var>n</var></code>
is mainly to keep things interesting by ensuring that the number of cycles is dependent upon the contents of the input set.</p>
<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>,
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>
<h3>Lexical Order</h3>
<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>
<p>For primitive programs: <code>SKIP</code> comes before <code>UNSET 0</code>
which comes before <code>UNSET 1</code> which comes before <code>UNSET 2</code>, etc.
All of these come before <code>SET 0</code>, which comes before <code>SET 1</code>, etc.
And all of these come before <code>BOTTOM</code>.</p>
<p>For compound programs, the ordering is <code>IFSET <var>n</var> THEN <var>a</var> ELSE <var>b</var></code>
comes before <code>IFSET <var>n+1</var> THEN <var>a</var> ELSE <var>b</var></code>
comes before <code><var>a</var>+<var>b</var></code> comes before <code><var>a</var>*<var>b</var></code>.</p>
<p>All primitive programs come before non-primitive programs, and in general, programs with shorter length
(measured in terms of number of subterms) come before those with longer length. In programs with the same
length, subterms are compared left-to-right. (This happens to be the same kind of lexical ordering as you
get in Haskell when you declare a data type as <code>deriving (Ord)</code>.)</p>
<h3>Comments</h3>
<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>
<p>True enough. Cabra is nowhere close to being a real programming language. But I decided to design it this way anyway,
for a couple of reasons.</p>
<p>One reason is to demonstrate that these algebraical problems involving parallel composition occur even for what would be
very small subsets of a "real" programming language. You can imagine a full-fledged version of Cabra with
variables, arrays, <code>WHILE</code> loops, input/output, and the like, but you can readily see that these ameliorations don't make the central
problems any easier.</p>
<p>Another reason is that Cabra, despite almost being, say, just a kind of algebraical structure, <em>looks</em> a lot
like the beginnings of a programming language. It's got a conditional form, and imperative update. It almost looks like an overspecified language —
heck, a <em>machine</em> — because of the definition of how parallel composition works in terms of cycles and everything.</p>
<p>A third reason is that it's just a little... askew. Note that if we had a <code>WHILE</code> instruction,
we wouldn't need a <code>BOTTOM</code> instruction
because we could just do something like <code>WHILE FALSE SKIP</code>. But we don't have <code>WHILE</code>.
Yet it is still possible for a Cabra program to hang.
This is, in my opinion, pretty weird: here's this very weak language, yet it's still capable of somewhat unpleasant things
which are usually only associated with powerful models of computation like Turing-machines...</p>
<p>And lastly I did it to irk people who think that the goal of esolang design is to make a language that
is Turing-complete. Give me an interesting weak language over a boring Turing-complete language anyday.</p>
<h2>Dioid Theory</h2>
<p>Now, recall — or go look up in an abstract algebra textbook — or just take my word for it — that
an idempotent semiring is a triple 〈<var>S</var>, +, *〉 where:</p>
<ul>
<li><var>S</var> is a set of elements;</li>
<li>+ : <var>S</var> × <var>S</var> → <var>S</var> is a binary operation on <var>S</var>; and</li>
<li>* : <var>S</var> × <var>S</var> → <var>S</var> is another binary operation on <var>S</var>,</li>
</ul>
<p>where the following axioms of dioid theory (over an equivalence relation!) hold:</p>
<ul>
<li> (<var>a</var> + <var>b</var>) + <var>c</var> ≡ <var>a</var> + (<var>b</var> + <var>c</var>) (addition is associative)</li>
<li> <var>a</var> + <var>b</var> ≡ <var>b</var> + <var>a</var> (addition is commutative)</li>
<li> <var>a</var> + 0 ≡ 0 + <var>a</var> ≡ <var>a</var> (existence of additive identity)</li>
<li> <var>a</var> + <var>a</var> ≡ <var>a</var> (addition is idempotent)</li>
<li> (<var>a</var> * <var>b</var>) * <var>c</var> ≡ <var>a</var> * (<var>b</var> * <var>c</var>) (multiplication is associative)</li>
<li><var>a</var> * 1 ≡ 1 * <var>a</var> ≡ <var>a</var> (existence of multiplicative identity)</li>
<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>
<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>
<li><var>a</var> * 0 ≡ 0 * <var>a</var> ≡ 0 (additive identity is multiplicative annihiliator)</li>
</ul>
<p>Now I'll attempt to show that Cabra programs form an idempotent semiring, over the equivalence relation of "semantically identical", under the
Cabra operations <code>+</code>,
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
convince you. A formal proof is also possible I'm sure, but it would be tedious, and probably not really illuminating.</p>
<p>Parallel composition is associative. The result of
<code>(<var>a</var>+<var>b</var>)+<var>c</var></code>
never differs from the result of
<code><var>a</var>+(<var>b</var>+<var>c</var>)</code>,
because all of <var>a</var>, <var>b</var>, and <var>c</var>
are working on the same input set, and whichever one finishes first, finishes first;
this is completely independent of the order in which they are considered to have been organized into a parallel arrangement.</p>
<p>Parallel composition is commutative. When running programs in parallel, one would naturally expect that the order of the programs
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
really running in any order; they're running at the same time. The result of <code><var>a</var>+<var>b</var></code>
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
side of the <code>+</code> operator. (In fact, that was why I introduced the "lexical order" tie-breaker,
lest a dependency on this were accidentally introduced.)</p>
<p>There is a neutral element for parallel composition. Indeed, <code>BOTTOM</code> is this neutral element.
Any program <var>a</var> that terminates will by definition terminate before <code>BOTTOM</code>,
therefore <code><var>a</var>+BOTTOM</code> ≡ <code>BOTTOM+<var>a</var></code> ≡ <code><var>a</var></code>.</p>
<p>Parallel composition is idempotent. Intuitively, executing two copies of the same program in parallel will have the same result as
executing only one copy would. Since they both have the same input set and they both
compute the same thing, it doesn't matter which one terminates first (and in our definition, this is undefined.)</p>
<p>Sequential composition is associative. The result of <code><var>a</var>*<var>b</var>*<var>c</var></code>
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>,
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>.
An analogy can be drawn in a "block-structured" language
like Pascal: the program <code>BEGIN A; B END; C</code> is semantically identical to <code>A; BEGIN B; C END</code>.
(Note that we are talking about <em>composition</em> here, not execution. When we put together programs to form a new program,
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
in a different order, that would be a different story: execution is indeed non-associative.)</p>
<p>There is a neutral element for sequential composition. Indeed, <code>SKIP</code> is this neutral element.
Say some program <var>a</var> takes input set <var>S</var> and generates output set <var>T</var>.
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>
<p>Sequential composition left-distributes over parallel composition. This is similar to the argument that parallel composition is
idempotent. If you have a program <var>a</var>
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
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>.
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>
<p>Sequential composition right-distributes over parallel composition. Consider <code><var>a</var>+<var>b</var></code>. On some input <var>S</var>,
<var>a</var> will take <var>x</var> cycles and
<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.
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.
Now suppose we sequentially compose <var>c</var> onto each of these subprograms:
<code><var>a</var>*<var>c</var></code> will take <var>x</var> + <var>z</var> cycles, and
<code><var>b</var>*<var>c</var></code> will take <var>y</var> + <var>z</var> cycles.
Because addition is monotonic — if x > y then x + z > y + z — whichever branch was the "winner" of <code><var>a</var>+<var>b</var></code>,
the same branch will be the winner of <code>(<var>a</var>*<var>c</var>)+(<var>b</var>*<var>c</var>)</code>.
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>.
Thus the final result will be the same. (See below for much more on this.)</p>
<p>The neutral element for parallel composition is an annihilator for sequential composition. Indeed, if we
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>
<h2>Notes</h2>
<h3>On Rings</h3>
<p>As I mentioned, the original intent was for Cabra programs to form a ring under sequential and parallel composition.
In a ring, the multiplicative operation need not have an inverse, and because of this,
I thought that designing Cabra, in comparison to designing Burro, would be easy.
Here, we don't need to devise something that "undoes" concatenation (sequential composition) of two programs, and
specifically, we don't have to worry if either program fails to terminate; the concatenated program simply
fails to terminate too. And parallel composition is "naturally" commutative, or so I thought.</p>
<p>But, it turned out not to be a cakewalk.</p>
<p>For Cabra programs to form a full-fledged ring, every program would need to have a unique additive inverse.
That is, for every program <var>a</var>, there would need to be another program <var>b</var>,
where <code><var>a</var>+<var>b</var></code> ≡ <code>BOTTOM</code>.
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
stop <var>a</var> from terminating.</p>
<p>So Cabra programs do not form a ring. Further, it's unclear what would have to change to allow this.
A simple instruction <code>HANGOTHERS</code> could be defined as sort of throwing a monkey wrench into every other
currently executing program: <code><var>a</var>+HANGOTHERS</code> ≡ <code>HANGOTHERS+<var>a</var></code> ≡ <code>BOTTOM</code>.
But every element is supposed to have a <em>unique</em> additive inverse, and this doesn't do that, because <code>HANGOTHERS</code>
causes every other program to hang.</p>
<p>The only thing I can think of that even might work is to require programs participating in
<code><var>a</var>+<var>b</var></code> to perform some kind of synchronization.
Then for every program, find another program that "thwarts" that synchronization: arranges
things so that the other program waits forever for a lock that will never be released, or a
message that will never come.</p>
<h3>Semantics of <code>+</code></h3>
<p>The semantics Cabra ended up having for parallel composition are not those which I originally envisioned.
I was certainly hoping for something more interesting than a deterministic race condition. However, if one chooses
parallel semantics that are perhaps more commonplace, definate problems arise, whether in a ring or a semiring.</p>
<p>Take, for instance, a semantics where the output set of <code><var>a</var>+<var>b</var></code> is
the union of the output sets of <var>a</var> and <var>b</var> individually. This coincides with a fairly intuitive
notion of parallel processing where we fork different processes to compute different parts of a larger computation,
then when they are all finished, we merge their results back together.</p>
<p>But if we try this for Cabra, we have a problem:
while sequential composition happily left-distributes over parallel composition, it fails to right-distribute over it,
as the following counterexample indicates. The Cabra program</p>
<blockquote><p><code>(SET 1 + SET 2) * IFSET 1 THEN (IFSET 2 THEN SET 3 ELSE SKIP) ELSE SKIP</code></p></blockquote>
<p>evaluates to {1, 2, 3} on a null input set, because <code>(SET 1 + SET 2)</code> evaluates to {1, 2}, and
the remainder of the program tests for the presence of both 1 and 2 and, finding them, puts 3 in the output as well.
However, the Cabra program that would be gotten by right-distributing the
sequential composition in the above</p>
<blockquote><p><code>(SET 1 * IFSET 1 THEN (IFSET 2 THEN SET 3 ELSE SKIP) ELSE SKIP) +<br/>
(SET 2 * IFSET 1 THEN (IFSET 2 THEN SET 3 ELSE SKIP) ELSE SKIP)</code></p></blockquote>
<p>evaluates to {1, 2}, because the tests for both 1 and 2 in each of the parallel programs fail, because each of those
programs only has one of the two values, not both. So 3 is never included.</p>
<p>Or, we could take a semantics where the output set of <code><var>a</var>+<var>b</var></code> is
the <em>intersection</em> of the output sets of <var>a</var> and <var>b</var> individually. While less
useful-seeming than union, perhaps, this still suggests a known parallel processing technique, namely, running the
same program (or different versions of the same program) on multiple processors to
ensure correctness of the processing equipment through redundancy.</p>
<p>But this, too, fails to be right-distributive. Consider</p>
<blockquote><p><code>(SET 4 + UNSET 4) * IFSET 4 THEN (UNSET 4 * SET 6) ELSE SET 5</code></p></blockquote>
<p>This evaluates to {5} on a null input set: 4 is not a member of the output set of the
parallel execution, so the test fails. But if we expand it,</p>
<blockquote><p><code>(SET 4 * IFSET 4 THEN (UNSET 4 * SET 6) ELSE SET 5) +<br/>
(UNSET 4 * IFSET 4 THEN (UNSET 4 * SET 6) ELSE SET 5)</code></p></blockquote>
<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>
<p>Also, both of these approaches would, naturally, require both of the parallel programs to terminate before
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>,
the result would be <code>BOTTOM</code> — which in turn suggests that <code>BOTTOM</code>
would be an annihilator for addition as well as for multiplication, and that (at least in the union case) <code>SKIP</code>
also serves as a neutral element for both multiplication and addition.
This is less than swell, in terms of conforming to ring axioms, because one theorem of ring theory is that
the multiplicative identity and the additive identity are equal iff the ring consists of <em>only one element</em>,
which is clearly not the case here.</p>
<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
either 0 or 1, it's that the additive operation and multiplicative operation are really the <em>same</em> operation
under the semantic equivalence relation. One of my very early designs for Cabra came up against this, and it's
somewhat intuitive once you think about
it: if two programs which <em>don't depend on each other at all</em> have some given result
when one is executed after the other, they'll have the <em>same</em> result when
they are executed concurrently — because they don't depend on each other at all! Thus
in this case <code>+</code> = <code>*</code>
and we're really talking about something that's a monoid or group or something, <em>not</em> a ring.)</p>
<p>Based on this, I will go so far as to conjecture that, in fact, <em>any</em> semantics for parallel composition
<code><var>a</var>+<var>b</var></code> (in an otherwise Cabra-like language)
that combines results from both <var>a</var> and <var>b</var> will not be right-distributive.
The only reason Cabra manages to be right-distributive is because it has a semantics which does not
combine the results, but picks one and discards the other.</p>
<h3>Other Algebras</h3>
<p>There are ways to address the problems of Cabra — or otherwise try to make it more interesting —
by formulating other algebras using other sets of axioms.</p>
<p>Take, for example, Kleene algebras.
A Kleene algebra is a dioid with an additional unary postfix operator *: <var>S</var> → <var>S</var>.
It denotes a kind of additive closure: for any element <var>a</var>,
<var>a</var>* ≡ 0 + <var>a</var> + (<var>a</var> * <var>a</var>) + (<var>a</var> * <var>a</var> * <var>a</var>)
+ (<var>a</var> * <var>a</var> * <var>a</var> * <var>a</var>) + ... Kleene algebras are used for such things
as the theory of regular expressions, where the Kleene star indicates "zero or more occurrences."</p>
<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
result. Since <code><var>a</var></code> always takes fewer cycles than <code><var>a</var>*<var>a</var></code>
(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>,)
and since any <var>a</var> takes fewer cycles than <code>BOTTOM</code>, it appears that
<code><var>a</var>*</code> ≡ <code><var>a</var></code> in Cabra.</p>
<p>What does that get us? I'm not sure. I suspect nothing, unless there is some neat property of the
ordering induced by the Kleene algebra that shows up. But it doesn't seem worth checking, to me.</p>
<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
"intuitive" semantics for parallel composition. I suppose then you get a kind of biased semiring. But I don't know what
can be said about biased semirings. I've not seen them mentioned elsewhere in the literature, and I suspect they are not very interesting
if there aren't many other examples of them, and if there are no non-trivial theorems about them.</p>
<p>Also, if it were not for <code>BOTTOM</code>, every program would have a multiplicative inverse: simply find which elements
of the set the program changes, and undo those changes: do a <code>SET</code> everywhere it did an <code>UNSET</code>,
and vice-versa. Then, I suppose, you get an idempotent semiring with multiplicative inverses, for whatever that's worth; again,
I've not seen these and I don't know what can be said about them.</p>
<h2>Implementation</h2>
<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.
There isn't even any parser: Cabra programs have to be given as Haskell terms, which syntactically only vaguely resemble
Cabra programs.</p>
<h2>History</h2>
<p>I came up with the idea to make a language whose programs formed a ring shortly after getting Burro basically done —
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
could work for the operators. Developing the language itself (and compromising on a dioid) occurred in late summer and fall of 2007.</p>
<p>May the goat be with you!</p>
<p>-Chris Pressey
<br/>November 1, 2007
<br/>Windsor, Ontario, Canada</p>
</body>
</html>