Collectivity and inten(s/t)ion

Eventually, i'm going to have to get back to the reproduction and replication thread, but this is just so cool i have mention it. Back in the postings on algebraic databases i explored the notion of generating logics from term languages by providing a generic procedure for generating formulae and their semantics from the term language. The idea is a generalization of what is going on is Caires' spatial logic -- which is itself a generalization of the program Abramsky outlined in Domain theory in logical form. These phenomena and others -- such as Stone duality -- are in my opinion part of a deeper notion that is adumbrated by what we call the Curry-Howard or propositions-as-types paradigm.

This notion shares a quality with the Church-Turing hypothesis. Both of these ideas have escaped mathematical characterization of their essential content. In the case of the Church-Turing hypothesis we have lots of instances of encoding one model of computation into another (such as the λ-calculus into Turing machines, or π-calculus into λ-calculus) but we have as a community been unable to formulate a statement of the idea as a provable (or refutable) statement. Likewise, there are lots of instances of the proposition-as-types paradigm and lots of connected phenomena but not statement of the idea underlying all these mathematical observations in an unequivocally provable or refutable fashion. As such the notion is particularly attractive to me -- elusive and deep.

Now, i believe i have a proposal in hand for a statement of the essential mathematical content. What's at stake here is the relationship between collectivity -- groups, populations, entities in which multiplicity and containment are explicit acknowledged and modeled -- and property -- some declarative or intensional description of a quality or aspect of observable form. That's what's going on in all these instances. i submit that a genuine understanding of this relationship has practical implications for technology, science and society -- which i will enumerate below. i also feel that -- like most deep concepts -- the formal content is profoundly simple.

So, without further preamble, i will state it now. We start with the following data.

• A monad for a term language (data structure, record structure, program structure).
• A monad for a notion of collection (sets, lists, destructively modifiable stores, ...).

Then we simply pull the notion of collection through the term language. That is, we build the term language over collections. At this point i have already given several examples in my blog and on LtU, but i will recapitulate a very simple one here. Here's our data.

• Monad for a free monoid
• Monad for sets

Then we simply distribute the monad for sets over the monad for the free monoid. Let's do this explicitly. Here's funny way to write the free monoid term language gadget.

• m ::= e | g1 | ... | gN | m*m
• This grammar generates "monoid expressions" in N generators
• If we impose the relation(s) (which we will call structural equivalence in the sequel) m*e = m = e*m, then we get the free monoid

We'll give the other monad -- for Set -- in a more standard way.

• unit(x) = { x }
• mult = flatten

Now, here's the essence of the trick we want to make our term language work over sets. This construction is a lot like standard pt-wise liftings of various constructions -- it's just that the language of monads allow us to be "pointless". We're going to get a "logical" language the denotations of which are sets of terms. So, if L(m) is the set of all monoid expressions then we can simultaneously specify the syntax and the semantics in the following equations

• [| true |] = L(m)
• [| ~φ |] = L(m) \ [| φ |]
• [| φ & ψ |] = [| φ |] ∩ [| ψ |]
  

This first set of equations comes to us for "free" because we are working in the power set of L(m). The next set is where we actually see the term language pulled over the collection monad.

• [| e |] = { m ∈ L(m) | m = e }
• [| gi |] = { m ∈ L(m) | m = gi }
• [| φ * ψ |] = { m ∈ L(m) | m = m1*m2, m1 ∈ [| φ |] m2 ∈ [| ψ |] }
  

Here the "=" refers to the structural equivalence. Our monoid term structure is giving us exactly the formulae we need to look into monoid terms. Finally, to this set we can add the usual things like quantifiers and least or greatest fixpoints. The point here, however, is that the collection monad has been "pulled through" the term language monad. This is another aspect of the content of Eugenia Cheng's insights about (iterated) distributed monad laws. (And, that's one of the sources informing the choice of title of this posting -- we're distributing 's' over 't'.) Now, there are lots of directions we can go with this. Let's enumerate some of the possible threads of discussion.

• What happens when you use different term languages and different collection monads? Brilliant question, grasshopper. i can see you will go far; but, let us proceed slowly.
  
• Curry-Howard is not just about formulae; it is about the correspondence of formulae and types and proofs and programs. How do you extend this approach to include morphisms? Further, when the term language is for program terms, how does all this work? To this i must say: well observed, grasshopper; and in time all will be revealed. In the interim look at Caires' recent CALCO paper.
• How is this math related to practical issues in technology and science? To this i must also say: excellent question, grasshopper; patience is the mother of enlightenment.
  

i want to focus here on the practical implications to society. At the heart of this discussion is a radical proposal regarding collectivity and intention with a 't'. Firstly, i want to propose that groups and collectives -- in the social sense -- are real entities, not just metaphors or (in)convenient legal fictions. There is a lot of popular press focusing in on 'group' or 'collective' intelligence. There are a number of primitive tools, like looking at averages of quantitative estimations, to provide witness to the existence and efficacy of 'collective' intelligence. Moreover, we recognize this reality in democratic forms of self-determination. Political will is something more than the aggregate of the individuals. And, we look for tools, like voting schemes and polling strategies, to provide some means of mediated communication between the individual and the collective. i argue, however, that these tools are much too primitive to facilitate a detailed and two-way dialogue between the collective and the individual. i think we need a language that can be spoken and understood by the collective and the individual.

i want to propose that the logics that arise from this operational view of the content of the Curry-Howard isomorphism are a family of natural candidates for such a language. If you were looking for a good fishing spot to catch such a fish, i'd advise you to fish there. And, now for the really radical proposal... (drum roll please)... Beyond the fact that these logics provide a means by which to describe qualities or aspects shared by members of the collective there is the possibility that the intention of the collective -- what brings them together as a collective -- might be identified with the logical, intensional description that picks out just that collective. In the formal language described above, i am suggesting that intention of the extension (the meaning, semantic denotation) of a given formula is the formula. Let me say it another way, the collective of individuals that may be described by a given formula intends that formula. What the group, the state, the electorate or the market says to (whoever's listening) is the formulae that picks out that group.

In terms of technical considerations like many formulae have the same extension, you can resolve this by composition (conjunction, disjunction, ...). This comment is designed primarily to keep focus on this very strange, but intriguing idea that what the collective says is what the formula that picks out that very collective means. To sloganize just a little, 'what brings us together is what we intend.' (And this is the other source for the choice of title for this posting, we are finding a way to 'confuse' intension with intention.) If this idea is more than just a crazy idea of a mad (computer) scientist, it means that individual and collective, voter and electorate, shareholder and corporation can sit down over a cup of coffee and have a conversation in a language as detailed and rich as the one employed to write this blog entry. That changes the game entirely -- at just the time when we have the technology -- the Internet -- to actually build that coffee shop and make the Berlitz "tapes" for that language widely available.