Re: typed lambda calculus:cartesian closed :sorted pi calculus:?

[Greg Meredith <lgreg.meredith@biosimilarity.com>]

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/ ]