- From: L.G. Meredith <lgreg.meredith@gmail.com>
- Date: Tue, 20 Jun 2006 15:17:23 -0700
- To: "Paul Bouche (HPI)" <paul.bouche@hpi.uni-potsdam.de>
- Cc: public-ws-chor@w3.org
- Message-ID: <5de3f5ca0606201517l3fe578b5ua2eec7241026af3@mail.gmail.com>
Paul, Based on my cursory reading of your paper i would hazard that you have gotten the evaluation criteria backwards. When a theory Y is claimed based on a theory X, one must exhibit a map from Y to X, not from X to Y. Your paper sought a mapping from \pi-calculus to WS-CDL. This is not what is required to ascertain whether WS-CDL is based on the \pi-calculus. Rather, one is looking for an interpretation (a map) of WS-CDL into the \pi-calculus. In traditional programming language semantics symbols, you seek something like a map [| - |] : WS-CDL -> \pi-calculus taking XML documents conforming to the WS-CDL schema and producing expressions in the \pi-calculus. Now, several comments are in order. First of all, we know that this is -- in principle -- possible. Why? Because the \pi-calculus is Turing complete. Thus, unless WS-CDL offers a model of computation that is richer than Turing machines -- highly unlikely -- we must be able to exhibit at least one such map (in fact there are many). But, just because we can exhibit such a map in no way actually justifies the claim "based on" the \pi-calculus. After all, we can also exhibit an interpretation of WS-CDL in the \lambda-calculus and finite automata with two pushdown stores and Turing machines and set theory and first order predicate logic, etc. None of these maps justify any claim of "based on". To justify this claim there must be some transparency of the mapping. Something must be preserved in the translation. For example, the notion of parallel composition maps directly to the notion of parallel composition, or the notions of choice maps directly to the notion of choice, etc. In symbols, you need something like [| <compose> WS-CDL-Process1 WS-CDL-Process2 <compose> |] = [| WS-CDL-Process1 |] | [| WS-CDL-Process2 |] or whatever the tag is that represents parallel composition (or the notion you seek to preserve). The more direct, i.e. transparent, i.e. the more that is preserved, the more you find justification for the claim "based on". Secondly, note that the \pi-calculus, like the \lambda-calculus, is a very impoverished model. It does not come with arithmetic types, or string types or structured data structures. There are, needless to say, lots of ways to interpret these notions as processes. But, that is unwieldy for practical purposes like specifying business protocols. In the \lambda-calculus there are very natural ways to embed these concepts at their standard levels of abstraction. In the \pi-calculus this is a much more subtle game and i submit that no one has found a particularly satisfying answer to this particular problem. (There is the notion of applied \pi-calculus; and i have investigated, more recently, notions of adding reflection to the \pi-calculus, thus embuing names with the structure of processes.) With this in mind one may find that the interpretation preserves gross program structure (parallel composition, sequencing, choice, etc); but not fine-grained program structure (data types and conditionals expressed on elements thereof). It is this latter activity that i believe the work on the global calculus reflects, but, i have not kept abreast of it and could easily be mistaken at this point. i hope this helps. Best wishes, --greg On 6/20/06, Paul Bouche (HPI) <paul.bouche@hpi.uni-potsdam.de> wrote: > > Hi Gero, hi everyone else, > > in response to Gero's questions, I can partly answer the last I think > because I have asked it here before. Here are three links I have found > helpful in discovering more about the global calculus: > [1] Carbone, Honda, Yoshida, "Programming interaction with Types" , > http://www.w3.org/2002/ws/chor/5/06/F2FJune14.pdf > > [2] Kavantzas, "Aggregating Web Service: Choreography and WS-CDL", > > http://lists.w3.org/Archives/Public/www-archive/2004Aug/att-0017/WS-CDL-April2004.ppt > > > [3] Honda, Yoshida, et. al. "A Theoretical Basis of > Communication-Centred Concurrent Programming", > > http://lists.w3.org/Archives/Public/public-ws-chor/2005Nov/att-0015/part1_Nov25.pdf > > (I tried all of them just now so they should work fine). > > Concering the global calculus and the formal grounding work for WS-CDL > the response I got was that more work on this is scheduled to finish for > the end of October this year (?). > > Concering the relationship between Pi-Calculus and WS-CDL I have done > some investigation in this as part of a seminar Gero also took part in. > I have been thinking about for while now to just mail it to this list so > as to contribute to the discussion and share my humble opinion on the > subject; so I shall do it now as the opportunity arises. It at best > might answer some of the questions Gero posed or at least might provided > hints to answers. Find the paper attached and please comment as you wish. > > Have a great day! > Paul > > Decker Gero wrote: > > >Hello everyone, > > > >I am currently working on my Master thesis (at SAP Research Brisbane) > about service choreographies und therefore I am very interested in the > activities of the CDL working group. > > > >I have a couple of questions regarding CDL: > > > >- It is claimed that CDL is based on pi-calculus which has proven to be > extremely expressive. Sequence, parallelism, choice and message exchanges > are enough to express common scenarios in the BPM domain. E.g. the > workflow patterns and the service interaction patterns could be fully > formalized. A trick in these formalizations is that each control flow > construct is encoded using a set of processes that exchange messages for > synchronization purposes. In CDL I do not see how I can do that. > > > >- Let us take a look at an example to clarify my question: Participant A > receives a number of messages via channel b. After three messages have been > received or a message has been received over channel c A continues by > sending a message over channel d. In pi-calculus I could write: > > A = (^h) (b(m1).b(m2).b(m3).'h.0 | c(m4).'h.0 | h.'d.0) > >^h is a private name, b() a message receipt and 'h a message send. I > introduced h to coordinate the two parallel processes. How does this work in > CDL? In BPEL there is the notion of control links which seems quite > powerful. > > > >- Another example would be (inspired by > http://bpt.hpi.uni-potsdam.de/twiki/pub/Public/PiHypeExample/PiHypeExample.pdf): > there are seven interactions a, b, c, d, e, f, g, h. a must happen before b > and e, b must happen before c, c must happen before d and f, d must happen > before h, e must happen before f, f must happen before g and g must happen > before h. Assuming a participant who is the sender in all these interactions > and for each interaction there is a channel with the name of the > interaction, the pi-calculus formalization for A would look as follows: > > A = (^x1,x2,x3,x4,x5,x6) ('a.('x1.0|'x2.0) | x1.'b.'c.('x3.0|'d.'x4.0) > | x2.'e.'x5.0 | x3.x5.'f.'g.'x6.0 | x4.x6.'h.0) > >How can I express this example in CDL? > > > >- How can I express scenarios where a participant A communicates with > participants B1, B2, B3, ... which are all of the same role but only bound > at runtime? E.g. like in the Single-transmission multilateral interaction > patterns ( > http://sky.fit.qut.edu.au/~dumas/ServiceInteractionPatterns/Multilateral..html > ). > > > >- Concerning parallel interactions: Is it allowed that two interactions > that do not have any preceding interactions happen in parallel? If so are > there any restrictions concerning correlation information or which > participant is involved in these initial interactions? > > > >- I read about some "global calculus". What is the current status? > Although I like pi-calculus I am also very interested in a calculus that > does not focus on interacting processes but rather communication from a > global perspective. A similar expressiveness like pi-calculus would be > desirable though. > > > >Best regards > >Gero > > > > > > > > > > > -- L.G. Meredith Partner Biosimilarity LLC 505 N 72nd St Seattle, WA 98103 +1 206.650.3740
Received on Tuesday, 20 June 2006 22:17:32 UTC