[cap-talk] Petnames versus E-order with ocaps

[David-Sarah Hopwood]

Charles Landau wrote:
> David-Sarah Hopwood wrote:
>> Karp, Alan H wrote:
>>> E-order guarantees the following property.  If Alice sends a
>>> message to Carol, and then Alice sends a message to Bob containing
>>> a reference to Carol,
>>
>> You mean "the same reference to Carol".
>>
>>> and Bob uses that reference to send a message to Carol, Carol will
>>> receive the message from Bob after she receives the message from
>>> Alice. (Did I get that right, MarkM?)
>> To avoid mistakes I suggest explicitly labelling the references, like
>> this:
>>
>> If alice sends a message to carol on reference C, and then alice
>> sends a message to bob containing C, and bob uses C to send a message
>> to carol, carol will receive the message from bob after she receives
>> the message from alice.
>>
>> (I prefer using lowercase names for subjects.)
> 
> Your usage of terms here leads to confusion. Permit me to recast this
> scenario in the precise terms used in MarkM's thesis. In that view, all
> references to an object are equivalent.
>
> If alice sends a message to bob containing C (and bob is in a different
> vat), then what bob receives is not C but a different reference C' to a
> different object with the different property that messages to C' are
> delivered (to carol) after certain other messages.

You're right; I stand corrected.

The statement above by Alan Karp did need a correction to ensure that
alice uses the same reference to carol in each of the messages alice
sends, though:

  If alice sends a message to carol on reference C, and then alice
  sends a message to bob containing C, which is received as C', and bob
  uses C' to send a message to carol, carol will receive the message
  from bob after it receives the message from alice.

> You can choose to view C and C' as facets of a composite object, but
> please do not confuse composite objects with objects.

That wasn't the mistake I was making. The mistake was to assume that
bob receives the same reference that was sent.

>>> A petname is a one-to-one mapping between an object reference and a
>>> name binding.
>> That's a bit imprecise. I use the following definitions:
>>
>> Petname: an identifier that is bound in a petnamespace.
>>
>> Petnamespace: a one-to-one mapping between petnames and subjects.
>>
>> Petname binding: a binding in a petnamespace -- that is, an ordered
>> pair (petname, subject).
>>
>> Note that the mapping is not to a reference, it is to a subject.
> 
> In MarkM's terms, there is a one-to-one relation between references and
> objects (aka subjects), so it makes just as much sense to say the
> mapping is to a reference.

No, since subjects are composites. All references to a given subject,
regardless of their position in the message ordering, are to the same
composite, and should map back to the same petname (for usability
reasons, as David Wagner pointed out).

>>> If Bob has a reference to Carol that he calls foo, a reference to 
>>> Carol that Bob receives from Alice will also be denoted foo.
> 
> No, because bob receives a different reference from alice.
> 
>> If "foo" is the petname for carol in a given petnamespace, then any
>> reference to carol will map back to "foo". I don't think this is a
>> problem, since there is no suggestion that petnames should replace
>> lambda names as the only way to denote references.
> 
> I think we are all operating with different notions of the hypothetical 
> petname system.

Indeed; that's why I specified that in the notion I'm operating with,
a petnamespace maps between petnames and subjects.

-- 
David-Sarah Hopwood ⚥