Re: Expressiveness of CDL

Paul,

As a postscript, i believe there is an very interesting issue behind the
issue you raise. The question arises: what is the specification of the
WS-CDL semantics? In particular, how is one to interpet WS-CDL
operationally? There are two different kinds of answers.

1. WS-CDL comes with its own (formal, machine-implementable) specification
of that operational interpretation.
2. WS-CDL inherits this operational interpretation via a mapping to
something that already has an operational interpretation.

In the first case the claim of 'based on' translates to a specific burden of
showing that the independent operational interpretation of WS-CDL programs
coincides with the operational interpretation of the \pi-interpretations of
those programs. In programming language semantics symbols, you need
something like

WS-CDL-Process1 ~ WS-CDL-Process2 <=> [| WS-CDL-Process1 |] ~ [|
WS-CDL-Process2 |]

where ~ on the left means the semantic equivalence of programs under the
independently specified WS-CDL operational interpretation and ~ on the right
means the semantic equivalence of programs in the \pi-calculus, i.e. some
form of bisimulation.

In the 2 case, WS-CDL has no independently specified operational
interpretation and gets it from its formal underpinning, so to speak. In
that case there is a very strong basis for the claim "based on". To the best
of my knowledge -- though i am no expert -- i believe that it is case 2 that
obtains. That is, i have not seen an independently specified operational
interpretation of WS-CDL. Rather, i think that WS-CDL looks to an
interpretation of WS-CDL programs into some variant of the \pi-calculus to
obtain an operational interpretation.

Best wishes,

--greg

On 6/20/06, L.G. Meredith <lgreg.meredith@gmail.com> wrote:
>
> 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
> >
> > <http://sky.fit.qut.edu.au/%7Edumas/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
>



-- 
L.G. Meredith
Partner
Biosimilarity LLC
505 N 72nd St
Seattle, WA 98103

+1 206.650.3740