PVS系统中基于操作的编程逻辑的评估

124理论计算机科学电子笔记42（2001）网址：http://www.elsevier.nl/locate/entcs/volume42.html19页PVS中的操作技术- 初步评价Jonathan M.福特2和伊恩A。Mason梅森1，3数学，统计，计算科学学院，U.N.E Armidale，NSW 2351澳大利亚摘要在本文中，我们提出了一个初步的分析，适用于使用PVS作为一个工具，开发操作语义和编程逻辑在一个半自动的方式。为此，我们提出了一个形式化的证明教会罗瑟定理的一个版本的调用值lambda演算的精神兰丁的ISWIM。证明是在PVS系统中开发的，并用作测试床或基准，用于评估该系统进行更复杂的操作参数的适用性。我们的方法是相对不寻常的，因为它是基于命名变量的方法，并集中在β规则的按值调用版本虽然在文献中有许多基于计算机的Church-Rosser定理的证明我们的方法的新颖之处在于：我们使用PVS系统，特别是它内置的抽象数据类型工具，来验证Church-Rosser定理的一个版本然而，这里报告的工作的主要目的是评估PVS作为一种工具，用于开发，最先进的，基于操作的编程逻辑，为现实的编程语言。1介绍在本文中，我们在Landin的ISWIM [9]的精神下，为按值调用lambda演算[23]的一个版本提供了Church-Rosser定理的形式化证明[4]证明是在PVS [2]系统中开发的，并用作一个测试台或基准，用于评估该系统在执行更复杂的操作参数时的适用性，例如使用1第二位作者得到了联合国教科文组织小额ARC赠款的部分支持8202 881 499.2电邮地址： jford@turing.une.edu.au3电子邮件地址：iam@turing.une.edu.au2000年1月由ElsevierScien ceB出版。 诉 操作访问和C CB Y-NC-N D链接。福德和梅森125上下文[11]，开发Feferman-Landin逻辑[15]或证明各种类型lambda演算的Curry-Howard同构定理，以及相应的逻辑[28]。我们的方法是相对不寻常的，因为它是基于命名变量的方法，并集中在β规则的按值调用版本。我们希望处理更复杂的β规则，是因为我们希望将这项工作扩展到更现实的编程语言。这个证明是基于新标准的Tait-Martin-Lo？f并行归约的概念。虽然在文献[26，8，25，22，17，20]中有许多基于计算机的Church-Rosser定理的证明α转换可以通过消除命名变量的语法类别而有利于deBruijn索引[3]，或者通过使用逻辑框架本身的变量[6]而不是将其纳入编码系统来避免。只有McKinna和Pollack [17]使用命名变量，而不是de Bruijn指数或逻辑框架本身的变量。然而，McKinna和Pollack，在根岑和Prawitz的脚步之后，对自由变量和约束变量进行了严格的句法区分。我们的命名变量方法不同于McKinna和Pollack，因为我们没有对自由变量和约束变量进行区分。因此，与McKinna和Pollack不同的是，我们必须在发展各种约化概念之前形式化α-等价。同样，这种处理λ演算的愿望，而不是PVS系统（或任何其他定理证明器）希望它看起来如何，是由我们希望将这种处理扩展到可能不那么容易简化的更丰富的系统的愿望所激励的。类似地，麦金纳和波拉克也使用了他们称之为棘手的表征，即忠实于直觉概念，但其忠实性未被正式化。[17]中的一个典型例子是将变量重命名为Lisp风格的关联列表，即一个变量对的列表，并使用Lisp风格的asclock操作来获得变量的新名称。 这类一个alist代表一个函数，这是一个偶然的特性，因为在alist前面的coning隐藏了与变量相关的任何旧值。 事实上，他们指出，这种代表性使它很难构造双射重命名，以至于他们避免这样做。类似地，当自然数学处理使用函数时，麦金纳和波拉克几乎只使用列表来表示。另一方面，我们的方法选择尽可能使用自然的数学表示。我们将在稍后更详细因此，我们的方法的新颖方面是：• 我们使用PVS系统，特别是它内置的抽象数据类型工具，来验证Church-Rosser定理的一个版本• 我们形式化了λ演算的一个版本，就像它通常出现在教科书中一样，福德和梅森126≡≡≡≡≡而不是根据机器或系统的需要进行调整• 我们在λ演算的按值调用版本上处理ISWIM变体，而不是更简单的传统按名称调用版本。然而，这里报告的工作的主要目的是评估PVS作为一种工具，用于开发，最先进的，基于操作的编程逻辑，为现实的编程语言。2Church-Rosser定理的旋风之旅跟随[24]的脚步，我们提供了按值调用λ-演算和Church-Rosser定理的旋风之旅。Church-Rosser定理在历史上被认为是一个系统的一致性证明，该系统被 如今，λ演算和Church-Rosser我们对λ-演算的处理遵循Landin [9]（a la ISWIM）的处理，因为我们包括常数和原始运算，以及更常见的λ-抽象和应用。每个原始操作都是随机的，我们将在本文的其余部分中抑制其存在。我们从一个无穷多变量集合X（x，y，z在X上的范围），一个常数集合A和一组原始运算符号O开始，并通过归纳法定义λ-表达式集合Λ。为了我们的目的，Λ是满足以下条件的最小集合：Λ：：= X<$A<$λX. Λ Λ（Λ）O（Λ，.，Λ）Λ的归纳性质允许无数的秩函数，以及结构递归。 使用结构递归的简单定义是出现在表达式中的变量、自由变量（FV（e））和绑定变量的集合。作为定义（避免捕获）替换e0 [x：=e1]和绑定变量重命名（也称为α-转换）的伴随概念的前奏，对λ-演算的仔细处理将通过结构递归定义变量重命名的概念。变量重命名拥有的一个很好的特性是它保留了等级，不像替换。于是α-转换和替换本身就由结构递归来定义。 在这个α一般来说，我们需要定义一个α-等价的概念，并注意到，αλ-表达式现在只区分到α或更少的频率形成商Λ/。 当然，后者首先需要确定，α是一致的，并且感兴趣的操作（例如重命名和α替换）都是关于它的功能。推导的规则，αα对于λ-抽象，λx0.e0λx1.e1，简化为显示e0[x0：=y] e1[x1：=y]对于合适的Y。从逻辑的观点来看，我们至少有两个选择：我们可以要求这个假设对某个新的y为真（即y/∈FV（e0）<$FV（e1）），或者我们可以要求它对所有这样的y都为真。 即使这两福德和梅森127βv−→βvβv00βvβv、、、1我n1我i+2nβvβvβv（βv）（λx.e）v−→e [x：= v]，其中v为值。（δ） o（e， . ，e）−β→vv如果e，...，e∈Dom（δ）和δ（o，e，.，e）= v.（Cλ）1n1n1ne0−→e1λx.e0e−→λx.e1ee−→e（C左）0e（e）−β→v1e（e1）（C右）0 1e（e）−β→v e（e）1（Cδi）o（e ，...，e，e，ee−β→v， .. . ，e）−β→veJo（e ，...，e，eJ，e，...，e ）的方式0≤i≤n。Fig. 1. 单步β值缩减形式将生成相同的关系，精确的选择将对严格的机器检查证明产生重要的后果。现在，在λ项上定义（按值调用）计算的时机已经成熟。要做到这一点，我们需要将值集V指定为λ项的子集（有时是归纳定义的），在这种情况下，λ项由常数、变量和λ抽象。 单步β值缩减关系−→是参数化的在一个δ函数中，δ：O（An）<$→V，由图1中的规则生成作为定义−→既不自反，也不传递。作为标准，给定一个关系R，我们定义R是R的传递自反闭包一个关系R被称为具有钻石性质，记为，（e0，e1，e2）（e0Re1e0 Re2（e3）（e1Re3e2 Re3））一个关系被称为 教会-Rosser定理指出that<$（−β→v）。因为−→既不是rexexive，也不是trans-in-如果ve不是这样，则（−β→v）的。希望他考虑以下几点反例 在每种情况下，虚线箭头都不属于−→。相对论性：（λx.y）（λw. （（λx.x）z））（λx.y）、、、、_，.、、、、，zy_λw.z、、、、、、、、、、、、、、zy_。、、、、、、、、、、、、、i+2βv、福德和梅森128，z、、pp−→ppN1112221p2及物性：（λx.xx）（λw. （（λx.y）z）），，，，，，，，，，，，，，，，，，，，，，，，，，，，，，（λx.xx）（.....，zλw。）z）（（λx.y）z））λw.y），，，，，，，，，，，，，，，，，，、、、.....（（λx.y、、（λw.y）（λw.y）这个定理的Tap演绎关系−→是自反的，它合并了左应用和右应用简化为单个规则，并允许在单个步骤中，抽象和值都在βv简化步骤中减少，完整定义见图2。因此，证据来自于确立三个事实：(i) （−→）成立。这是证据的微妙部分。我们的证明版本是一个结构归纳法，它证明了e0e1和在最后一步证明中，通过案例分析，这不是唯一的证明方法，例如Takahashi [29]最近发表了一个证明，它不分析约简，而是依赖于取最大并行缩减步骤（称为完全展开）。我们不遵循这个版本的证明。(ii) （−→）意味着 这对任何关系R都成立，有一个很好的几何证明。使用双重归纳法也相对简单。LM1M2. . .M LM1M2M....................J J1 1J填充到NJJ J......王空军王空军...王空军.........NJNJ...王空军(iii) −→v与−β→v的关系相同-是的Pollackpointsout[24]thatthisstepis通常被认为是微不足道的，但可能会导致命名变量approach.在我们的证明版本中，这些观察都不是真的。这些证明不是微不足道的，但也不是有问题的。2.1编码与证明综述总而言之，我们对λ演算的编码，以及随后对Church-Rosser定理的证明NN福德和梅森129ppp≡pppβv02131n1nppp∗（Pre）e−→ee−→ eJv−→pVJ（Pβv）（λx.e）v−→对于va值。eJ[x：=vJ]p（δ）o（e1，.，e n）−→ vife1，.，en∈Dom（δ）和δ（o，e1，.，e n）= v.（Pλ）e0−→e1λx.e0−→λx.e1p（P）e0−→ e1e2−→e3（P）ei−→ eJi0≤i≤ n。appe（e）−→e（e）δo（e， .e）−→o（eJ，.，eJ）• 语法：图二. 并行β值约简定义λ-表达式的语法，以及表达式秩、自由变量和绑定变量、重命名和替换的相关概念。• 阿尔法：德费恩α “那是一种等价关系。α重命名和替换都是模函数。几个引理关于重命名和替换之间的相互作用，也需要建立。• 商：α形式化只识别λ-表达式到λ的概念。• β和 δ：定义单步β值缩减（δ函数中的参数）• 关闭：开发一种通用的机制，用于生成关系的传递性和响应性闭包，以及一种建立关于这种闭包的事实的方法（例如秩归纳）。• 平行：定义单步并行归约的概念，并建立有关它的一些基本事实。例如，它保持值，并通过替换保持：e−→eJ<$$>（e∈V<$eJ∈V）（e0−→e1v0−→v1）e0[x：=v0]−→e1[x：=v1]• 校样：现在的证明包括上述三个步骤p·（−→）保持p· （−→）意味着· −→将相同的关系转换为−→pppppp福德和梅森1303PVS概述PVS是由SRI开发的验证系统，并借鉴了近20年的设计经验。PVS有一个非常复杂的类型系统，它包括谓词子类型、依赖类型、参数化理论、定义抽象数据类型的机制、数字（实数和整数）、序数和归纳形式。当然，这种力量是有代价的。 在这种情况下，代价是类型检查是不可判定的。 因此，类型检查器生成需要由PVS系统或其用户释放的TCC（类型正确性条件）。PVS类型系统的优点是前置条件和后置条件可以合并到函数的类型中。前置条件通过声明一个限制性更强的参数类型来合并，而后置条件通过声明一个限制性更强的返回类型来合并。由于PVS的规格复杂，有可能被TCC淹没。因此，提供了一种通过判断来减轻TCC的积累的机制，其使类型检查员可以获得更具体的信息。判断有两种。常量判断表明一个特定的常量有一个比它声明的类型更特殊的类型，而子类型判断表明一个类型是另一个类型的子类型。我们在证明中指出我们在哪里使用判断机制。在PVS序言中提供了理论的背景集合。包括数字，集合运算，有限集合，序数，函数，归纳方案和抽象数据类型的理论，包括列表定义。序言还载有若干判决。PVS prover通过类似Lisp的接口接受Emacs中的命令。这些命令由称为策略的高级命令和称为规则的一些更具体的命令组成。策略旨在解决广泛的问题，并理想地自动完成证明另一方面，规则使用户对证明有更多的控制，尽管所采取的操作通常更原子化。例如，分裂规则将当前证明分裂成许多子证明，而prop策略将证明分裂，然后应用命题简化和简化。一般来说，首先尝试使用更高级别的策略进行证明是一个好主意，只有在必要时才使用较低级别的命令。除了提高自动化水平外，这种方法还产生了更能抵抗规格变化的证明。PVS提供了一种使用构造函数列表来归纳定义抽象数据类型（ADT）的机制。从这些构造器中，自动生成一组完整的公理，其中包含：• 外延性公理（两个对象是相同的，如果它们是由相同的组件构造的）。• Eta公理（由X的相同成分构造的对象与X相同）福德和梅森131• 访问器公理（构造函数的组件是适当的访问器参数）• 介绍计划（介绍会计发展工具包的结构• 递归组合器（用于定义自然数或序数集的秩函数）除了ADT公理之外，PVS还自动为所有归纳定义生成归纳方案。PVS规范分为理论和数据类型定义。每个定理由一个（可能是空的）参数列表、导入和导出语句、类型定义、常数定义、函数定义、判断和引理组成。参数可以是类型、子类型或常量。导出语句用于指定对导入当前理论的理论可见的名称。参数化状态指定要导入的理论列表，并且可以参数化或非参数化。4λ-演算的编码4.1语法变量集被定义为一个类型，其属性为对于每个有限元素，在一组变量中，有一个变量不包含在其中。根据这个定义， 一个新的函数可以定义在有限个变量集上，具有以下性质：（x）（x）（y）（y）（λ-表达式的集合被定义为抽象数据类型。Λ[A：TYPE+，O：TYPE+，#：[O→nat]]：DATATYPE开始导入XVar（x：X）： Var？λ（x：X，e：Λ）：λ？ap p（e：Λ，eJ：Λ）：app？K（a：A）：K？δ（o：O，l：list[Λ]）：δ？结束Λ数据类型有三个参数，原子的非空类型A，原始函数的非空类型O，以及将每个原始函数映射到其arity的函数#λ-表达式的秩是使用自动生成的递归组合子定义的（参见第3节）。秩在我们的规范中用于对λ-表达式进行归纳证明证明了福德和梅森132∈一个表达式的秩大于它的所有子表达式的秩rk（e）= 1e∈（X<$A）rk（λx.e）= 1 +rk（e）rk（e（e0））= 1 +rk（e）+rk（e0）rk（o（e1，e2，...，e n））= 1 + rk（e1）+rk（e2）+. +rk（en）我们通过归纳定义发展了自由变量（FV）的概念FV（x）={x}FV（a）={}FV（λx.e）= FV（e）−{x}FV（e（e0））= FV（e）<$FV（e0）FV（o（e1，e2，.，e n））= FV（e1）<$FV（e2）<$. FV（en）我们可以将新函数应用于表达式的自由变量集，以获得新的变量，从而避免意外捕获。这里的问题是，新函数定义在X的有限集合上，FV（e）定义为具有setof（X）类型，因此取FV（e）的new将导致生成TCC。包括一项判决，但该判决指出，我们规范中的FV（e）Fin（X）抑制了此类TCC 的产生。序言包含关于有限集合并、交等的判断（例如（<$X，Y∈Fin（T））（X<$Y）∈Fin（T））。因此，即使是new（FV（e）<$FV（e0））形式的表达式也不会产生TCC。定义FV允许我们处理重命名和替换。重命名函数将一个变量的所有自由出现替换为另一个变量。为了实现这一点，有时可能需要重命名表达式的绑定变量以防止捕获。（λy.x）[x：=y]/=λy.y我们通过重命名所有λ绑定变量来做到这一点。（λy.x）[x：= y]= λz.y 对于某个新变量z一般来说，对于λ-抽象，重命名被定义为（λx.e）[y：= z] = λx0. （e[x：=x0][y：=z]）其中x0=new（FV（e）<${y，z}）在定义重命名功能时，我们首先遇到了TCC的麻烦。如第3节所述，TCC需要由PVS系统或用户证明不幸的是，有可能产生无法证明的TCC，通常来自相当无害的规范。 例如，考虑lambda情况福德和梅森133≡α∀α重命名函数：e[y：=z]：递归Λ =以下情况e：...λx.e0：设x0=new（FV（e）<${y，z}），λx0。（e0[x：=x0][y：=z]）...Endcases措施rk（e）为了证明函数终止，我们需要证明递归调用中的每个表达式都小于原始表达式。现在很明显rk（e0）

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