Timeline for Terminologies of "Process calculus" and "Process algebra"
Current License: CC BY-SA 3.0
10 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Oct 12, 2014 at 14:45 | vote | accept | hengxin | ||
| Oct 10, 2014 at 13:34 | comment | added | babou | As I recall, maybe wrongly, the early models of λ-calculus were syntactic. The contribution of Dana Scott was to show how to build non syntactic models. I thought that the same might be true of the π-calculus. I agree that the laws derive from the algebra, not the syntax alone. That is why I was thinking that whatever computation rule are thus defined, for example by orienting laws as rewrite rules stay pretty close to the algebra. But they are probably not enough to do all you might want. But I am stretching my competence. | |
| Oct 10, 2014 at 13:12 | comment | added | Bordaigorl | As for how models are derived, they are not derived from syntax as you described: to give op sem as a directional version of the laws you need the laws in the first place, and those do not come as a specification of the syntax itself. Saying you can put two things in parallel does not tell you what they can do when they are. Algebraic laws are an alternative starting point to give semantics. | |
| Oct 10, 2014 at 13:11 | comment | added | Bordaigorl | You kind of lost me at Gödel (I think you need to constrain the kinds of models you are comparing to which kinds of algebras to make this point formal) but I think I see your general points. The thing is my remarks are specific to how things are done in concurrency theory and may not be directly relevant to the general level at which you are considering the problem of "algebra" vs "calculus". | |
| Oct 10, 2014 at 12:15 | comment | added | babou | Given that an algebra is an axiomatic view, and that a calculus is more an algorithmic view, i.e. a proof view, I would guess that the two views may run into Gödel type of incompleteness results, so that they are not quite equivalent, even though they aim to be so. All you need is enough arithmetics in the algebra. I have no idea whether that is the case for process algebra. Still, as soon as you use the algebra to prove things, an equivalence for example, it is no better than a calculus in that respect. Am I making sense? | |
| Oct 10, 2014 at 12:15 | comment | added | babou | I think your remarks do bring significant light on the issues. I am not familiar with the process view, which may make a difference. My impression was that the abstract computation machine, the operational semantics, is often derived from the syntactic model of the algebra. For example, you take known identities, provable algebraically, and use them directionally as a rewriting system, at least to get normal forms. But then, this is probably too simple to apply to all algebras, or to all problems for a given type of algebra. | |
| Oct 10, 2014 at 11:19 | comment | added | Bordaigorl | The difference between laws and concrete models is also made explicit by the fact that you need to prove that they match, it is not automatic. However, do not get me wrong, as I said none of the works I have seen take a "pure" view on these constructions, there are semantics models for CSP, for example. It's just that both viewpoints can spot different (and powerful) light on these systems. | |
| Oct 10, 2014 at 11:15 | comment | added | Bordaigorl | We are probably speaking about different things when saying "model". The "initial model" gives you syntax and a structural recursion principle. What I mean by model here is a "concrete abstract machine", an operational semantics which is in a sense external to syntax...does this make sense? | |
| Oct 10, 2014 at 10:56 | comment | added | babou | I am no longer very familiar whith these issues, so please correct me if I am wrong. It seems to me that your remark about specifying a model should be mitigated by the fact that you will usually choose an initial model to define semantics with a calculus, so that both the algebra and the calculus can be specialized hand in hand to any interpretation. So the idea that you specify a model (choose a specific model) for the calculus is not really accurate: you do not choose it, but it is given, imposed up to isomorphism. | |
| Oct 9, 2014 at 17:28 | history | answered | Bordaigorl | CC BY-SA 3.0 |