User loginNavigation 
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 reductionruleequivalenceclasses of terms as morphisms. Since the blue calculus isn't confluent, that approach doesn't really work. Given a category T of types and typepreserving 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 20080609 04:46  LtU Forum  previous forum topic  next forum topic  other blogs  4114 reads

Browse archives
Active forum topicsNew forum topics 
Recent comments
2 weeks 2 days ago
2 weeks 3 days ago
2 weeks 3 days ago
2 weeks 4 days ago
2 weeks 5 days ago
2 weeks 5 days ago
2 weeks 5 days ago
2 weeks 5 days ago
2 weeks 6 days ago
4 weeks 6 hours ago