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

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

[Greg Meredith]

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

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

[Mike Stay]

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

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

[Greg Meredith]

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

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

[Mike Stay]

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