Unbounded nondeterminism

Discussion of unbounded nondeterminism tends to get involved with discussions of fairness. The basic concept is that all computation paths must be "fair" in the sense that if the machine enters a state infinitely often, it must take every possible transition from that state. This amounts to requiring that the machine be guaranteed to service a request if it can, since an infinite sequence of states will only be allowed if there is no transition that leads to the request being serviced. Equivalently, every possible transition must occur eventually in an infinite computation, although it may take an unbounded amount of time for the transition to occur. This concept is to be distinguished from the local fairness of flipping a "fair" coin, by which it is understood that it is possible for the outcome to always be heads for any finite number of steps, although as the number of steps increases, this will almost surely not happen.

An example of the role of fair or unbounded nondeterminism in the merging of strings was given by William D. Clinger, in his 1981 thesis. He defined a "fair merge" of two strings to be a third string in which each character of each string must occur eventually. He then considered the set of all fair merges of two strings merge(S, T), assuming it to be a monotone function. Then he argued that merge(⊥,1^ω)⊆ merge(0,1^ω), where ⊥ is the empty stream. Now merge(⊥,1^ω) = {1^ω}, so it must be that 1^ω is an element of merge(0,1^ω), a contradiction. He concluded that:

It appears that a fair merge cannot be written as a nondeterministic data flow program operating on streams.

Edsger Dijkstra [1976] argued that it is impossible to implement systems with unbounded nondeterminism. For this reason, Tony Hoare [1978] suggested that "an efficient implementation should try to be reasonably fair."

Nondeterministic Turing machines have only bounded nondeterminism. Likewise sequential programs containing guarded commands as the only sources of nondeterminism have only bounded nondeterminism (Edsger Dijkstra [1976]). Briefly, choice nondeterminism is bounded. Gordon Plotkin gave a proof in his original 1976 paper on powerdomains:

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].

William Clinger [1981] provided the following analysis of the above proof by Plotkin:

This proof depends upon the premise that if every node x of a certain infinite branch can be reached by some computation c, then there exists a computation c that visits every node x on the branch. ... Clearly this premise follows not from logic but rather from the interpretation given to choice points. This premise fails for arrival nondeterminism [in the arrival of messages in the Actor model] because of finite delay [in the arrival of messages]. Though each node on an infinite branch must lie on a branch with a limit, the infinite branch need not itself have a limit. Thus the existence of an infinite branch does not necessarily imply a nonterminating computation.

Spaan et al. [1989] have argued that it is possible for an unboundedly nondeterministic program to solve the halting problem; their algorithm consists of two parts defined as follows:

The first part of the program requests a natural number from the second part; after receiving it, it will iterate the desired Turing machine for that many steps, and accept or reject according to whether the machine has yet halted.

The second part of the program nondeterministically chooses a natural number on request. The number is stored in a variable which is initialized to 0; then the program repeatedly chooses whether to increment the variable, or service the request. The fairness constraint requires that the request eventually be serviced, for otherwise there is an infinite loop in which only the "increment the variable" branch is ever taken.

Clearly, if the machine does halt, this algorithm has a path which accepts. If the machine does not halt, this algorithm will always reject, no matter what number the second part of the program returns.

Clinger and Carl Hewitt have developed a model (known as the Actor model) of concurrent computation with the property of unbounded nondeterminism built in [Clinger 1981; Hewitt 1985; Hewitt and Agha 1991; Hewitt 2006b]; this allows computations that cannot be implemented by Turing Machines, as seen above. However, these researchers emphasize that their model of concurrent computations cannot implement any functions that are outside the class of recursive functions defined by Church, Kleene, Turing, etc. (See Indeterminacy in concurrent computation.)

Hewitt [2006] justified his use of unbounded nondeterminism by arguing that there is no bound that can be placed on how long it takes a computational circuit called an arbiter to settle (see metastability in electronics). Arbiters are used in computers to deal with the circumstance that computer clocks operate asynchronously with input from outside, e.g.., keyboard input, disk access, network input, etc. So it could take an unbounded time for a message sent to a computer to be received and in the meantime the computer could traverse an unbounded number of states.

He further argued that Electronic mail enables unbounded nondeterminism since mail can be stored on servers indefinitely before being delivered, and that data links to servers on the Internet can likewise be out of service indefinitely. This gave rise to the Unbounded nondeterminism controversy.

Hewitt argued that issues in fairness derive in part from the global state point of view. The oldest models of computation (e.g.. Turing machines, Post productions, the lambda calculus, etc.) are based on mathematics that makes use of a global state to represent a computational step. Each computational step is from one global state of the computation to the next global state. The global state approach was continued in automata theory for finite state machines and push down stack machines including their nondeterministic versions. All of these models have the property of bounded nondeterminism: if a machine always halts when started in its initial state, then there is a bound on the number of states in which it can halt.

Hewitt argued that there is a fundamental difference between choices in global state nondeterminism and the arrival order indeterminacy (nondeterminism) of his Actor model. In global state nondeterminism, a "choice" is made for the "next" global state. In arrival order indeterminacy, arbitration locally decides each arrival order in an unbounded amount of time. While a local arbitration is proceeding, unbounded activity can take place elsewhere. There is no global state and consequently no "choice" to be made as to the "next" global state.

