Cabra

Cabra is a formal "programming" language, the set of whose programs form an algebraic dioid (an idempotent semiring) under the operations of sequential composition (considered multiplicative) and parallel composition (considered additive), over the equivalence relation "computes the same function". Cabra was designed by Chris Pressey in 2007.

The fact that Cabra programs form an idempotent semiring means that they have some of the same properties as mathematical structures such as lattices. For example, it is sensical to take the max() or min() of a set of Cabra programs.

Despite a persistent "programming" motif (Cabra programs contain imperative updates, conditionals, and can fail to terminate,) Cabra is nowhere near Turing-complete, nor suitable for any serious programming. In fact, Cabra is not even equivalent to finite-state machines, since it cannot properly loop.

Introduction

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 that five times fast!)

Cabra is the successor to Burro, 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 programming in Cabra... but it is a formal language.)

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 group over an equivalence relation 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 algebra over an equivalence relation, and it is this notion that is applied in Cabra to dioids.

The original intent of Cabra was to devise a language whose programs formed a ring 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 idempotent semirings were chosen instead. Idempotent semirings, sometimes called dioids, lack the additive inverses that rings have, but unlike rings, have an idempotent additive operator.

Let's get straight to it.

Language Definition

Every Cabra program takes, as input, an input set, which is a set of non-negative integers. Every Cabra program either produces an output set, which is also a set of non-negative integers, or it fails to terminate.

A Cabra program is defined inductively as follows.

The instruction SET n, where n 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 {n}. (The output set is just like the input set except that it also includes n if it was missing from the input set.)

The instruction UNSET n, where n 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 {n}. (The output set is just like the input set except that it never includes n, even if n was included in the input set.)

If a and b are Cabra programs, then IFSET n THEN a ELSE b is a Cabra program, where n is any non-negative integer. If n is a member of the input set of the IFSET program, then the input set is used as the input set of a, and the output set of a is used as the output set of the IFSET; b is ignored. Conversely, if n is not a member of the input set the IFSET, then the input set is used as the input set of b, and the output set of b is used as the output set of the IFSET; a is ignored. (IFSET is the conditional statement form.)

If a and b are Cabra programs, then a*b is a Cabra program. The input set of a*b is used as the input set of a. The output set of a is used as the input set of b. The output set of b is used as the output set of a*b. (This is sequential composition; a is executed, then b. A more usual notation might be a;b.)

If a and b are Cabra programs, then a+b is a Cabra program. The input set of a+b is used as the input set of both a and b. The output set of whichever of a or b terminates first is used as the output set of a+b. 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 a||b.)

If a is a Cabra program, then (a) is a Cabra program. This is just the usual usage of parentheses to alter precedence. Without parentheses, * has a higher precedence than +, which has a higher precedence than IFSET. For example, this means that IFSET 42 THEN SET 51 ELSE SET 5 * SET 6 + SET 7 is parsed as IFSET 42 THEN (SET 51) ELSE ((SET 5 * SET 6) + SET 7).

The instruction SKIP is a Cabra program. The output set of SKIP always equals the input set. (SKIP is a no-op.)

The instruction BOTTOM is a Cabra program. Regardless of the input set, this program always fails to terminate. (BOTTOM is an infinite loop.)

Were I a pedantic mathematician, here's where I'd mention how nothing else is a Cabra program. As if I could be so sure about that.

Terminates First

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 cycles. A Cabra program a terminates before b if the number of cycles taken by a on some input set S is less than the number of cycles taken by b on S; or, if the number of cycles taken by a on S is the same as the number of cycles taken by b on S, then a terminates before b if a has a smaller lexical order than b. (If a and b have the same lexical order then a = b and "terminate before" is meaningless because it only defined between two different Cabra programs.)

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 a is executed, then one cycle of b, and so forth, until one or the other terminates.)

• SKIP takes 0 cycles.
• BOTTOM takes an infinite number of cycles.
• a*b takes the sum of the number of cycles taken by a and the number of cycles taken by b.
• a+b takes the either the number of cycles taken by a or the number of cycles taken by b, whichever is fewer.
• IFSET n THEN a ELSE b takes either the number of cycles taken by a or the number of cycles taken by b, whichever was selected for execution.
• SET n takes n cycles if n was not already set, but only 1 cycle if it was already set.
• UNSET n always takes 1 cycle.

