RE: Yet Another Choreography Specification

Thanks that is very helpful. I have a few follow-on questions:

1) do you have a guideline in mapping processes, events, and actions in BPML
   to names in pi calculus; it seems to be quite arbitrary in your example
2) a similar question regarding parameters and properties to names in a
restriction
   prefix
3) don't mean to be picky about your word usage, but since we are dealing
with a
   formal system, imprecise words may lead to confusion.  in particular,  in
your
   description about P1 reducing to P2 in pi calculus, didn't you need to
first
   perform an apply followed by a communication in order for P1 to reduce to
P2?
4) your comment that the relationship between BPML and pi-calculus parallels
that
   between Java and lamda-calculus is very puzzling... did you mean to say
that
   anything computable in Java is also computable in lamda-calculus, and
vice versa,
   or you really did mean that any one java method can be reduced to a pure
lamda-calculus
   expression, which is functional, no side effects.

Thanks,
Joshua

>From: "Assaf Arkin" <arkin@intalio.com>
>To: <ed.peters@webMethods.com>, <abarros@dstc.edu.au>, <ChBussler@aol.com>,
<bill.flood@sybase.com>, <public->>ws-chor@w3.org>
>Cc: <W.M.P.v.d.Aalst@tm.tue.nl>, <m.dumas@qut.edu.au>,
<l.aldred@qut.edu.au>, <a.terhofstede@qut.edu.au>
>Date: Fri, 31 Jan 2003 10:18:34 -0800
>Message-ID: <IGEJLEPAJBPHKACOOKHNEECLDCAA.arkin@intalio.com>
>Subject: RE: Yet Another Choreography Specification


>> -----Original Message-----
>> From: public-ws-chor-request@w3.org
>> [mailto:public-ws-chor-request@w3.org]On Behalf Of Ed Peters
>> Sent: Friday, January 31, 2003 7:52 AM
>> To: 'Assaf Arkin'; abarros@dstc.edu.au; ChBussler@aol.com;
>> bill.flood@sybase.com; public-ws-chor@w3.org
>> Cc: W.M.P.v.d.Aalst@tm.tue.nl; m.dumas@qut.edu.au; l.aldred@qut.edu.au;
>> a.terhofstede@qut.edu.au
>> Subject: RE: Yet Another Choreography Specification
>>
>>
>>
>> Assaf,
>>
>> Thanks very much for these pointers.  I wonder, are there any
>> resources that
>> might bridge the gap between theoretical treatments of pi-calculus and
its
>> manifestation in or influence on the BPML specification?  I've
>> read numerous
>> papers on pi-calculus, and I've pored through the BPML spec many
>> times, and
>> I'm afraid I'm missing the connection.

>pi-calculus is a mathematical model. If you can reduce the process
>definition into its pi-calculus form you can use pi-calculus to analyze it.
>I'll illustrate by an example selected for its simplicity (taken from a
>document I am writing about the design of BPML).

>For the sake of this example I am using the 'pi' primitive (which refers to
>some internal operation, say an assign) and equality test introduced in
>later texts since they simplify the discussion. I am showing two systems
>talking to each other:

>P = P1 | P7

>P1 = v(b,c,x,y,z) a!(w,b,c).P2 P2=P3+P4 P3=b(x).0 P4=c(y).P5 P5=pi.P6
>P6=d!z.0

>P7 = v(w,v,x,y,z) !P8 P8=!a(w).P9 P9=pi.P10 P10=?v=0.P11 - P12 P11=b!x.0
>P12=c!y.P13 P13=d(z).0

>property b,c

>process P1
>  parameter w
>  property w,x,y,z
>  action operation=a output=w,b,c
>  choice P2
>    event P3
>      action operation=b input=x
>      empty
>    event P4
>      action operation=c input=y
>      . . . (determine z here)
>      action operation=d output=z
>             locate=d

>property d

>process P7
>  property v,w,x,y,z
>  event P8
>  action P8 operation=a input=w
>  ... determine v
>  switch
>    case P11
>      condition v=0
>      action operation=b output=x
>             locate=b
>    default P12
>      action operation=c output=y
>             locate=c
>      action operation=d input=z,d
>
>In workflow terms you would say that activity P2 is enabled when process P1
>starts, is executed after the action and is disabled after it is executed
>(since it cannot be repeated in this context).

>In pi-calculus you would reduce P1 to P2 by performing an action, then
>reduce P2 after receiving one of the two inputs. If you run a trace of the
>BPML process on the one hand and the pi-calculus process on the other hand,
>you will see how processes get reduced in the same way.

>The fact that both languages reduce in exactly the same way is what makes
>pi-calculus so appealing as a formal model.

... [deleted]

>You have to remember that the relationship between BPML and pi-calculus is
>the same as the relationship between Java and lambda-calculus. Every Java
>method can be reduced into a lambda-calculus form, and some of the
>similarity is very obvious (you can easily see that a method is a function,
>setting variables is the same). But where Java is a programming language
and
>uses higher level constructs, lambda-calculus is a concise mathematical
>language, the translation is not always trivial, but mathematically
>provable!

... [deleted]

>arkin


>>
>> Regards,
>> Ed
>>

Received on Monday, 3 February 2003 13:51:59 UTC