通过Isabelle的机器检查验证π演算中的互模拟等价代数公理化的合理性和完备性

理论计算机科学电子笔记192（2007）61-75www.elsevier.com/locate/entcs基于IsabelleJesper Bengtson和Joachim Parrow乌普萨拉大学瑞典乌普萨拉摘要我们使用交互式定理证明Isabelle来证明π演算中互模拟等价的代数公理化是合理且完备的。这是第一个完全由机器检查的证明虽然结果已经知道了一段时间的证明有部分需要仔细注意的细节，成为完全正式的。这并不是说这个结果曾经有过疑问;相反，我们的贡献在于证明完备性的方法，并获得证明是正确的绝对确定性，同时遵循原始证明的直觉推理路线公理化的完备性与微积分的许多变体有关，因此我们的方法具有超出这个单一结果的应用。我们建立在我们以前的e-实现一个框架的π演算在Isabelle使用名义数据类型包，并加强我们的主张，这个框架是非常适合代表理论的π演算，特别是在顺利治疗绑定名称。保留字：π演算，定理证明器，Isabelle，互模拟，公理化1引言我们给出了π演算中强后期双相似公理化的可靠性和完备性证明[8]。在交互式定理证明器Isabelle [9]中，使用标称数据类型包[1]对证明进行了机器检查。它代表了我们在Isabelle中形式化π演算的工作的继续[3]。完备性证明是同类证明中第一个正式验证的证明。原始的手工对应物只不过是一个草图，我们的机械验证证明在结构上非常接近它。因此，我们认为我们的贡献是三方面的：它明确了这个特殊证明的完全形式化所需要的东西，它打开了更容易检查类似证明的可能性，它支持我们的主张，即名义数据类型包中的Isabelle公式非常适合导出这种结果。像大多数类似的演算一样，π演算也配备了结构化操作语义（SOS），它根据代理可以执行的通信动作来定义代理的含义。此语义用于定义互模拟等价1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.08.01762J. Bengtson，J.Parrow/Electronic Notes in Theoretical Computer Science 192（2007）61不严格地说，是最大的等价物，这样无论一个主体能做什么，任何等价的主体都能模仿并保持等价。有几个变种，我们研究的最基本的，即晚强双相似性。但是，也有一种完全不同的方式来描述等价性：提出一组代数定律，并说两个代理人是等价的，当他们可以从定律和标准等式推理中证明这一点时。这种方式根本不使用SOS语义。在这里，我们使用[8]中的代数定律，并形式化了现在众所周知的结果，即它们精确地捕获了后期强双相似性。证明遵循标准结构，并被划分为健全性部分（即每个定律都是健全的，即，在所有情况下，右手侧与左手侧是双相似的）和完整性部分（说如果两个代理是双相似的，则存在来自代数定律的等价性证明在这些情况下，可靠性证明很简单，但详细写出来很繁琐，而完整性证明需要更多的独创性。我们将遵循的一种常见方法是将主体的子集定义为所谓的头范式。作为最外层的句法操作符，它们具有直接的交流能力，因此在某种意义上，最初的行为从句法结构中是显而易见的。然后，我们得出结论，首先表明，每个代理人有一个可证明的等价头范式，两个bisilimeric头范式是可证明的等价。这个特殊结果的原始手工证明可以追溯到π演算的第一次介绍[8]，它的草图在杂志上占据了大约一页（第这个结果没有争议，因为它是过程代数中完备公理化的许多类似结果之一，第一个是Hennessy和Milner在CCS [5]上的结果。这个证明的变体已经在微积分的变体中使用过，但从来没有完整地写下来。它包含了几个笼统的声明，需要相当多的注意细节，以核实正式。一个例子是，如果两个头范式具有可证明等价的和项，则使用和算子的交换性、结合性和幂等性的定律，可以证明两个主体是等价的（在下面的第4节中形式化为引理4.10最后，我们认为这是一个最广泛的结果，从一个机械化的定理证明有关的Meta理论的进程代数。我们超越了π演算[11，7，4，6]中其他根本不处理完备性的重要研究。今天还有其他几个来自Meta数学的机械化证明，例如Güodel的《复杂系统理论》[ 1 2 ]和《PoplMark挑战》[ 2 ]中的《系统分析》。2π演算及其完备公理化2.1语法我们假设读者熟悉π演算的基础。在本文中，我们使用一个标准的一元π演算没有递归和复制的变种。演算的语法定义在表1中。我们让P，Q等J. Bengtson，J.Parrow/Electronic Notes in Theoretical Computer Science 192（2007）6163代理P：：=0无ax.P输出前置a（x）.PInput Prefixτ。 P静音前置P+P总和P|P平行[x= y] P匹配[x/=y]PMismatch（νx）P限制表1π演算的语法而不是特工和a b...，z在名字上。在输入Prefix中，a（x）.P被称为在P中绑定x，x在P中的出现被称为绑定。相反，输出Prefix ax。P不约束X。这些Prefix被称为有主语a和宾语x，其中宾语在输出Prefix中被称为free，在输入Prefix中被称为bound。沉默的前缀τ既没有主语也没有宾语。限制算子（νx）P也将x约束在P中。自由名fn（P）是那些出现次数不受约束的名字，我们说x是新鲜的对于Ptome，如果x/f∈n（P），或者认为xfmen是所有n的自由值在讨论的背景下。类似地，绑定名称bn（P）是具有绑定出现的名称。替换是从名称到名称的函数。我们写{x/y}作为将y映射到x的替换，并且对于所有其他名称都是恒等式。 代理P{x/y}是P，其中所有自由名称x都被y替换，在需要避免被抓。记为多个主体P1+···+Pn的和卢恩i=1 Pi或者只是ΣjPj当n是不重要的或明显的，我们在这里允许的情况下n= 0时，总和意味着0的情况。2.2结构操作语义学α所涵盖的作用包括四类：(i) 内部动作τ。(ii) 类ax的（自由）输出动作。(iii)类型a（x）的输入动作。(iv) 受约束的输出作 用 为νx。64J. Bengtson，J.Parrow/Electronic Notes in Theoretical Computer Science 192（2007）61−→普雷菲克斯α.P−→Pα总和P+Q−→PJP−→PααJαJ匹配[x=x]P−α→PJP−→PαJ失配P−→P，x/=y[x/=y]P−→αJPpar P−α→PJ，bn（α）<$fn（Q）=<$P|Q −→ PJ|Qαa（x）JauJ网P|Q −→ P J{u/x}|QJP−→P，Q −→QτresP−→P，x/α∈（νx）P−α→（νx）PJαJaxJ开放P−→P，a/=x（νx）PaνxPJ−→a（x）J密切P−→P，Q−→Q阿武JP|Q −→（νu）（PJ{u/x}|QJ）τ表2操作语义。省略了sum、par、com和close的对称版本。代理商被识别为alpha等价，即选择绑定名称。我们写了x/∈α toomentt ttxdoesnt otoccurinα。表2中给出了结构化操作语义。可以看出，这是一个较晚的版本，没有结构一致性。2.3互模拟我们概括了强后期互模拟的定义。定义2.1互模拟是关于代理的对称二元关系R，满足：求PRQ和Pα 其中bn（α）是新鲜的，这意味着J. Bengtson，J.Parrow/Electronic Notes in Theoretical Computer Science 192（2007）6165−→(i) 如果α=a（x），则U：PJ{u/x}RQJ{u/x}(ii) 如果αi不是一个输入，则n<$QJ：Q−α→QJ<$PJRQJP和Q是互相似的，记作P<$Q，如果它们通过互模拟相关。2.4公理化表3和表4给出了强后期双相似性的公理。我们还隐含地使用等式推理的定律，即，代理之间的平等是自反的、对称的和传递的。请注意，替代性（一个代理人可以在任何表达式中替换一个相等的代理人）并不隐含，因为双相似性不是一个同余。相反，替代性质是由牛顿第一定律str 1-str 5通常是包含更多定律的结构同余的一部分。我们在这里只使用完全性证明所实际需要的结构定律。特别是我们将不需要任何结构性的法律对于parallel，因为它们的所有实例都可以从扩展定律导出。顺便说一下，str5定律可以用两个更简单的定律（νx）0=0和（νx）（νx）P=（νx）P来代替。我们说两个施动者P和Q是可证明等价的，记为P<$Q，如果它们的相等性可以由这些公理和等式推理建立。主要结果是将可证明等价性与双相似性联系起来的定理：定理2.2P<$Qi <$P<$Q这个定理自1980年代后期首次构思π演算时就已为人所知。它的有效性从来没有被怀疑，即使所有的证据提出，到目前为止，已经在几个点上使用了挥手。 为了给读者一个证明的概述，也为了欣赏这种证明的详细程度，在这里，我们引用了[10]中的部分证明。 健全，即的从右到左，其优点不过是（[8]中的原始证明只是更详细一点;它继续假设所有代数定律的互模拟关系，而没有实际证明这些关系是互模拟）。关于完备性部分，在第529页，我们读到，对于没有并行运算符的子演算：让一个agent的深度是它的prefixes的最大嵌套7号提案 使用公理每个代理P是可证明的等于一个头Σ类i α i的正规形（HNF）Pi没有更大的深度。证明是通过归纳的代理人的结构和所有的情况下是容易的。 如果P是Match或Mismatch，则应用m166J. Bengtson，J.Parrow/Electronic Notes in Theoretical Computer Science 192（2007）61str1P+0=Pstr2 P + Q = Q + Pstr3P+（Q+R）=（P+Q）+Rstr4（νx）（νy）P=（νy）（νx）Pstr5x/f∈n（P）→（νx）P=Pcongr1如果P = Q那么au. P = au。Qτ。 P = τ。QP + R = Q + RP |R = Q|RR|P = R|Q（νx）P=（νx）Qcongr 2如果P{y/x}=Q{y/x}，对所有y∈fn（P，Q，x），则a（x）.P=a（x）.Q同上P+P=Pm1[x=x]P=Pm2[x=y]P=0ifx/=ymm1[x/=x]P=0mm2[x/=y]P=Pifx/=yr1（νx）α 。 P=α 。（νx）Pifx/α∈r2（νx）α。 P= 0，如果x是α的主题r3（νx）（P+Q）=（νx）P+（νx）Q表3强后期双相似性的公理，除了平行。命题8如果P<$Q，则P=Q可由公理证明。证明是通过对P和Q的深度的归纳。根据命题7，我们可以假设P和Q是头标准形。基本情况P=Q=0是平凡的。 对于归纳步骤，我们证明，对于每个被加数在P有一个可证明的相等的被加数在Q，反之亦然。例如，取P中的J. Bengtson，J.Parrow/Electronic Notes in Theoretical Computer Science 192（2007）6167被加数a（x）.PJ。假设通过alpha转换，所有顶级输入操作都具有相同的68J. Bengtson，J.Parrow/Electronic Notes in Theoretical Computer Science 192（2007）61−→exp设P =iαi. Pi和Q =j βj。其中，bn（αi）<$fn（Q）= n且bn（βj）<$fn（P）=0，对于所有i，j。然后Σ ΣΣΣαi。 （Pi|Q）+ βj。（P|Qj）+ΣP|Q=τ。Rij我αicompβj其中关系αicompβj和Rij通过以下四种情况定义：(i) αi= a（x）和βj= au，其中Rij= Pi{u/x}|Qj，(ii) αi= a（x）和βj=（νu）au，此时Rij=（νu）（Pi{u/x}|Qj），(iii) 1的倒数(iv) 2的反面表4强双相似性的传统扩展律这里，αi和βj的范围超过前缀形式（输入，Output和Silent）以及绑定输出前缀（νu）au的组合。a（x）绑定对象x. 然后从PQ和P−→我们得到Qa（x） QJ，使得PJ{u/x}<$QJ{u/x}对于所有u。 通过归纳，它们也可以证明对所有的联合 所以a（x）。 QJ是Q 的 一个 和项，从congr2中我们得到它是可证明的等于a（x）.其他的情况都是类似的和简单的。因此，P的每个被加数都可证明等价于Q的一个被加数，因此，根据定理idem（和str），P可证明等价于Q。[8]中的原始证明使用了相同的思想，只是更详细一点（写出“其他情况”，而不是说它们“相似且更简单”）。这两种对深度的定义都是错误的。 在上面的引用中，3游戏名称：Isabelle：Soundness在我们早期的工作[3]中，我们已经在Isabelle中实现了语义和各种我们的结果包括替代性prop的形式证明-例如P→R→P|QR|Q和许多代数定律。我们的实现使用名义数据类型包，并有效地处理绑定名称，因此我们几乎不必担心代理或操作的alpha变体。唯一的例外是当绑定名称被显式地提到，并且关于它们的身份的论证是证明的一部分时。 一个例子是代数定律（νx）（νy）P=（νy）（νx）P，其中证明将在x = y的一种情况下分裂，而在x/=y 的情况下 则没有。在大多数情况下，implementation将保证绑定名称始终是适当的新名称，从而自动形式化J. Bengtson，J.Parrow/Electronic Notes in Theoretical Computer Science 192（2007）6169这是人工证明经常做的假设。我们将首先展示只包含Nil、Prefix、Sum、Match和Mismatch的子演算的可靠性和完备性。然后，我们将扩展我们的证明，以包括限制和平行。为了证明公理化的可靠性，我们必须证明所有可证明的等价过程对也是双相似的。在[3]中，我们证明了强互模拟被除了输入前缀之外的所有算子保持，并且所有结构全等项也是双相似的。这意味着表3中str和congr1的证明已经完成。其余公理的可靠性证明是微不足道的，除了congr2。引理3.1如果P{y/x}<$Q{y/x}对所有y∈fn（P，Q，x），则a（x）.P<$a（x）.Q通过互模拟的定义和案例分析证明x和y与引入的名称u冲突。Q我们可以证明我们的定理：定理3.2如果P<$Q，则P<$Q4完整性完备性证明的核心是头部范式，简称hnf。如果一个项是前缀过程的和，则它是头范式。 在Isabelle中，我们使用以下函数来确定一个术语是否在hnf中。4.1HNF的定义hnf（0）=Truehnf（α.P）=Truehnf（P+Q）=hnf（P）<$hnf（Q）<$P/=0<$Q/=0hnf=假我们将根据它们的被加数来推理hnfs。一个项的被加数是由+-运算符组成的它的前置子项的集合定义4.2被加数的定义和数（α.P）={α.P}summands（P+Q）=summands（P）summands（Q）summands={}在完备性证明的直观版本（上面引用的命题8）中，有一种诉诸于法则同原理的方法，以去除可证明等价的被加数的重复实例。为了正式地推理，我们想让被加数是项的等价类（对应于）的集合在伊莎贝尔，70J. Bengtson，J.Parrow/Electronic Notes in Theoretical Computer Science 192（2007）61为了更有效地通过唯一HNF或UHNF的概念来实现这一点，其中在集合中仅保留每个等价类的一个代表4.3UHNF的定义uhn f（P）=hn f（P）PJPJJ∈被加数s（P）. PJ/=PJJ−→<$（PJ<$PJJ）我们的主要证明将通过归纳法在被证明相等的项的深度上进行。直观地说，术语的深度是它可以进行的转换数量的上限。我们定义以下函数：4.4术语的深度深度（0）= 0深度（α.P）= 1 +深度（P）depth（[a=b]P）=depth（[a/=b]P）=depth（（νx）P）=depth（P）深度（P + Q）= max（深度（P），深度（Q））深度（P |Q）=深度（P）+深度（Q）对于完整性证明的其余部分，我们将主要使用UHNFs。因此，我们需要能够证明每一项都可以重写为可证明相等的UHNF。我们还必须确保生成的uhnfs没有比原始项更大的深度，否则这将破坏我们在主要证明中对深度的归纳。在下文中，我们提出了伊莎贝尔完成证明所需的引理序列，以及所涉及的证明策略的指示。首先，我们需要以下辅助引理：引理4.5若Q ∈ summands（P）且Q <$QJ，则P + QJ<$P。用归纳法证明了P.Q引理4.6如果uhnf（P）和uhnf（Q），则存在R使得uhnf（R），P + Q<$R且深度（R）≤深度（P + Q）。用归纳法证明了P.在基本情况下，引理4.5用于过滤掉可证明等于被加数（Q）中某项的项基本情况：P的形式为α.PJ。 如果Q=0，则将R设置为P，否则，如果aQJ∈summands（Q）s.t.根据引理4.5，QJ<$P则Q+P<$Q，因此将R设为Q，否则将R设为P+Q。归纳步骤：由于uhnf（P），只有P具有形式PJ+PJJ适用于：我们有uhnf（PJ+PJJ），因此有uhnf（PJ）和uhnf（PJJ）。从IH两次，我们得到一个QJ，其中uhnf（QJ），PJJ+Q<$QJ和深度（QJ）≤深度（PJJ+Q）。Q有了这些引理，我们可以证明：引理4.7对于每个P，存在一个Q s.t. uhnf（Q），P<$Q和深度（Q）≤J. Bengtson，J.Parrow/Electronic Notes in Theoretical Computer Science 192（2007）6171深度（P）。72J. Bengtson，J.Parrow/Electronic Notes in Theoretical Computer Science 192（2007）61−→−→用归纳法证明了P.在P具有以下形式的情况下，PJ+PJJ，使用引理4.6。Q为了证明双相似性和公理之间的对应关系，我们需要形成到转换系统的链接我们在总结中发现了这样的联系引理4.8若hnf（P）则Pα PJi <$α.PJ∈summands（P）.用归纳法证明了P.Q用被加数表示相等的直观方法是，如果两个主体的被加数之间有一个双射f，使得f（P）对所有P都≠P，则这两个主体可证明相等。显然，证明这一点的方法必须是通过对被加数的归纳，在那里我们需要下面的辅助引理：引理4.9如果uhnf（Q）和P ∈ summands（Q），则存在一个QJs. t。 P + QjQ和summands（Q j）= summands（Q）− {P} uhnf（Q j）。用归纳法证明了P. str2和str3用于将P拉到Q的顶层。直觉是，由于+-运算符是可交换的和结合的，人们总是可以将任何被加数拉到项的前面。由于该项是在uhnf上，我们知道不存在其他可证明相等的子项，因此余数的被加数将是去除拉取项后的原始项的被加数。Q现在我们可以证明以下引理：引理4.10如果 uhnf（P）和 uhnf（Q） 和 那里 存在 双射f：和数（P）→和数（Q）s.t. P f（P）则P Q。通过归纳法证明和数（P）。基本情况：被加数（P）={}因为f是双射，所以summands（Q）={}，并且因为uhnf（P）和uhnf（Q），所以P=0Q=0。因此，P Q是由的反射性决定的。归纳步骤：和数（P）={PJ}S从引理4.9我们得到一个PJJ，其中PJ+PJJ<$P，summands（PJJ）=summands（P）− {PJ}和uhnf（PJJ）。由于uhnf（PJJ），S=summands（P）。由于f（PJ）∈summands（Q），我们得到一个QJJ，其中f（PJ）+QJJ<$Q，summands（QJJ）=summands（Q）−{f（PJ）}和uhnf（QJJ）。由于f是一个双射且uhnf（PJJ）和uhnf（QJJ）存在一个双射函数FJ：summands（PJ）→summands（QJJ），则通过IHPJJ=QJJ.因此P<$PJ+PJJ<$f（PJJ）+QJJ<$Q。Q为了进行归纳，我们需要知道过程比其衍生物具有更大的深度引理4.11如果uhnf（P）和Pα PJ则depth（PJ）

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