Lambda the Ultimate

Plotkin's proof that a global state machine has bounded nondeterminism:

Now the set of initial segments of execution sequences
of a given nondeterministic program P,
starting from a given state, will form a tree. 
The branching points will correspond to the choice points in the program.  
Since there are always only finitely many alternatives at each choice point, 
the branching factor of the tree is always finite.  
That is, the tree is finitary. 
Now König's lemma says that if every branch of a finitary tree is finite, 
then so is the tree itself. 
In the present case this means that if every execution sequence of P terminates, 
then there are only finitely many execution sequences. 
So if an output set of P is infinite, 
it must contain a nonterminating computation.

Consequently, either
* The tree has an infinite path. ⇔ The tree is infinite. ⇔ It is possible that P does not halt.
If it is possible that P does not halt, then it is possible that that the set of outputs with which P halts is infinite.
or
* The tree does not have an infinite path. ⇔ The tree is finite. ⇔ P always halts.

If P always halts, then the tree is finite and the set of outputs with which P halts is finite.

What is unbounded non-determinism useful for?

I'm not even convinced my languages should be pervasively Turing complete.

Hoare was convinced that unbounded nondeterminism could not be implemented and so the semantics of CSP specified bounded nondeterminism.

[X :: Z!stop( )
   ||                                                                    
 Y :: guard: boolean; guard := true;
       *[guard→ Z!go( ); Z?guard]
   ||                                                                    
 Z :: n: integer; n:= 0; 
      continue: boolean; continue := true;
        *[
          X?stop( )→ continue := false;
                      Y!continue
              []        
          Y?go( )→ n := n+1;
                   Y!continue]]

According to Clinger [1981]:

 
this program illustrates global nondeterminism, 
since the nondeterminism arises from incomplete specification
of the timing of signals between the three processes X, Y, and Z. 
The repetitive guarded command in the definition of Z has two alternatives: 
either the stop message is accepted from X, 
in which case continue is set to false, 
or a go message is accepted from Y, 
in which case n is incremented and Y is sent the value of continue.
If Z ever accepts the stop message from X, 
then X terminates. 
Accepting the stop causes continue to be set to false, 
so after Y sends its next go message, 
Y will receive false as the value of its guard and will terminate.
When both X and Y have terminated, 
Z terminates because it no longer has live processes providing input. 

As the author of CSP points out, therefore, 
if the repetitive guarded command in the definition of Z were required to be fair, 
this program would have unbounded nondeterminism: 
it would be guaranteed to halt 
but there would be no bound on the final value of n. 
In actual fact, the repetitive guarded commands of CSP are not required to be fair, 
and so the program may not halt [Hoare 1978].
This fact may be confirmed by a tedious calculation 
using the semantics of CSP [Francez, Hoare, Lehmann, and de Roever 1979] or 
simply by noting that the semantics of CSP is based upon a conventional power domain and 
thus does not give rise to unbounded nondeterminism.

The upshot was that Hoare was convinced that unbounded nondeterminism is impossible to implement. That's why the semantics of CSP specified bounded nondeterminism. But Hoare knew that trouble was brewing in part because for several years proponents of the Actor Model had been beating the drum for unbounded nondeterminism. To address this problem, he suggested that implementations of CSP should be as close as possible to unbounded nondeterminism! But his suggestion was difficult to achieve because of the nature of communication in CSP using nondeterministic select statements (from nondeterministic state machines, e.g., [Dijkstra 1976]), which in the above program which takes the form [X?stop( ) → ... [] Y?go( ) → ...]. The structure of CSP was fundamentally at odds with guarantee of service.

Using the semantics for CSP, it was impossible to formally prove that a server actually provides service to multiple clients (as had been done previously in the Actor Model). That's why the semantics of CSP were reversed from bounded non-determinism [Hoare CSP 1978] to unbounded non-determinism [Hoare CSP 1985]. Bounded non-determinism was but a symptom of deeper underlying issues with nondeterministic transitions in communicating sequential processes (see [Knabe 1992]).

Computations are represented differently in State Machines and Actors:
1. State Machine: a computation can be represented as a global state that determines all information about the computation. It can be nondeterministic as to which will be the next global state, e.g., in simulations where the global state can transition nondeterministically to the next state as a global clock advances in time, e.g., Simula [Dahl and Nygaard 1967].
2. Actors: a computation can be represented as a configuration. Information about a configuration can be indeterminate. (For example, there can be messages in transit that will be delivered at some indefinite time.)

Perhaps I'm off the mark here, but it strikes me as peculiar that there is no mention of Carl Adam Petris dissertation "Kommunikation mit Automaten" or any other reference to Petri nets as a model of concurrent systems. Seems to me that the hypothesis that a global state machine (i.e. a model in which the state is assumed to be global and changes are also assumed to have a global effect as well as depending on the global state) is very similar to the Petris idea that global state when taken to extremes is physically impossible, hence the need for local state and local state changes. And if you are so inclined you can view state machines as just a special case of plain place/transition nets.

Hi Carl,

I've been thinking a lot about arbiters and the assumptions we tend to make about arbiters, and how it limits our design options.

Going forward, the speed of light will be our bottleneck. There will no longer be such things as liquid bottlebecks and 'elastic' clouds, because eventually the rubberband snaps.

I attempted to create a programming language based on patterns from control theory, such as Predictive Model Control, but I gave up because the bottleneck to implement many real scenarios is too severe due to physics of the real world; for example, to spin up a new slave server requires creating a copy, which also eats bandwidth and has real propagation delay. Propagation delay is the fundamental issue at the speed of light, as communication protocol design becomes THE dominating factor in system design. Further, most control laws have to be driven by 'human hints' rather than detecting periodicity in a system using characteristic functions such as those found in machine learning... or the system will be vulnerable to 'Black Swans'.

Awhile back, I asked you about exactly this problem, and your answer back then was 'Actor Model will get better'. Have I still stumped you?