In fact, other formulae are possible. The somewhat unusual determination of cycles in the case of SET n is mainly to keep things interesting by ensuring that the number of cycles is dependent upon the contents of the input set.

Probably goes without saying, but to state it anyway: for a program a which is an element of a set of programs P, we say a terminates first (with respect to P) if it terminates before every other program in P.

Lexical Order

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.

For primitive programs: SKIP comes before UNSET 0 which comes before UNSET 1 which comes before UNSET 2, etc. All of these come before SET 0, which comes before SET 1, etc. And all of these come before BOTTOM.

For compound programs, the ordering is IFSET n THEN a ELSE b comes before IFSET n+1 THEN a ELSE b comes before a+b comes before a*b.

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 deriving (Ord).)

Comments

Oh, but I can hear you objecting now: Waitaminnit! This language is totally weak. You can't do hardly anything with it.

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.

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, WHILE loops, input/output, and the like, but you can readily see that these ameliorations don't make the central problems any easier.

Another reason is that Cabra, despite almost being, say, just a kind of algebraical structure, looks 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 machine — because of the definition of how parallel composition works in terms of cycles and everything.

A third reason is that it's just a little... askew. Note that if we had a WHILE instruction, we wouldn't need a BOTTOM instruction because we could just do something like WHILE FALSE SKIP. But we don't have WHILE. 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...

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.

Dioid Theory

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 〈S, +, *〉 where:

• S is a set of elements;
• + : S × S → S is a binary operation on S; and
• * : S × S → S is another binary operation on S,

where the following axioms of dioid theory (over an equivalence relation!) hold:

• (a + b) + c ≡ a + (b + c) (addition is associative)
• a + b ≡ b + a (addition is commutative)
• a + 0 ≡ 0 + a ≡ a (existence of additive identity)
• a + a ≡ a (addition is idempotent)
• (a * b) * c ≡ a * (b * c) (multiplication is associative)
• a * 1 ≡ 1 * a ≡ a (existence of multiplicative identity)
• a * (b + c) ≡ (a * b) + (a * c) (multiplication left-distributes over addition)
• (a + b) * c ≡ (a * c) + (b * c) (multiplication right-distributes over addition)
• a * 0 ≡ 0 * a ≡ 0 (additive identity is multiplicative annihiliator)

Now I'll attempt to show that Cabra programs form an idempotent semiring, over the equivalence relation of "semantically identical", under the Cabra operations +, considered additive, and *, 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.

Parallel composition is associative. The result of (a+b)+c never differs from the result of a+(b+c), because all of a, b, and c 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.

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 a+b, a and b aren't really running in any order; they're running at the same time. The result of a+b is determined by which of a or b terminates first, and this is not affected by which order they appear on either side of the + operator. (In fact, that was why I introduced the "lexical order" tie-breaker, lest a dependency on this were accidentally introduced.)

There is a neutral element for parallel composition. Indeed, BOTTOM is this neutral element. Any program a that terminates will by definition terminate before BOTTOM, therefore a+BOTTOM ≡ BOTTOM+a ≡ a.

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.)

Sequential composition is associative. The result of a*b*c does not differ if one first composes a and b to obtain a new program, say d, then composes d and c, or if one first composes b and c to get e, then composes a and e. An analogy can be drawn in a "block-structured" language like Pascal: the program BEGIN A; B END; C is semantically identical to A; BEGIN B; C END.

(Note that we are talking about composition 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 execute those component programs in a different order, that would be a different story: execution is indeed non-associative.)

There is a neutral element for sequential composition. Indeed, SKIP is this neutral element. Say some program a takes input set S and generates output set T. Then the programs a*SKIP and SKIP*a will also, fairly obviously, produce T when given S.

Sequential composition left-distributes over parallel composition. This is similar to the argument that parallel composition is idempotent. If you have a program a that runs before two programs in parallel b+c, it doesn't matter if one copy of a runs sequentially before both b and c, or if two copies of a run in parallel, one sequentially before b and one sequentially before c. In both cases it's as if one copy of a ran, and in both cases both b and c get the same input set.

