名义SOS：操作语义学的逻辑和结构方法的正式框架及其与演算的一致性证明

可在www.sciencedirect.com在线获取理论计算机科学电子笔记286（2012）103-116www.elsevier.com/locate/entcs标称SOSMatteo Ciminia MohamamdReza Mousavib Michel A.RenierscMurdoch J.Gabbayda计算机科学部，雷基亚大学，雷基亚，冰岛b荷兰埃因霍温理工大学计算机科学系c荷兰埃因霍温工业大学机械工程系d联合王国摘要Plotkin的结构操作语义（SOS）风格已经成为一个事实上的标准，为形式主义和过程演算提供操作语义。 在许多这样的形式主义和演算中，名称、变量和粘合剂是必不可少的成分。在本文中，我们提出了一个正式的框架，在SOS里处理人名该框架基于Gabbay和Pitts的名词逻辑，因此称为名义SOS。我们定义名义上的双相似性，双相似性概念的适应意识到约束力。 我们通过在名义SOS中制定早期的π演算和Abramsky对于这两个结石，我们建立了与原始结石的操作对应关系。此外，在π-演算的背景下，我们证明了名义双相似性与Sangiorgi的开放双相似性一致我们证明了名义双相似性与Abramsky的应用双相似性是一致的关键词：SOS，名义SOS，名义演算，λ-演算，π-演算。1引言为编程和规范语言开发形式语义例如，形式语义允许证明语言实现的正确性，并且是证明程序优化的有效性的先决条件。操作语义学（Operational Semantics）是一种广泛使用的定义计算机语言形式语义的方法，它将程序的执行表示为抽象机器的逐步结构操作语义学（SOS）由Gordon Plotkin在[24]中引入，在[25]中再版，作为定义操作语义的逻辑和结构方法。SOS规范的逻辑结构支持各种推理原则，这些原则可用于证明使用SOS给出语义的此外，SOS语言规范可以1571-0661 © 2012由Elsevier B. V.出版，CC BY-NC-ND许可下开放获取。doi：10.1016/j.entcs.2012.08.008104M. Cimini等人理论计算机科学电子笔记286（2012）103用于语言设计的快速原型设计，并提供计算机语言的实验实现。SOS已经成为定义操作语义的事实上的标准，并且大量的编程和可执行规范语言已经使用它被赋予了形式语义。近年来，在SOS的基本理论和实践方面已经进行了大量的工作，例如，[3，21]和[6，13，20]分别。许多编程语言和规范语言使用名称和绑定器的概念。例如，在π演算[18，19，29]中，名字是第一类对象，整个语言都建立在并发代理通过交换名字进行通信的思想近年来，在SOS中定义名义概念受到了一些关注，但SOS的元理论并不适用于这些新的框架。在本文中，我们提出了一个正式的框架来处理SOS中的名称，称为名义SOS，这是基于Gabbay，Pitts和Urban的名义技术[11，31]。在SOS的上下文中，最重要的程序等价概念是双相似性[22]。我们认为，这个概念，因为它是，是不令人满意的，我们适应bisimilarity，以更好地适应我们的上下文与粘合剂。我们称这种等价为名义双相似性。基本概念如α-转换和替换是大多数名词演算的基本部分。我们表明，这些概念可以自然地捕获名义SOS框架。此外，我们通过对两个最突出的名义演算的例子进行建模，即懒惰λ演算和早期π演算，来证明我们的框架的表现力。对于这两者，我们表明我们的规范分别与[2]和[29]的原始定义在操作上一致。此外，我们证明，在π演算的情况下，我们的名义双相似性的概念与著名的Sangiorgi [29，28]的开放双相似性相一致。最后，我们证明了在我们的懒惰λ-演算公式的上下文中的名义双相似性与Abramsky的应用双相似性一致。正文中省略了证明，读者可以在[8]中找到它们，以及对名义SOS的详细说明。这份文件扩展了Cimini论文[7]。论文的结构。本文的其余部分组织如下。在第2节中，我们定义了名义术语，在第3节中，我们定义了名义SOS的框架。我们在第4节中展示了如何在名义SOS中容纳α转换和不同类型的替代第5.1节致力于我们的π-演算的公式化，第5.2节讨论懒惰的λ-演算。在第6节中，我们讨论了相关的工作，第7节结束了论文。2名义价值下面的种类和名义签名的定义是从[31]中熟悉定义2.1（排序）排序由以下语法归纳定义：σ：：= 1 |δ|一|[A] σ |σ × σ，M. Cimini等人理论计算机科学电子笔记286（2012）103105一其中1是单位排序，δ是基排序，A是原子排序，[A] σ表示抽象排序，×表示配对。直觉上，[A]σ是一个排序，其元素是从排序A的对象到排序σ的对象的函数。 作为标准，对排序将关联到左侧，因此，σ1×σ2×σ3代表（σ1×σ2）×σ3。定义2.2（名义签名）A标称签名Σ是三重（Δ，A，F），其中(i) Δ是一组范围为δ的基本排序(ii) A是一组由A排列的原子种类，并且(iii) F是一组算子f（σ1×... ×σn）→δ，表示函数符号f的arity（σ1×σ n）。×σ n）→δ，其中n≥ 0。对于每个原子类A，我们固定一个可数无限原子集aA，bA，cA，dA...，对于每一种类型σ，我们假设变量符号的可数无限集合Vσxσ，yσ，zσ........我们有时只写f，a，b，c，d，n，m和x，y，z，保留arities和sort隐式的（但仍然存在）。我们假设所有这些符号集是成对不相交的。定义2.3（名义项）给定一个签名<$=（Δ，A，F），签名<$的名义项集用T（<$）表示，它定义如下，其中我们对排序为σ的项t写tσt：：= x σ|aA|（[aA] t σ）[A] σ|（f（σ1×... ×σn）→δ（t σ1，.，tσn））δ其中A ∈A，aA∈ A，x σ∈V σ，f∈F，arity（σ1××σ n）→δ.名词术语的下标控制排序，当它们与上下文无关或不重要时，我们倾向于省略它们我们称之为一种抽象。我们没有介绍任何方法来引入项对，因为我们只使用乘积排序来给转移关系排序（见第3节）。对于一个名义项t，下面的定义在本文的其余部分将是有用的在下文中，f和g是一元和二元函数符号。• A（t）代表出现在t中的原子的集合。例如，A（f（[a]g（a，b）={a，b}。• ba（t）是在t中存在子项[a]tJ的原子a的集合，即，t中抽象原子的集合。例如，ba（f（[a] g（a，b）={a}。• fa（t）是（t）中的原子a的集合，对于某项tJ，它们在t中的出现不在抽象[a]tJ的范围内。我们称fa（t）为t的自由原子的集合。 F或例如，fa（f（[a]g（a，b）={b}，以及fa（g（f（[a]a），a）={a}。• 当a∈fa（t）时，原子a在t中是新鲜的。我们还说，如果fa（t）= f，则项t是约束性的，即， 术语T不包含一定的自由原子。1[1]结合封闭术语对应于文献中通常称为封闭的术语。 例如在λ-演算的上下文λ-项λa，λb. （a b）是封闭的，因为它不包含自由变量，见[2，4]。我们采用不同的命名法，以避免与封闭术语的标准概念混淆。106M. Cimini等人理论计算机科学电子笔记286（2012）103JJ我们说一个名义项是封闭的，如果它不包含变量。否则就叫开放。例如，a和[a]f（b）是封闭项，但x和[a]y是开放项。注意a和[a]f（b）都不是绑定闭的。3标称SOS假设a是一个原子，t是某种项。我们把一个公式称为新鲜性断言。在下文中，我们给出一个推导系统，以便推导新鲜性断言。定义3.1（新鲜度推导规则）设f是一个名义签名，并让原子a和项t在签名f上。 我们说a #t是可导出的，当它可以使用以下规则导出时，其中a和b是不同的原子。a#ba #t1，.，a #t na #f（t1，...， t n）a#[a]ta#ta#[b]t这些推导规则与现有的工作[31，9]相似。我们现在准备定义名义过渡系统规范的概念其规则采用上面定义的新鲜度断言定义3.2（标称转换系统规范）标称转换系统规范（NTSS）是一个三元组（R，R，D），包括：(i) 名义签名;(ii) 一组（过渡）关系符号R。 对于每一个r ∈ R，我们都有一个（转换关系）元，它是一种形式σ × σ l× σJ。 我们可以称之为：σ是“ 转 移 的 源 的 排 序 ” ， σ是 “ 转 移 的 目 标 的 排 序 ” ， σ l 是 “ 转 移 的 标 签 的 排 序 ” 。(iii) 一组推导规则D（见下文）。给定NTSST，我们用A（T）表示T的签名的原子集合。对于元数为σ×σl×σJ的关系r∈R，如果σl是单位排序1，则我们说，R没有标签。如果σ也是单位排序，则r是谓词符号。我们可以悄悄地删除σl（和σJ），如果它们是单位排序。对于元数为σ×σl×σJ的关系r∈R，给出了一个正转移公式t→lrtj，其中t是σ的可能开项（我们称之为sou-c-e项），l是σ l的可能开项（我们称之为标号），TJ是σj的可能开项（我们称之为目标项）.对于相同的关系r，我们写作t~lr为负变换公式，其中t是σ，l是σl。转换公式是正转换公式或负转换公式。SOS，即，不包含变量的项M. Cimini等人理论计算机科学电子笔记286（2012）103107→~||定义3.3（推导规则）推导规则的形式如下：{tiritJi|i ∈ I}{tjLJRJ|j∈ J}{a k#tk| k ∈ K}哪里• I、J和K是索引集，t→lrtJ• {tiritJi | i ∈ I} is a set of positive transition formulae, called the positive规则的前提LJ• {t jrj | j ∈ J } is a set of negative transition formulae, called the negative规则的前提• {a k #t k|k ∈ K}是一组新鲜度断言，称为规则的新鲜度前提，以及• t→lrtj是一个正态变换公式，它包含了该定理的结论.我们将t、l和tJ分别称为规则的源、标签和目标。如果I，J和K为空，我们称一个推导规则为公理.当索引集合J为空时，导出规则为正。当NTSS的所有演绎规则都为正值时，NTSS为正值。积极的NTSS伴随着语义的自然概念，即，可证明的闭转换公式的集合;通过定义中给出的推导规则，新鲜度公式3.1.在本文中，我们将自己限制在积极的NTSSSOS中定义的程序之间最重要的等价概念是双相似性[17，22]。不幸的是，这种等效性在粘合剂的情况下并不令人满意。在[29]的第64-65页上，在π演算的背景下仔细解释了这一点，其中表明两个过程P=νz.xzx（y）且Q = νz。（xz νw.wy）是不同的，因为P可以执行一个转换x（y）而Q不能执行任何 →转换;原因是Q不能将其绑定变量改为y，因为y在Q中不是新的。因此，下面引入名义双相似性作为意识到结合的普通双相似性的适应。π演算理论中发生了什么x（z）调整了双相似性，并且仅匹配形式→的转换对于那些两项都是新的约束变量我们的双相似性概念以这种方式重新审视普通的双相似性在本文的其余部分，我们将涉及名义上的双相似性的重要概念定义3.4（名义双相似性）设T是NTSS。 名义双相似性Participatea∈ba（l），则若P→lPj，则存在Re，使得Q→lQJ且Pj<$QJ.→~LiLi→108M. Cimini等人理论计算机科学电子笔记286（2012）103a→z→−→a→z4取代和α-转化4.1替代转换替换和α-等价在定义具有粘合剂的演算的语义中起着关键作用。现在我们将展示如何在名义SOS的框架内以统一的方式术 语替 换原 子 通 常被 高阶 演 算所 采用 ， 例如 λ 演 算、 高阶 通 信系 统演 算（CHOCS）。[30]和高阶π演算[26]，仅举几例。给定一个名义签名，我们继续生成以下类型的演绎规则，a→Tt2目标是证明某些原子a和项t1，t2的形式t1-→t3的跃迁T3。这种类型的跃迁应该被理解为术语t2取代了原子a，项t1导致项t3。对于所有的原子a和函数符号f，我们有以下规则。不a−→z（a1Ts）a#x不（a2Ts）yTzx−→xJa#za#y不(abs1Ts）a−x→→z a[a]xy<$→z[a]xJ.y→TzJ不[a]x−→[a]x（abs2Ts）x i−→ xi |0

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