Talk:Pi-calculus
From Wikipedia, the free encyclopedia
Contents |
[edit] Usefulness of pi-calculus?
Articles with a red discussion link are either very very good or substandard. It is as yet completely unclear to me how the pi-calculus can be used to do anything usefull. It has the zero process. You can run two of them concurrently, but isn't 0|0 = 0 ? And also !0 = 0 ? How then do you build processes that _do_ anything? Or do you use lambda calculus for this? Also I am mystified by the deduction rule "if P -> Q then also P|E -> Q|E". And by the way -> is not explained anywhere. We have "if x<y>.P | x(z).Q, then also P | Q[y/z]" thus
(x<y>.P | x(z).Q) -> (P | Q[y/z]) implies
(x<y>.P | x(z).Q | x<a>.P) -> (P | Q[y/z] | x<a>.P) but also by symmetry
(x<y>.P | x(z).Q | x<a>.P) -> (P | Q[a/z] | x<y>.P) .
This does not seem right. Anyone? MarSch 16:06, 14 Apr 2005 (UTC)
- As stated in the article, Pi-calculus in not a programming language; its purpose is to model concurrent processes. This end is achieved with creating and communicating names. I believe -> means "can be reduced to". Your example is absolutely right and contains no contradiction: you have three concurrent processes, two of which send a message on channel x, and one of them blocks waiting for a message on that channel. Obviously, the "listener" process can receive either one of the two messages, as illustrated by your example. --146.6.101.9 17:58, 2 May 2005 (UTC)
Not finished reading this interesting article yet, but I'd like to suggest changing the BNF syntax description for readability. The "|" sign is used in different meanings. It is used as the BNF "or" and in the Pi-calculus itself. I suggest changing one sign or quoting the blocks. -- Helmut 84.133.58.203 17:42, 19 December 2005 (UTC)
- I’ve tried to make it a bit more readable without changing the | symbols. If it is sufficiently less ambiguous now, then the spacing hint should be better than a change of either grammar. (After all, formal definitions are supposed to make things clear, not confusing…)
- However, I am a bit unsure about whether the grammar and the immediately subsequent discussion is entirely accurate. Rather than try to pick out inaccuracies (difficult for me due to not having enough knowledge about the topic), I’ll just ask whether it might be a good idea to make the formal definition more similar to the one in chapter 2 of Milner’s tutorial. I’ll see if I can get back to the article with a good book, but help is appreciated. --xyzzy_n 23:12, 16 February 2006 (UTC)
Shouldn't Occam-Pi be added to the implementations list? --Sergiu.dumitriu 01:36, 4 January 2006 (UTC)
[edit] Pi- and n-calculus
I'm confused - the article is supposed to discuss the pi-calculus, but half of it explain the n-calculus instead. Why? Which is which and how do they differ? --134.102.204.196 10:44, 25 January 2006 (UTC)
- I believe you'll find that the article is discussing the π-calculus (as in the Greek letter pi), rather than the "n-calculus". Pi-calculus == π-calculus, but the latter is the form that π-calculus researchers like Milner, Parrow, and Sangiorgi tend to use, so that's what appears in this article. Perhaps it just isn't rendering well in your browser. --Allan McInnes 16:23, 25 January 2006 (UTC)
[edit] Parallel languages
The article states that the lambda calculus has been used to model parallel languages. While that may be true, in some strict sense, wouldn't it a better comparison with pi-calculus to say that lambda-calculus models _sequential_ programming languages? —The preceding unsigned comment was added by 83.72.35.16 (talk • contribs) .
- I think you'll find that the article originally did say that, and was changed by User:CarlHewitt as part of what appears (to me) to be a campaign to make widely known his opinions about the relative capabilities of the Actor model and λ-calculus to model concurrency. I agree that "sequential programs" is less confusing — I'll switch it back now. --Allan McInnes 23:17, 28 January 2006 (UTC)
[edit] Notation for Early and Late bisimilarity unexplained.
The section on early and late bisimilarity left me lost, mainly, I believe because of the unexplained notation. Why is a(x) used sometimes and α used other places?
For example:
VS
And to what might the x in a(x) refer - especially as the text seems to talk about a binary relation?
- I think you'll find that, if you look further up in the article, a(x) indicates that a value should be received through channel a, and bound to the name x in the following process. Thus the need to break out the bisimulation definition involving a(x) separately from the definitions for every other kind of action (every other kind of action being denoted α): the definition for a(x) actions requires the additional rule that , i.e. that p' and q' both perform the same substitution of received values (y) for previously unbound names (x).
- I'm not sure it's a good idea to repeat the symbol definitions given in the syntax section again in the bisimilarity section. But if you feel that the surrounding text could explain things better, I'd be interested in hearing suggestions. --Allan McInnes (talk) 16:49, 13 June 2006 (UTC)
[edit] Recent cleanup
I cleaned up the presentation quite a bit. In particular, the presentation of structural congruence had become confusing, and as a consequence the account of the reduction semantics was close to meaningless. I also added a short example that should explain the finer points of name passing. If I find the time at some point, I will add a short section about type systems. HansHuttel 16:50, 5 Jul 2006 (UTC)
[edit] Errors in the examples
The section "The example revisited" seems to have extra open parentheses or be lacking close parentheses. I'm not confident enough in my grasp of the material to correct them, so could someone experienced take a look? --Lemur821 17:29, 6 August 2006 (UTC)
- Thanks for noticing that! I’m no expert either, but it looked like there was a bad opening parenthesis, so I removed it. Does it work now? —xyzzyn 17:51, 6 August 2006 (UTC)
The examples are still wrong. The scope of the bindings for receives should extend to the closing parenthesis. That is,
- x(y).P
should consider all free variables y in P to be replaced. This means that
should have been
I also suggest to explain scope extrusion in more detail.
--Robert van Engelen 21:50, 6 December 2006 (UTC)