| Popis: |
[Church 1931] and [Turing 1936] 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, which inspired the development of the Actor Model in 1972 to characterize all digital computation. Indeterminate computation can be thousands of times faster than the parallel λ-calculus (cf. [Takahashi 1989]) or pure logic programs [Hewitt 1969]. This article presents metatheory for a universal theory of digital computation that is more general and powerful than Church/Turing computation [Church 1935, Turing 1936]. Meta[Actors] (meta theory of Actors) proves that theory Actors has the following properties: • The theory Actors is uniquely categorical, i.e., it characterizes Actors (including types) up to an unique isomorphism. • The theory Actors is model sound, i.e., every theorem of Actors of is true in the unique up to isomorphism model. • The unique up to isomorphism model has partial predicates and propositions because of indeterminacy. • Proof checking in the theory Actors is computationally decidable. • There are no “monsters” [Lakatos 1976] in models of the theory Actors such as the ones in 1st-order theories of computation in which there can be Zeno-like computations, which have an infinite number of computational steps between two steps. Consequently unlike 1st-order theories, the theory Actors is not subject to cyberattacks using “monsters” in models. • The theory Actors is algorithmically inexhaustible, i.e., it is impossible to computationally enumerate theorems of the theory thereby reinforcing the intuition behind [Franzen, 2004]. Contrary to [Church 1934], the conclusion in this article is to abandon the assumption that theorems of a theory must be computationally enumerable while retaining the requirement that proof checking must be computationally decidable. Thesis: Any digital system can be directly modeled and implemented using Actors. |