• Carl Hewitt, Peter Bishop and Richard Steiger. A Universal Modular Actor Formalism for Artificial Intelligence IJCAI 1973.
• Robin Milner. Processes: A Mathematical Model of Computing Agents in Logic Colloquium 1973.
• Carl Hewitt, et al. Actor Induction and Meta-evaluation Conference Record of ACM Symposium on Principles of Programming Languages, January 1974.
• Carl Hewitt, et al. Behavioral Semantics of Nonrecursive Control Structures Proceedings of Colloque sur la Programmation, April 1974.
• Irene Greif. Semantics of Communicating Parallel Professes MIT EECS Doctoral Dissertation. August 1975.
• Gordon D. Plotkin. A powerdomain construction SIAM Journal on Computing, 5:452-487, September 1976.
• Edsger Dijkstra. A Discipline of Programming Prentice Hall. 1976.
• Carl Hewitt and Henry Baker Actors and Continuous Functionals Proceeding of IFIP Working Conference on Formal Description of Programming Concepts. August 1–5, 1977.
• Gilles Kahn and David MacQueen. Coroutines and networks of parallel processes IFIP. 1977
• Henry Baker. Actor Systems for Real-Time Computation MIT EECS Doctoral Dissertation. January 1978.
• Michael Smyth. Power domains Journal of Computer and System Sciences. 1978.
• George Milne and Robin Milner. Concurrent processes and their syntax JACM. April, 1979.
• C. A. R. Hoare. Communicating Sequential Processes CACM. August, 1978.
• Nissim Francez, C. A. R. Hoare, Daniel Lehmann, and Willem de Roever. Semantics of nondeterminism, concurrency, and communication Journal of Computer and System Sciences. December 1979.
• Nancy Lynch and Michael Fischer. On describing the behavior of distributed systems in Semantics of Concurrent Computation. Springer-Verlag. 1979.
• Jerald Schwartz Denotational semantics of parallelism in Semantics of Concurrent Computation. Springer-Verlag. 1979.
• William Wadge. An extensional treatment of dataflow deadlock Semantics of Concurrent Computation. Springer-Verlag. 1979.
• Ralph-Johan Back. Semantics of Unbounded Nondeterminism ICALP 1980.
• David Park. On the semantics of fair parallelism Proceedings of the Winter School on Formal Software Specification. Springer-Verlarg. 1980.
• Dana Scott. What is Denotational Semantics? MIT Laboratory for Computer Science Distinguished Lecture Series. April 17, 1980.
• William D. Clinger, Foundations of Actor Semantics. MIT Mathematics Doctoral Dissertation, June 1981.
• William D. Clinger, Nondeterministic call by need is neither lazy nor by name Pages 226-234 in Symposium on LISP and Functional Programming. Pittsburgh, Penn., 1982.
• Stephen Brookes, Tony Hoare and Bill Roscoe A Theory of Communicating Sequential Processes JACM. July 1984.
• Carl Hewitt, The Challenge of Open Systems Byte Magazine. April 1985. Reprinted in The foundation of artificial intelligence---a sourcebook Cambridge University Press. 1990.
• Bill Roscoe. Unbounded nondeterminism in CSP in `Two papers on CSP', technical monograph PRG-67, Oxford University Computing Laboratory. July 1988.
• Carl Hewitt and Gul Agha Guarded Horn clause languages: are they deductive and Logical? International Conference on Fifth Generation Computer Systems, Ohmsha 1988. Tokyo. Also in Artificial Intelligence at MIT, Vol. 2. MIT Press 1991.
• A. W. Roscoe: The Theory and Practice of Concurrency, Prentice Hall, ISBN 0-13-674409-5.
• Edith Spaan, Leen Torenvliet and Peter van Emde Boas. Nondeterminism, Fairness and a Fundamental Analogy. EATCS bulletin, 37:186-193, 1989.
• David A. Schmidt, The Structure of Typed Programming Languages. MIT Press, Cambridge, Massachusetts, 1994.
• Butler, M. J. and Morgan, C. C. Action Systems, Unbounded Nondeterminism, and Infinite Traces Formal Aspect of Computing. 1995
• Thomas A. Sudkamp, Languages and Machines. 2nd Edition. Addison-Wesley, Reading, Mass., 1997.
• Luca Aceto and Andrew D. Gordon (editors). Algebraic Process Calculi: The First Twenty Five Years and Beyond' Process Algebra. Bertinoro, Forl`ı, Italy, August 1–5, 2005
• Stephen Brooke. Retracing CSP in Algebraic Process Calculi: The First Twenty Five Years and Beyond. August 2005.
• A. W. Roscoe: The Theory and Practice of Concurrency, Prentice Hall, ISBN 0-13-674409-5. Revised 2005.
• Carl Hewitt. The repeated demise of logic programming and why it will be reincarnated What Went Wrong and Why: Lessons from AI Research and Applications. Technical Report SS-06-08. AAAI Press. March 2006.
• Carl Hewitt, What is Commitment? Physical, Organizational, and Social COIN@AAMAS. April 27, 2006.
• Toby Ord. Hypercomputation: Computing more than the Turing machine can compute on arxiv.org.