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

- m1 *C m2 *C ... *C mN

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

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

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

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

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]

- [C| t : p |C]

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

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

## 3 comments:

Dude, you are high.

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

# C,D ::= (! m !)

This language appears to be empty (at least in a least-fixpoint manner) due to a lack of terminals.

JP,

i didn't see your comment until now. Just like set theory, this bottoms out at the empty braces.

Best wishes,

--greg

Post a Comment