具有无限字母表的反应式图灵机
Reactive Turing Machines with Infinite Alphabets
摘要：
反应图灵机（Reactive Turing machine，RTM）的概念是对具有交互作用的图灵机的正交扩展. RTM用于定义可执行转换系统的概念，就像图灵机用于定义自然数上的可计算函数的概念一样。RTM继承了图灵机所涉及的所有集合的有限性，因此，在单步的中，RTM只能从有限的数据集中传递元素。一些进程演算，如π演算，本质上依赖于无限的动作字母表，因此在这些演算中指定的转换系统是不可执行的。然而，仔细观察，π演算似乎并没有以不可计算的方式使用无限数据。在本文中，我们研究了几种放松有限性要求的方法。我们首先考虑RTM的一个变体，其中所有集合都允许是可数的，我们得到了无限RTM的概念。无限RTMs具有极强的表现力，因此我们很难将其用作表现力标准。然后，我们通过添加额外的限制来改进模型。因此，我们定义了一个原子RTM的概念。它是RTM的一个更受限制的变体，其中动作和数据符号的集合仍然允许是无限的。我们提出了一个名义上的可执行性的概念，基于RTMs与原子，并证明了每一个有效的原子转移系统是名义上可执行的。由此可见，在π演算中可定义的进程在名义上是可执行的。相反，在进程规约语言mCRL 2中，可以指定名义上不可执行的进程。因此，名义上的可执行性为进程演算提供了一个新的表达标准。
英文摘要：
The notion of Reactive Turing machine (RTM) was proposed as an orthogonal extension of Turing machines with interaction. RTMs are used to define the notion of executable transition system in the same way as Turing machines are used to define the notion of computable function on natural numbers. RTMs inherited finiteness of all sets involved from Turing machines, and as a consequence, in a single step, an RTM can only communicate elements from a finite set of data. Some process calculi, such as the pi-calculus, essentially depend on an infinite alphabet of actions, and hence it immediately follows that transition systems specified in these calculi are not executable. On closer inspection, however, the pi-calculus does not appear to use the infinite data in a non-computable manner. In this paper, we investigate several ways to relax the finiteness requirement. We start by considering a variant of RTMs in which all sets are allowed to be countable, and we get a notion of infinitary RTM. Infinitary RTMs are extremely expressive such that we can hardly use them as a expressiveness criterion. Then, we refine the model by adding extra restrictions. As a result, we define a notion of RTM with atoms. It is a more restricted variant of RTMs in which the sets of actions and data symbols are still allowed to be infinite. We propose a notion of of nominal executability based on RTMs with atoms, and show that every effective transition system with atoms is nominally executable. It will follow that processes definable in the pi-calculus are nominally executable. In contrast, in the process specification language mCRL2 it is possible to specify processes that are not nominally executable. Thus, nominal executability provides a new expressiveness criterion for process calculi.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
