breaking symmetry to maintain it

In the last post i suggested a syntax that shared a family resemblance with Dirac notation. Now, i'm going to take that idea considerably further. i'm going to get there by pushing hard on this interpretation of composition as container. The metaphor we developed previously was denoting containers in terms of "colored" braces; and, because our notion of composition is associative we can legitimately write n-ary compositions without needing to indicate the order of binary compositions necessary to achieve the n-ary term. In symbols

• [C| m1, m2, ..., mN |C]

the opening and closing braces, [C| and |C], respectively, are colored C; and the components of the composition are m1,...,mN. This corresponds to a term of the form

• m1 *C m2 *C ... *C mN
  

We assume, for the moment, that colors are given outside the framework. They could be specified as some set of elements. In some sense our theory is dependent on a notion of color -- much like the π-calculus is dependent on a notion of name. (This should be a big clue as to what will ultimately come about.) The simplest syntactic account of our data structure is

• m ::= g1,...,gN | [C| m* |C]

(Ask yourself: where are the identities?) This structure depends on a supply of generators, gi, and a supply of colors, C. Eventually, we are going to eliminate these dependencies, but the first step we take is to relax color-matching. Every opening must be matched by a closing, but not necessarily a closing of the same color. Thus, we have

• m ::= g1,...,gN | [C| m* |D]

This is the step that allows us to form bra-ket-like terms. If generators could be interpreted as operators and colors as nomenclature for vectors (and their duals), then we have the potential for a term language for performing certain class of quantum mechanical calculations. The next step might seem to take us away from that possibility, however, as we're just going to ditch the generators. What get's us 'off the ground' as it were is the pairs of colored braces with nothing in between (in Dirac notation this is just a fancy way of writing a scalar).

• m ::= [C| m* |D]

Now, we remove the dependency on a set of colors. The way we do this is to invent a color of braces that turns terms to colors. This may seem circular, and it is. My favorite kind of circular: meta-circular. We are trading the risk of a possibly infinite set of unknowns (the colors), for exactly one unknown, a single color. We'll make this builtin color symbolically distinct from the others.

• m ::= [C| m* |D]
• C,D ::= (! m !)
  

So far so good. We now have an infinite set of compositors. This allows for a great deal of freedom in interpreting what's a generator and what isn't.

In fact, this corresponds to the intuition i had several years ago, now, that set theory with atoms could be done with different colored braces -- thus eliminating the need for infinitary risk (aka non-effectivity) in that theory. You can read more about it in those posts. However, the operational idea is simply stated. Set theory comes with a certain collection of observations and procedures you can perform on entities in that universe of discourse. You can ask whether a certain something is an element of a set, and you can enclose a given collection of things in between braces. In particular, we cannot probe into the structure of a "thing" unless it is a set, and then we can probe with element-of questions. All of this structure and discipline is completely undisturbed if we imagine that the braces come in colors and that for each color of brace we have a corresponding element-of operation that can only see into braces of that color. This is easily and effectively modeled and i have written Haskell programs to illustrate the core set theory you get from this. Moreover, i have given representations of von Neuman style numerals in this system to illustrate how coding works in this framework.

The framework we're exploring now represents an enrichment of this idea where the colors have been reified and the act of opening must be matched by the act of closing, but the colors don't have to match. You can open tragically and close comically, to add a little color to the discussion. We are, however, going to borrow a little more from the set theoretic intuitions. We're going to see what we can do with a comprehension notation. The reason for that is we would like to be able to form infinitary compositions, but to do so lazily -- or more accurately, intensionally. You see, once we adopt the braced notation, the intuition that

• [C| m1, ..., mN |C]
  

is a lot like an extensionally described set -- a set in which we have explicitly delineated each of the elements -- leads one to wonder what would be an intentionally described set. This question is deeply related to Phil Wadler's insight that monads are a lot like comprehensions. The comprehension notation allows one to give an intensional description of a set, to specify a set's elements in terms of patterns and predicates. In our multi-colored world this should look something like

• [C| t : p |C]

where t is a pattern and p is a predicate. All we have to do is say what patterns and predicates are. Given the discussion so far, it should come as no surprise that we are going to build these entirely out of what we have in the existing term language.

For predicates we are going to make heavy use of the idea of generating logics from term languages that was developed in previous posts. In fact, what we developed was the notion that a logic is nothing more than pulling the operations of a given 'notion of collection' (set, multiset, list, quantale, ...) through a given term language. Again, we would like to remain completely agnostic about the 'notion of collection'. These are going to be given by some color of brace. Furthermore, all of the operations on such collections will also be given by some color brace. So, a predicate is given entirely in terms of rules for distributing one set of braces over another. Thus, syntactically, we can enclose a term in a request to perform this distribution to describe a predicate. If we have another built-in color for that specific request, we've already got the syntax.

• m ::= [C| m* |D] | [C| t : p |D]
  
• C,D ::= (! m !)
• p ::= (? m ?)
  

The idea of pattern is closely related to the idea of predicate, but more concrete. A grammar for patterns is quite literally a differentiation of a term language -- adding variables to the term language. We know how to make variables -- we quote terms; but... quotes are just another color of brace. Thus, our language is given completely by the following grammar.

• m ::= [C| m* |D] | [C| t : p |D]
• t ::= [C| x* |D]
• x ::= m | v
  
• C,D ::= (! m !)
• p ::= (? m ?)
• v ::= (: m :)
  

So, we have arrived at a term language in which we can express extremely general kinds of calculations on very fancy containers including monadic calculations and -- yes -- quantum mechanical calculations. In fact the term language captures a kind of syntactic symmetry underlying a very broad class of languages for hosting computations. In the next few posts, we'll put it to work to expose more of this. For now, we close with a reminder of the title of this posting -- we broke the literal symmetry of color-matching on open-close pairings to expose a much deeper symmetry.