typed lambda calculus:cartesian closed categories::sorted pi calculus:?
As far as I can tell, the major difference between lambda calculus and pi calculus is that the rewrite rules in pi calculus aren't confluent, so it doesn't make a lot of sense to consider rewrite-equivalence classes of terms. What kind of category (or bicategory) does sorted pi calculus give? -- Mike Stay - metaweta@gmail.com http://math.ucr.edu/~mike http://reperiendi.wordpress.com [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
Dear Mike, Is your question motivated by an interest in equivalences or categorical models? For the "unsorted" π-calculus the most well exercised categorical models are certain classes of functor categories. You need this "extra layer" to take into account the name generation. Maybe i'm not seeing something, but i don't think introducing a sorting discipline will perturb these models very much. It certainly doesn't affect confluence. You can have well sorted processes that are not confluent. The lack of confluence arises from the essential non-determinism in reduction. Here's a race condition that is still well-sorted: - (new u : S)x?(y).y!(u) + (new v : T)z?(w).w!(v) | (new a : A)x!(a) | (new b : B)z!(b) - reduces along one path to (new a)(new u)a!(u) - and along another to (new b)(new v)b!(v) The better equivalence for the π-calculus is bisimilarity. In fact, in many cases of (nominal) rewrite systems that are confluent, bisimilarity can be the better equivalence. Consider applicative bisimilarity for the lambda calculus. More generally, there are results that show that the entire family of proposed processes equivalences can be characterized as bisimulation up to. Best wishes, --greg P.S. There's something very strange going on in this hierarchy of equivalences. As the equivalences can see more fine-grained structure, the complexity goes down. Language equivalence for regular languages is P-Space. The corresponding bisimulation problem is polynomial. The language equivalence problem for CFLs: not decidable. The corresponding bisimulation problem: polynomial. You might wave this away by observing that in the language equivalence situation you are searching "program space" while in the bismulation situation you are checking that two program match in a step-by-step fashion. But, then consider the logical equivalence of spatial-behavioral logic -- which is strictly more expressive than bisimilarity. On Tue, Aug 25, 2009 at 10:40 AM, Mike Stay <metaweta@gmail.com> wrote:
As far as I can tell, the major difference between lambda calculus and pi calculus is that the rewrite rules in pi calculus aren't confluent, so it doesn't make a lot of sense to consider rewrite-equivalence classes of terms. What kind of category (or bicategory) does sorted pi calculus give? -- Mike Stay - metaweta@gmail.com http://math.ucr.edu/~mike <http://math.ucr.edu/%7Emike> http://reperiendi.wordpress.com
[For admin and other information see: http://www.mta.ca/~cat-dist/<http://www.mta.ca/%7Ecat-dist/>]
-- L.G. Meredith Managing Partner Biosimilarity LLC 1219 NW 83rd St Seattle, WA 98117 +1 206.650.3740 http://biosimilarity.blogspot.com [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
Dear Mike, i missed another point in your mail. There's another difference between the lambda calculus and the π-calculus. As formulated, the lambda calculus is higher order: you can pass lambda terms as arguments to lambda terms. In the original formulation of the π-calculus it is not higher order. You can pass names around, but you can't pass processes around. There are higher order versions and there is a compilation scheme from higher order to name-passing. However, the higher order structure significantly changes the calculus. For example, you can get rid of replication with higher order structure. Beyond this point you have a bifurcation in the kinds of higher order calculi. In the models proposed by Sangiorgi, et al, you have two kinds of variables -- ones that carry names and ones that carry processes. To my sensibilities this is significant extra structure. In the models proposed by Radestock and myself, you have only 1 kind of variable, but you have reflective structure, allowing the interconversion between processes and names. This structure allows you to drop the new operator. Again, this is clearly extra structure. All in all, i think we can safely conclude that "higher order capability" is another difference between lambda and π-calculus that is not merely administrivia. Best wishes, --greg [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
Thanks, all, for your helpful comments! On Tue, Aug 25, 2009 at 10:40 AM, Mike Stay<metaweta@gmail.com> wrote:
As far as I can tell, the major difference between lambda calculus and pi calculus is that the rewrite rules in pi calculus aren't confluent, so it doesn't make a lot of sense to consider rewrite-equivalence classes of terms. What kind of category (or bicategory) does sorted pi calculus give? -- Mike Stay - metaweta@gmail.com http://math.ucr.edu/~mike http://reperiendi.wordpress.com
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]
participants (2)
-
Greg Meredith -
Mike Stay