交互系统逻辑分析：演员与计算理论

理论计算机科学电子笔记141（2005）115-133www.elsevier.com/locate/entcs参与者与交互系统的逻辑分析伊恩·A梅森1，2新英格兰Armidale，NSW 2351，Australia卡罗琳湖Talcott3计算机科学实验室Menlo Park，CA 94025，美国摘要逻辑理论中的形式化可以通过两种方式对交互系统的基本理解做出贡献。一个是提供语言和原则来规范和推理这些系统。另一个是更好地理解顺序（图灵等价）计算和交互式计算之间的区别，使用递归理论和证明理论的技术和结果。在本文中，我们简要回顾了演员系统的交互语义的概念，并报告正在进行的工作，以形式化这个交互模型。特别是，我们已经表明，集理论模型的正式互动理论具有更大的递归理论的复杂性比类似的模型的理论顺序计算，使用一个众所周知的结果从递归理论。关键词：演员，交互语义，费费曼理论，递归理论。[1]作者感谢Michael Beeson提供了有益的讨论，感谢匿名评论者提供了有益的批评。这项工作得到了NSF资助CCR- 023446的部分支持。2 电子邮件地址：iam@turing.une.edu.au3 电子邮件地址：clt@cs.stanford.edu1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.05.019116I.A. Mason，C.L.Talcott/Electronic Notes in Theoretical Computer Science 141（2005）1151引言交互式计算基础的一个重要挑战是为交互式系统的规范和推理提供基础，甚至最终导致设计、实现和部署此类系统的原则性方法。一个基金会应该识别用于规范化的原语另一个挑战是更好地理解交互式计算和图灵机或lambda演算意义上的可计算性之间的区别。直觉上似乎很清楚，交互式计算不等同于图灵计算。问题是如何使这种直觉更加精确。传统上，可计算性的概念与一阶逻辑和其他逻辑片段的复杂性密切相关。 我们建议，开始理解顺序（图灵等价）计算和交互式计算之间的区别的一种方法是理解形式化表示交互式计算模型所需的逻辑的能力。为了更深入地探讨这个想法，我们研究了一个形式化，目前正在开发的，演员系统的交互语义。需要说明的是，我们并不是在提出一种新的交互式计算模型，而是在分析现有模型与顺序计算相比的表达能力。为了设置上下文，在第2节中，我们简要回顾了我们在动作语义方面的一些工作，这些工作导致了交互语义的概念。 第三节在Feferman的构造性数学形式化理论的基础上，简要总结了我们在顺序计算形式化理论方面的工作序贯计算理论对输入输出关系及其性质进行了形式化和推理。这些理论具有自然的、术语生成的、递归可重复的模型，这些模型捕获了预期的语义。例如，Feferman全函数空间Nat →Nat的被解释为总递归函数，而相应的部分递归函数函数空间中的部分递归函数。相反，交互式计算的理论必须形式化系统可能与其环境的交互，其中对环境中实体的行为一无所知。在第4节中，我们表明，递归可重复的模型是不足以捕捉预期的交互语义的演员系统使用一个众所周知的结果，从递归理论。I.A. Mason，C.L.Talcott/Electronic Notes in Theoretical Computer Science 141（2005）1151172行动者语义Actor模型[13，12，2，3]是一种基于独立计算代理概念的分布式计算模型，称为Actor，仅通过消息传递进行交互。一个参与者可以创建其他参与者;发送和接收消息;修改自己的本地状态。一个参与者只能通过向其他参与者发送消息来查看他们的本地状态，并且它只能向它的参与者发送消息--要么是在创建时被赋予名称的参与者，要么是它在消息中收到的名称，要么是它创建的参与者的名称。Actor语义只允许公平的计算，在最简单的情况下，这意味着可靠的消息传递。2.1传统角色语义传统角色语义学的核心概念是事件的偏序（事件是消息接收），熟人定律（谁可以认识谁）和计算的公平性。事件图[11，6]描述了参与者系统的可能计算，其基本属性被捕获。在下文中，我们将使用工作量很大的Ticker参与者来说明概念。一个Ticker actor，t，有自己完整的时间n概念，并响应两种类型的消息：一个tick请求和一个time请求。Ticker处理请求如下：• 一旦接收到滴答消息（tagick），Ticker就递增n，并向其自身发送新的滴答消息。• 在接收到来自参与者c的时间请求时（tatime@c），c消息回复（n），其中n是其当前时间概念图1显示了一个可能的Ticker计算的事件图，其中Tickert与某个外部参与者c交互。我们可以说和/或证明什么关于一个股票？• 每次请求tatime@c得到一个回复careply（n）为某个数字n.• 如果总是有另一个时间请求，那么对于任何n都有一个应答CA应答（nJ），其中n nJ是所发送的消息中的。如果不对事件施加一些额外的因果关系约束，就不能说太多其他的东西。118I.A. Mason，C.L.Talcott/Electronic Notes in Theoretical Computer Science 141（2005）115不、、、e1：ta时间@c\\/\/e0：tatick/升\\\e ：tatime@c\ \\）e：caO1回复（1）3\\//L/\e2：打勾\\\\\（d）e：caO3回复（2）Fig. 1. Ticker事件图。 垂直线t是自动收报机参与者t的本地时间线。 该图说明了：到达顺序（进入箭头）在t-e0

下载后可阅读完整内容，剩余1页未读，立即下载