Physical Indeterminacy in Digital Computation

The Actor Model moved the foundations of digital computing beyond the work of Alan Turing and Alonzo Church, who developed equivalent models of computation based on the concept of an algorithm, which by definition is provided an input from which it is to compute a value without external interaction. After physical computers were constructed, they soon diverged from computing only algorithms meaning that the Church/Turing theory of computation no longer applied to computation in practice because computer systems are highly interactive as they compute with incremental new input affecting future computation. The divergence inspired development of the Actor Model in 1972 to characterize all digital computation. There are simple digital computations that cannot be performed by a nondeterministic Turing Machine. The Actor Model has been axiomatized up to a unique isomorphism thereby removing all ambiguity from the most fundamental theory of digital computation. As part of the axiomatization, Actor theory has an induction axiom for computation events that is suitable for proving all kinds of properties (including specifications) for Actor systems. Event induction is much more powerful and practical than the methods developed by Turing [1949], Hoare [1969], and Lamport [2018] because it can express many more properties and because proofs are more intuitive. Concepts of the Actor Model have been deployed at scale at Ericsson, Erlang Solutions, Lightbend, Microsoft, PayPal, Twitter, and many other companies. Actors are being incorporated into the foundations for many-core intelligent systems that will be the foundation for the future of computing.

Strong types for the Actor model overturned an assumption beginning with Euclid that has persisted for millennia including Hilbert, Gödel, Church, Turing, and von Neumann. The assumption was that the theorems of a theory must be algorithmically enumerable by beginning with axioms and applying rules of inference. However, in order to characterize computation up to a unique isomorphism, it was necessary to develop an event induction axiom with uncountable instances. Because there are uncountable instances of the event induction axiom, it cannot possibly be the case that theorems of Actor theory are algorithmically enumerable because, of course, each axiom instance is a theorem of the theory. However, the theory of Actors is nevertheless effective because proof checking is algorithmically decidable. Consequently the foundational theory of digital computation is algorithmically inexhaustible. Furthermore, if a mathematical theory of digital computation is consistent, then the theory must be inexhaustible.

Strong types for the Actor model also exposed inadequacies in Gödel’s proof of the incompleteness (i.e. inferential undecidability) theorem using his proposition I’mUnprovable. Using strong types, the construction of I'mUnprovable is blocked because the mapping Ψ↦⊬Ψ has no fixed point because ⊬Ψ has order one greater than the order of Ψ since Ψ is a propositional variable. Consequently, some other way had to be found to prove inferential undecidability without using Gödel’s proposition I'mUnprovable. A complication is that theorems of strongly-typed theories of computation are not computationally enumerable, as mentioned above. The complication was overcome using special cases of the induction axioms to prove inferential undecidabilty.