Sequential composition right-distributes over parallel composition. Consider a+b. On some input S, a will take x cycles and b will take y cycles, and the output set T will from be whichever of these numbers of cycles is smaller. So if there was a subsequent program c, it would take T as its input set, and it itself would take z cycles. Now suppose we sequentially compose c onto each of these subprograms: a*c will take x + z cycles, and b*c will take y + z cycles. Because addition is monotonic — if x > y then x + z > y + z — whichever branch was the "winner" of a+b, the same branch will be the winner of (a*c)+(b*c). Also, in this branch, the input set to c will still be T, the output set of the winning branch of a+b. Thus the final result will be the same. (See below for much more on this.)

The neutral element for parallel composition is an annihilator for sequential composition. Indeed, if we run a*BOTTOM, or BOTTOM*a, neither of those terminate, so we get the same result as running just BOTTOM.

Notes

On Rings

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.

But, it turned out not to be a cakewalk.

For Cabra programs to form a full-fledged ring, every program would need to have a unique additive inverse. That is, for every program a, there would need to be another program b, where a+b ≡ BOTTOM. But there can be no such program, as Cabra has been defined: if a terminates, then there's nothing b can do to stop a from terminating.

So Cabra programs do not form a ring. Further, it's unclear what would have to change to allow this. A simple instruction HANGOTHERS could be defined as sort of throwing a monkey wrench into every other currently executing program: a+HANGOTHERS ≡ HANGOTHERS+a ≡ BOTTOM. But every element is supposed to have a unique additive inverse, and this doesn't do that, because HANGOTHERS causes every other program to hang.

The only thing I can think of that even might work is to require programs participating in a+b 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.

Semantics of +

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, definite problems arise, whether in a ring or a semiring.

Take, for instance, a semantic where the output set of a+b is the union of the output sets of a and b 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.

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

(SET 1 + SET 2) * IFSET 1 THEN (IFSET 2 THEN SET 3 ELSE SKIP) ELSE SKIP

evaluates to {1, 2, 3} on a null input set, because (SET 1 + SET 2) 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

(SET 1 * IFSET 1 THEN (IFSET 2 THEN SET 3 ELSE SKIP) ELSE SKIP) +
                  (SET 2 * IFSET 1 THEN (IFSET 2 THEN SET 3 ELSE SKIP) ELSE SKIP)

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.

Or, we could take a semantics where the output set of a+b is the intersection of the output sets of a and b 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.

But this, too, fails to be right-distributive. Consider

(SET 4 + UNSET 4) * IFSET 4 THEN (UNSET 4 * SET 6) ELSE SET 5

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,

(SET 4 * IFSET 4 THEN (UNSET 4 * SET 6) ELSE SET 5) +
                  (UNSET 4 * IFSET 4 THEN (UNSET 4 * SET 6) ELSE SET 5)

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}.

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 BOTTOM, the result would be BOTTOM — which in turn suggests that BOTTOM would be an annihilator for addition as well as for multiplication, and that (at least in the union case) SKIP 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 only one element, which is clearly not the case here.

(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 same 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 don't depend on each other at all have some given result when one is executed after the other, they'll have the same result when they are executed concurrently — because they don't depend on each other at all! Thus in this case + = * and we're really talking about something that's a monoid or group or something, not a ring.)

Based on this, I will go so far as to conjecture that, in fact, any semantics for parallel composition a+b (in an otherwise Cabra-like language) that combines results from both a and b 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.

Other Algebras

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.

Take, for example, Kleene algebras. A Kleene algebra is a dioid with an additional unary postfix operator *: S → S. It denotes a kind of additive closure: for any element a, a* ≡ 0 + a + (a * a) + (a * a * a) + (a * a * a * a) + ... Kleene algebras are used for such things as the theory of regular expressions, where the Kleene star indicates "zero or more occurrences."

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 a always takes fewer cycles than a*a (except when a is SKIP, and in that case a*a ≡ a,) and since any a takes fewer cycles than BOTTOM, it appears that a* ≡ a in Cabra.

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.

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.

Also, if it were not for BOTTOM, every program would have a multiplicative inverse: simply find which elements of the set the program changes, and undo those changes: do a SET everywhere it did an UNSET, 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.

Implementation

There is an implementation of Cabra in Haskell, cabra.hs, 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.

History

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.

May the goat be with you!

See also

• Burro

External resources

• Cabra entry at Cat's Eye Technologies