Re: Formal semantics paper - from Marco Carbone et al

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> 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>> 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
> >)?
> >>
> >>     Best wishes,
> >>
> >>     --greg
> >>
> >>     On 8/1/06, *Steve Ross-Talbot* < steve@pi4tech.com
> >>     <mailto:steve@pi4tech.com>> wrote:
> >>
> >>
> >>         Is at:
> >>
> >>
> 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>
> >     home:   http://www.dcs.qmul.ac.uk/~carbonem
> >     <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