Re: Alternative language versioning formalism

I've looked over your formalism and it looks... formal...  The question is
what to do with the proposed text and the finding.

Is your idea that most of your text goes into a section of the
compatibility-strategies document?

We certainly should spend some time talking about this at the f2f.

Stuart, can you add this as reading for the f2f versioning section?

Cheers,
Dave

On Mon, Jun 16, 2008 at 11:13 AM, Jonathan Rees <jar@creativecommons.org>wrote:

>
>
>
> On Jun 5, 2008, at 3:49 AM, Marc de Graauw wrote:
>
>> Hi Jonathan,
>>
>> A general difference is your model does not include receiver state; that
>> is,
>> given a message m, the receiver action a is determined by m and the
>> function
>> R. This is a bit too coarse for real messaging systems; for instance
>> messaging systems typically include a unique message id, so accepting a
>> message m and rejecting (or ignoring) the same message m if it has been
>> resent later is desired behaviour.
>>
>
> I did not think this was a particularly interesting or problematic part of
> the framework and felt it would unnecessarily complicate the presentation.
> Personally the way I would handle it is with the method used in the
> Scott/Strachey denotational semantics framework, which is to say that the
> "actions" are functions of the state or from state to modified state. But
> unless you are going after some particular theorem, going in this direction
> is an example of what I call "diminishing returns" or overformalization.
>
>  Another difference is our approach to a new message m', undefined in v1 of
>> the language. In my approach the receiver transforms m' to a known message
>> m
>> (possibly through ignoring unknown content) and will exhibit the behaviour
>> associated with m, in your approach you define an action by 'adequate
>> defaulting', i.e. providing a default action for any unknown message in
>> v1.
>> I think your approach may be more fruitful here. I may steal this idea and
>> incorporate it into my own formalism to see how this works out.
>>
>> Both approaches probably suffer from their dependance on behaviour/action
>> -
>> in real messaging systems, a lot of message do not lead to a perceivable
>> action, but to a database update, possibly but not necessarily affecting
>> future actions. (I.e. store a new customer address, which may or may not
>> be
>> used later.) This is one comment David Orchard gave me - what's the
>> behaviour of a name language message? I think this could be handled by
>> defining some receiver state as well, which influences the outcome of
>> future
>> actions, but it may also be a point where abstraction from the 'real
>> world'
>> is warranted.
>>
>
> I would say that a database update, or even a change of mind, is a kind of
> action. The approach ought to be that the action space is as rich as it
> needs to be to explain whatever you want to explain, and no richer. Leaving
> it completely unconstrained in the initial presentation allows for you to
> make it as rich or as spare as you like in a deeper analysis. This is the
> usual modularity trick that mathematicians and mathematical modelers pull.
>
>  Thanks anyway for this contribution, it is a insightful exercise to
>> compare
>> the two approaches.
>>
>
> I should say there are two things I was striving for that I found missing
> in David's and your analyses:
>
> 1. I wanted to make sure that every move in the analysis was forced, so
> that every condition was both necessary and sufficient - to make sure I
> didn't miss any possible degrees of freedom.
>
> 2. I wanted the central results to be theorems, not axioms - to say that to
> achieve extensibility it is necessary *and sufficient* to do such and such.
> Although the theorems end up being trivial, without this the whole
> presentation risks being (or sounding like) a jumble of arbitrary decrees.
>
> I'm not sure how I well I succeeded in these goals, but I think they are
> worthwhile in any modeling effort.
>
>>
>> Regards,
>>
>> Marc de Graauw
>>
>
> Best
> Jonathan
>
>