So the other day I had this fairly sizeable revelation in the shower, the explicit description of which apparently goes back at least to a 1994 paper of Bellegarde and Hook, which I only found out after I had the idea and checked citeseer for previous work on it. In hindsight, it's almost a non-idea; it's just an interpretation of a certain category-theoretic idea (whose name I will suppress for the sake of suspense) that I should have had from the very beginning.

What I was hunting around for in one of my little mathematical side projects was an algebraic structure whose elements are like terms over some finite set of variables; the algebra is supposed to be just abstract enough to permit substitution. This is so I can write down a type theory that has an annotation on every judgment that says in what way all the resources (i.e. variables) in the context are used. If I have a system kind of like linear logic, I might record that, say, to make the term M in the context x:A,y:B,z:C, the variable x is used 3 times, y 5 times, and z 17. The data (3x, 5y, 17z) would be an element of such an algebra. If I substituted a term N:B for y, and N exists in a context w:D,v:E, and, say, N uses w 100 times and v 0 times, then [N/x]M uses w 5 * 100 = 500 times, and v 5 * 0 = 0 times, because each of x's 5 occurrences in M is replaced by a term that uses w 100 times.

So, I have some sort of mapping T that takes a finite set of variables (say x,y,z) and returns a set of all the "descriptions" over that set. T(x,y,z) would contain things like (100x,4y,2z), (0x,0y,1z), and so on. Substitution would take an assignment from variables in, say Γ to terms over Δ, and allow me subsequently to convert full terms over Γ to terms over Δ. So if
f : Γ → TΔ
then there must be some function
f* : TΓ → TΔ
"Holy crap," I know you're saying to yourself just as I did yesterday morning, "I reckon that looks like the lifting operation of a Kleisli triple!" Indeed, the injection
η : Γ → TΓ
is also sensible, and necessary to say that each variable is actually a term, and the Kleisli axioms
η* = id
f* o η = f
f* o g* = (f* o g)*
correspond exactly to some basic properties of susbtitution
[x/x]M = M
[M/x]x = M
[O/y][N/x]M = [[O/y]N/x]M (assuming y not free in M)
So an algebraic "notion of term that supports substitution" is just a Kleisli triple, or to use a word that more programmers have heard of, a monad.

Moreover, the particular extra structure and equational axioms I need on top of this monad turn out to be very conveniently stated in the existing language of category theory. The fact that I need the little term algebras to be preordered can be accomplished merely requiring that the monad is in fact situated in the category of preordered sets, and the fact that the binary operation that exists over it respects both the preorder and substitution can be accomplished by saying it's a natural transformation from one carefully chosen functor to another.

---

The more I think about it, the more I'm surprised I hadn't figured this out earlier; the thing that I had been working with as a special case was the algebra of formal sums over some set of variables (i.e. the free commutative monoid over a set). It's painfully obvious in hindsight that it's a monad: it's just a slight variation of about the most canonical monad I can think of, the list monad, which arises in the exact same way from the free (not necessarily commutative) monoid over a set.
Tags:
• Post a new comment

#### Error

Anonymous comments are disabled in this journal

default userpic