Examine individual changes

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