Home » forums » LtU Forum

What kind of a category is the blue calculus?

The blue calculus has been mentioned here before, but I'm having trouble figuring out what kind of category arises from it. Terms in Blue are objects and reduction rules are morphisms.

This is kind of odd, since the typical view of the lambda calculus has types as objects and reduction-rule-equivalence-classes of terms as morphisms. Since the blue calculus isn't confluent, that approach doesn't really work.

Given a category T of types and type-preserving maps, you can type the blue calculus with a functor F:Blue->T; this functor is defined recursively using type inference rules. The original paper only considered the case where T is a discrete category.

This paper on how pi calculus is a cartesian closed double category might be relevant, but I haven't been able to understand it yet. It's not even clear to me what the objects, horizontal and vertical morphisms are.

Can anyone help?

By mikestay at 2008-06-09 04:46 | LtU Forum | previous forum topic | next forum topic | other blogs | 5206 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

One thing to note is often

One thing to note is often times that "reduction-rule-equivalence-class" is avoided by instead using a 2-category where the 2-cells are rewrite rules.

By Derek Elkins at Mon, 2008-06-09 04:57 | login or register to post comments

composition

Yes, I'm aware of that; thanks. However, in the lambda calculus, given a term, it's clear what morphisms are being composed:

A term is the name of a morphism, a morphism from the unit object to the type of the term. Let f:X -o Y, x:X (I'll use the lollipop to distinguish the internal hom from the external hom.)

The application fx uncurries f to get ~f and then composes with x:
   I --x--> X --~f--> Y
which is a term fx:Y, as desired.

If we use a 2-category instead, this composition might not be strictly associative, but it would still be clear who things were being hooked together.

What's being composed in a blue calculus term like
   (( fz | z<=x ) | z<=y ) ?

By mikestay at Mon, 2008-06-09 16:50 | login or register to post comments