Actors and Logical Analysis of Interactive Systems

Formalization in a logical theory can contribute to the foundational understanding of interactive systems in two ways. One is to provide language and principles for specification of and reasoning about such systems. The other is to better understand the distinction between sequential (turing equivalent) computation and interactive computation using techniques and results from recursion theory and proof theory. In this paper we briefly review the notion of interaction semantics for actor systems, and report on work in progress to formalize this interaction model. In particular we have shown that the set theoretic models of the formal interaction theory have greater recursion theoretic complexity than analogous models of theories of sequential computation, using a well-known result from recursion theory.