zbMATH — the first resource for mathematics

A reflective higher-order calculus. (English) Zbl 1276.68124
Goldin, Dina (ed.) et al., Proceedings of the workshop on the foundations of interactive computation (FInCo 2005), Edinburgh, UK, April 9, 2005. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 141, No. 5, 49-67 (2005).
Summary: The \(\pi\)-calculus is not a closed theory, but rather a theory dependent upon some theory of names. Taking an operational view, one may think of the \(\pi\)-calculus as a procedure that when handed a theory of names provides a theory of processes that communicate over those names. This openness of the theory has been exploited in \(\pi\)-calculus implementations, where ancillary mechanisms provide a means of interpreting of names, e.g., as tcp/ip ports. But, foundationally, one might ask if there is a closed theory of processes, i.e., one in which the theory of names arises from and is wholly determined by the theory of processes.{
}Here we present such a theory in the form of an asynchronous message-passing calculus built on a notion of quoting. Names are quoted processes, and as such represent the code of a process, a reification of the syntactic structure of the process as an object for process manipulation. Name- passing in this setting becomes a way of passing the code of a process as a message. In the presence of a dequote operation, turning the code of a process into a running instance, this machinery yields higher-order characteristics without the introduction of process variables.{
}As is standard with higher-order calculi, replication and/or recursion is no longer required as a primitive operation. Somewhat more interestingly, the introduction of a process constructor to dynamically convert a process into its code is essential to obtain computational completeness, and simultaneously supplants the function of the \(\nu\) operator. In fact, one may give a compositional encoding of the \(\nu\) operator into a calculus featuring dynamic quote as well as dequote.
For the entire collection see [Zbl 1273.68034].

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68Q60 Specification and verification (program logics, model checking, etc.)
03B70 Logic in computer science
Full Text: Link