[pi4soa-model-analysis] A basic point.

[Kohei H. <ko...@dc...>]

The following is a brief observation on EEP and GVE. It is written in 
relationship
to the "memo" series in the forum. Since it in effect pertains to a 
general point,
I'll also post this mail in the mailing list.

Having both a global description language (CDL) and a good local, or 
end-point,
language (applied pi) is fundamental for deciding a proper realm of 
description
for communication-centred software behaviours. For example a good notion of
types arises through the interplay between these two descriptions. Even the
decision on primitives themselves, such as exceptions and timeout, comes 
from
how they arise in two calculi.

This comes from the following observations. If you start from only the 
end-point,
then you can write any details of local behaviour whose global description
may not make sense, at least as a protocol.  The same thing can be said 
the other
way round (though it may be better to start from well-formed global 
behaviour
for protocol description since at least you get a clear idea of what the 
protocol is:
as far as it is well-formed, hence EPPable, this would be a preferred 
way in most
practical contexts).

For me, the fundamental contribution of CDL to the principles of 
distributed
programming is that it defined, for the first time, a clear notion of 
(essentially
typed) global describability. We need to have this stipulation, a 
description
language,  separately from the local describability. This is subtle, 
since once
we have EPP/GVP, it seems one is enough and another unnecessary, in either
way. But the truth is we need both, even just for defining each's realm. 

Practically a global description language may as well be execution-language-
free since what we need is business protocols, not their execution details,
which can be realised by different languages (even over time). In this 
sense,
description may as well centre on global formalism. It is not without reason
that we often see the following description:

A --> T:  {A, B}_KA
T --> A:  {KAB, {KAB}_KB}_KA
A --> nB:  {KAB}_KB

who wishes to understand this protocol in local description? (except, of 
course,
the pi-calculus theorists, and for them with good reasons).

But the focal point of having these two formalisms lies in that, for 
stipulating
a sound notion of "good" interactional behaviours (say those of well-formed
business protocols),  we need both. Suppose you can write something locally
but not globally. It is not a good description! But suppose you can 
write some-
thing globally but not locally: it may not be easily executable. By careful
understanding of relationship between them, we can arrive at an effective
engineering of communication-centred applications.  The CDL-Pi dialogue
we have been having in the CDL WG is a unique and fruitful opportunity to
work torwards this goal.

I also note, for these reasons, there are still many subtleties to be 
uncovered
as to the relationship between two descriptive frameworks,  especially when
advanced constructs are present. They also interact non-trivially with 
types.
We hope our subsequent work can contribute to a further clarification of
these aspects.

Best wishes,

kohei