Semantics of non-methods in the object system

[cwgoes]

Thanks for this post. I think that this broad question is related to other discussions that we’ve had previously about action structure, most recently here, here, and perhaps even going back to the original proposal for actions.

The action concept and structure originally resulted from practical attempts to implement applications. At the time, we didn’t have a clear idea of what high-level behavior we wanted from the resource machine, much less the plan of compiling an object system to it. We now have a better understanding of the desired high-level semantics, and I think we can leverage this understanding to fix more precisely what interface we want the resource machine to have (which might, in my view, eventually necessitate some changes, perhaps e.g. to the “action” concept and structure).

In particular, when thinking about higher-level object systems, the relevant concepts in play are “objects” and “messages”. Object definitions in the higher-level semantics will then fix constraints as to what sets of objects and messages constitute valid transactions, where we can understand these sets as organized into (a) which objects were involved in the transaction and (b) which messages were sent and received by those objects (in order).

Let’s take the example from @Lukasz with two counters, the syntax of which I found a bit ambiguous at first. The semantics which I understand you to mean (per the invariants) is:

1. Query the value of the first counter, store it (value c1)
2. Query the value of the second counter (value c2)
3. Increment the first counter by the stored value of the second counter
4. Increment the second counter by the stored value of the first counter

Note that this is different from a program with the more sequential semantics which I think the current syntax loosely implies:

1. Query the value of the second counter
2. Increment the first counter by that value
3. Query the value of the first counter
4. Increment the second counter by that value

In this latter semantics, the second counter would be incremented by its own original value plus the value of the first counter, since the first counter is modified before we query it.

I would suggest a syntax for your desired semantics that looks a bit more like:

mutualIncrement (c1 : Counter) (c2 : Counter) := 
  v1 := value c1;
  v2 := value c2;
  c1.incrementBy(v2);
  c2.incrementBy(v1);

Or, alternatively, explicitly discard the new objects so that it’s clear that the second query queries the old version:

mutualIncrement (c1 : Counter) (c2 : Counter) := 
  _ := c1.incrementBy(value c2);
  _ := c2.incrementBy(value c1);

That slight nit aside, I would illustrate this program in diagram form as:

Here we have a “ProgramObject” (the implict context of the code snippet) which:

1. Queries the value of the first counter (“getValue”)
2. Queries the value of the second counter (“getValue”)
3. Receives the value “4” from the first counter (“value(4)”)
4. Receives the value “3” from the second counter (“value(3)”)
5. Increments the first counter by “3” (“incrementBy(3)”)
6. Increments the second counter by “4” (“incrementBy(4)”)

Now, let’s generalize this to use variables instead of specific values:

There are two free variables here (just the actual values of the counters in question). Supposing that we just had sets of objects and messages, what would we need to check in order to ensure that a transaction is valid (matches this pattern)? In general, just that:

1. The messages sent and received by each object are correct method calls and responses.
2. The messages sent and received by different objects correspond to one another.

In general, the former checks are non-linear – we don’t really care what happens to data “inside an object” – while the latter checks are linear – messages must be sent and received exactly once.

Unfortunately I’m running out of time to write, so I’ll leave this here for now, and hopefully continue tomorrow – but in the meantime curious if this provides anything useful.