Re: Formal semantics paper - from Marco Carbone et al

Hi Greg

Just to respond to your last point, I think there is definitely a place 
for both 'full blown choreographies' representing a global view of a set 
of interacting services, as well as a description of the specific 
behavior associated with a service. They have different roles to play.

The global model provides a design approach to enable the 
responsibilities of each service to be understood with respect to a 
particular business process. This global model can then be used to 
derive the behavior of a new service, or ensure that existing legacy 
services conform to the required behavior (using the service's 
observable behavior description).

Similarly, as you have described, if a service has its own endpoint 
behavior description, then it would be possible to do a behavioral 
equivalence lookup within a service registry. However, the required 
service behavior could be derived from the choreography.

At the moment Marco and Kohei's type system addresses both of these 
aspects, it is only WS-CDL that is lacking an endpoint representation - 
which as you have pointed out would ideally be a simple extension to 
WSDL. But that was not within the charter of the working group.

However, this is one area where potentially abstract BPEL may provide a 
solution, but that does not preclude other more compact notations being 
associated with the WSDL in the future.

Regards
Gary


L.G. Meredith wrote:
> Kohei,
>
> Many thanks for the edifying remarks. i hope you will allow me to 
> probe on a related front.
>
> Suppose we took a different approach to the architecture of WS-CDL in 
> which what is published is something like (collections of) Kobayashi's 
> usages, (an appropriately XML-ified version of) which could be seen as 
> a simple and direct extension of WSDL, leaving more detailed 
> descriptions of service logic (in which resides potentially 
> proprietary business value) behind the firewall, so to speak.
>
> i emphasize publish in this context because i want to call attention 
> to what's of general public interest in a service description. i argue 
> that the primary function of a public service description is search. i 
> submit that in a world where SOA is the norm there will be billions of 
> services, and a service consumer will need to find services that
>
>     * do what they need them to do (a semantic question)
>     * do it in a way that is compatible with their own needs and
>       practices
>
> Further, i argue that the former is far more important than the 
> latter. Consider the case where there is only one provider. The 
> consumer will adapt to any incompatibility. (Note that just because 
> there is only one such provider does not alleviate the search burden. 
> The consumer may not know of the provider, even when there is only one.)
>
> i want to argue that a great deal of semantic information can be 
> gleaned from information about behavior. i can provide some 
> interesting and illustrative examples, if you want them. One question, 
> however, is how much information needs to public to help the consumer 
> address their needs, and what needs to remain behind the firewall to 
> protect hard won business value?
>
> Now, to bring this line of reasoning back to my question above. Does 
> the market need a standard to capture full-blown choreographies? Or, 
> is there another niche that is likely to see better adoption? For 
> example, consider a small extension to WSDL, like Kobayashi's usages, 
> which can -- in Marco's words more powerfully and more generally -- 
> ensure both compatibility issues (like eliminating deadlock) and 
> increase the information available by which to conduct semantic-based 
> search one.
>
> Best wishes,
>
> --greg
>
> On 8/2/06, *Kohei Honda* <kohei@dcs.qmul.ac.uk 
> <mailto:kohei@dcs.qmul.ac.uk>> wrote:
>
>     Hi Greg,
>
>     It is great to get reactions so quickly.
>
>     L.G. Meredith wrote:
>     > Marco, Kohei,
>     >
>     > Thanks for clarifying. i was refering to the EPP theorem on page 85,
>     > which i took as the central result of the work. Sorry, if i was
>     a bit
>     > eliptical. My thought was that the end point calculus is actually a
>     > type system and end point projection was like the calculation of a
>     > kind of minimal type. Then, you can see the EPP theorem in the
>     light
>     > of subject reduction.
>
>     I may rather say that the global calculus and the end point
>     calculus are
>     two different description
>     languages, each with its own typing system, with respective notions of
>     minimum typing.
>
>     The type structures are common, but the way descriptions are typed are
>     quite different.
>
>     The idea is to project each "well-formd" global description to a
>     collection of endpoint processes,
>     which are the code for the participants involved.
>
>     What the EPP theorem asks is:
>
>         Do these projected participants interact following a scenario
>     (choreography) which the
>         original global description has laid out?
>
>     It turns out that, if a global description satisfies certain
>     well-structuredness, or "healthiness conditions",
>     then
>
>     (1) there is a very simple endpoint projection, and
>     (2) the correspondence in behaviour is as exact as can be.
>
>     There are three well-structuredness conditions we have identified.  We
>     believe they offer a natural
>     way to do a well-structured global description.
>
>     I will post a brief discussion on the engineering meaning of this
>     result, but for the time being let us
>     say the EPP theorem offers a way to relate the global description
>     languages and the process calculi.
>     The latter gives rigorous theories of behaviours, their properties
>     and
>     composition, while the former
>     offers a useful engineering medium.
>     >
>     > i know that you have a separate notion of typing laid out in the
>     > paper, but i tend to think -- much in the way Kohei laid out -- of
>     > towers of typing of increasing strength. Abramsky gives a good
>     example
>     > of such in his Marktoberdorff lecture with Simon Gay and Raja
>     > Nagaranjan on types for concurrency.
>
>     On this point I firmly agree: types and various analyses including
>     process/program logics are great toos
>     especially when we know how to integrate them consistently.
>
>
>     >
>     > That said, i was trying to draw an analogy between the EPP and
>     > Kobayashi's usages. More specifically, in my mind there is
>     connection
>     > between the fact that EPP is a function and Kobayashi has a type
>     > inference algorithm -- apart from the practical implication that the
>     > programmer doesn't have to write the type.
>
>     So the EPP theorem is not so much about type discipline or program
>     analysis but rather about a basic way
>     to relate two distinct ways of describing interactions. It is like the
>     result on encoding of some calculi into
>     the pi-calculus, saying the encoding fully respects the original
>     dynamics, under certain conditions.
>
>     These "under certain conditions" are the well-structuredness
>     (healthiness) conditions.
>
>     I will discuss on the general picture further in my coming post.
>
>     Best wishes,
>
>     kohei
>
>
>
>     >
>     > Best wishes,
>     >
>     > --greg
>     >
>     > On 8/2/06, *Marco Carbone* <carbonem@dcs.qmul.ac.uk
>     <mailto:carbonem@dcs.qmul.ac.uk>
>     > <mailto: carbonem@dcs.qmul.ac.uk
>     <mailto:carbonem@dcs.qmul.ac.uk>>> wrote:
>     >
>     >>     This looks like a lot of work. i may be misreading, because i
>     >>     have only skimmed, but it looks as though the main theorem
>     is a
>     >>     subject reduction-like theorem in which the subject
>     reduction is
>     >>     simulation-style (ala Kobayashi's type systems) as opposed to a
>     >>     static subject reduction (ala Honda, et al's type systems).
>     Have
>     >>     you seen, therefore, Kobayashi's 2006 types for concurrency
>     paper (
>     >
>     >
>     >     Just to clarify, the paper has three main theorems:
>     >
>     >     1) Subject Reduction for the global calculus type system
>     (session
>     >     types) i.e. when the system evolves it is still well typed (
>     e.g.
>     >     I evolves to I' and I is well typed then also I' is well typed.
>     >
>     >     2) Subject Reduction for the end-point calculus (similar to
>     point 1)
>     >
>     >     3) EPP Theorem, i.e.
>     >     a) Type Preservation i.e. a well typed global description is
>     >     projected to a well typed global interaction.
>     >     b) Completeness i.e. if a global interaction I evolves to I'
>     then
>     >     its projection evolves to the "projection" of I' (EPP(I') )
>     >     c) Soundness i.e. if a projection EPP ( I ) evolves to N then I
>     >     can evolve to I' and the projection of I' is "similar" to N
>     >
>     >     1) and 2) guarantee that working with typed programs is safe
>     (you
>     >     never evolve to untyped i.e. unwanted things).
>     >
>     >     3) shows that given a global description (e.g. a WS-CDL
>     >     choreography), its end-point projection is good and respects
>     what
>     >     the programmer wanted to specify in the choreography.
>     >
>     >     Hope this clarifies the key points of the paper.
>     >
>     >     Best,
>     >     Marco
>     >
>     >     P.S.
>     >     I didn't read the paper you linked but I believe it is related
>     >     with another of his works i.e. having CCS processes as types.
>     >     Session types are related to this but Kobayashi's are much more
>     >     powerful and lose.
>     >
>     >
>     >
>     >
>     >>    
>     http://www.kb.ecei.tohoku.ac.jp/~koba/papers/concur2006-full.pdf
>     <http://www.kb.ecei.tohoku.ac.jp/%7Ekoba/papers/concur2006-full.pdf>
>     >>    
>     <http://www.kb.ecei.tohoku.ac.jp/%7Ekoba/papers/concur2006-full.pdf>)?
>     >>
>     >>     Best wishes,
>     >>
>     >>     --greg
>     >>
>     >>     On 8/1/06, *Steve Ross-Talbot* < steve@pi4tech.com
>     <mailto:steve@pi4tech.com>
>     >>     <mailto:steve@pi4tech.com <mailto:steve@pi4tech.com>>> wrote:
>     >>
>     >>
>     >>         Is at:
>     >>
>     >>        
>     http://lists.w3.org/Archives/Public/www-archive/2006Aug/att-0000/
>     <http://lists.w3.org/Archives/Public/www-archive/2006Aug/att-0000/>
>     >>         workingNote.pdf
>     >>
>     >>         Please read and comment as soon as possible.
>     >>
>     >>         Cheers
>     >>
>     >>         Steve T
>     >>
>     >>
>     >>
>     >>
>     >>     --
>     >>     L.G. Meredith
>     >>     Partner
>     >>     Biosimilarity LLC
>     >>     505 N 72nd St
>     >>     Seattle, WA 98103
>     >>
>     >>     +1 206.650.3740
>     >
>     >     ---------------------------------------------------------
>     >     Marco Carbone
>     >
>     >     Dept. of Computer Science
>     >     Queen Mary University of London
>     >     Mile End Road
>     >     E1 4NS London
>     >     United Kingdom
>     >
>     >     Phone: +44 (0) 207 882 3659
>     >     Fax:      +44 (0) 208 980 6533
>     >     email:   carbonem@dcs.qmul.ac.uk
>     <mailto:carbonem@dcs.qmul.ac.uk> <mailto:carbonem@dcs.qmul.ac.uk
>     <mailto:carbonem@dcs.qmul.ac.uk>>
>     >     home:   http://www.dcs.qmul.ac.uk/~carbonem
>     <http://www.dcs.qmul.ac.uk/%7Ecarbonem>
>     >     < http://www.dcs.qmul.ac.uk/%7Ecarbonem>
>     >     ---------------------------------------------------------
>     >
>     >
>     >
>     >
>     > --
>     > 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

Received on Thursday, 3 August 2006 08:13:30 UTC