42→∀ ∃理论计算机科学电子笔记70第2期（2002）URL：http://www.elsevier.nl/locate/entcs/volume 70. html18页s从程序Femke van Raamsdonk1荷兰阿姆斯特丹自由大学理学院数学与计算机科学系CWI，阿姆斯特丹，荷兰Paula Severi保拉·塞韦里2，3Dipartimento diInformaticaUniversit`adegliStudidiTorino Torino，Italy摘要本文提出了一个步骤，在发展中的一个可操作的方法，程序提取类型论。为了从lambda项得到一个程序，需要删除逻辑部分。 这是通过一个简化关系来实现的。- 是的我们研究了β-归约和β-归约的组合，无论是在简单类型的lambda演算的设置和纯类型系统。在一般情况下，研究了其性质一致性、主题约简和强规范化。1介绍一个程序的规范，例如“对于每一个自然数的有限列表，都有一个排序的置换”，一般是x的形式。y.P（x，y）.在类型论中，这被表示为类型x：A。B.P（x，y）.程序提取的思想是从这样一个类型的居民t中提取一个函数f：A→B，该函数具有P（x，f（x））对所有x都成立的性质。提取这样一个函数f的问题是，一般来说，它将包含信息其正确性证明。1 电子邮件地址：femke@cs.vu.nl2电子邮件地址：severi@di.unito.it3 第二作者感谢 自由大学和 莱斯特大学他们的好客。她得到IST-2001-322222 MIKADO; IST-2001-33477 DART的部分支持。2002年由ElsevierScienceB. V. 操作访问根据C CB Y-NC-N D许可证进行。范拉姆斯东克和塞维里43→在过去的二十年中，已经研究了几种程序提取方法。本文以[19，18]中介绍的规范理论为出发点。在那里，从一个规范的证明中提取程序的过程是通过一个归约关系→ σ来建模的。基于规范理论的软件工具应该使用β-约简和σ-约简的组合。因此，研究其组合β-约化和σ-约化。事实证明，这种组合产生了几个问题;例如，主题减少并不成立。本文主要研究β-归约与σ-归约结合所引起的句法问题。我们将注意力限制在定义σ-归约关系的九条规则中的三条规则上，这三条规则是概率性的。σ-约化关系的这个子集称为σ-约化关系。我们研究了β-约化与α-约化的结合。结果表明，当β-约化受限制时，β与β的组合具有约化、连续性和强正规化等性质.证明和程序都表示为λ-项。然而，术语的类型揭示了它是证明还是程序。归约关系删除了程序中的证明.例如，考虑以下术语：（λx：Nat. λy：（Eq x x）。x）零回复它包含一个命题（Eqx x）作为参数的证明，也包含一个抽象，其中y被声明为这个命题的证明。 为了得到一个真正的程序，简化的方法分两步删除了这个证明和抽象.（λx：Nat. λy：（Eq x x）。x）零回复→λ（λx：Nat. λy：（Eq x x）。x）零→λ（λx：Nat. x）零显然，如果我们希望类型在归约下保持不变，我们需要将递归归约扩展到类型。然后是类型x：Nat。（Eqx x）→Nat简化为（Nat →Nat）。2一种可操作的程序抽取方法在[19，18]中引入的σ-归约描述了程序提取的过程（见图1）。这种描述与我们选择的lambda演算类型无关[6]。它给出了一个清晰的理解的过程，可以被看作是一个系统，提取不执行后验，但集成到逻辑系统的语义的candidate。程序抽取的常用算法是这种约简的规范化策略的实现由于σ-约化规则的加入，Σ-型变得比σ-型强范拉姆斯东克和塞维里44分配性U.S.（Σ y：A.P y）→Σ f：（σ x：U. A）。U.S.P（f x）λx：U。 σ_a，p_a →σ_λ_x：U. a，λx：U. pa，pCurry公式（我们假设x s=x d，x p）。x s：（→σ_x d：A. P.Uλ xs ： （λ xd ： A.P ） .u→σλ xd ：A.λx p：P. uua，p→σua p从程序中消除证明： 如 果 xp/∈FV（A），则<$xp：P. A→σAλxp：P. a→σa如果xp/∈FV（a）ap→σ aFig. 1. 定义σ-reduction。强烈的，强烈的。在这里我们称之为超投影至少具有强投影的表达能力，因为第一个和第二个投影可以编码为：π1=λxs.xd和π2=λxs.xp。但它也超越了强可扩展性，因为它有一个额外的属性，使程序提取总是可能的。这一附加属性对应于可实现性概念的内在化：任何具体化在计算上等于基本具体化：A.P x，并且该具体化的任何证明在计算上等于一对a，p，a：A和p：P a。 然后，从一个居民的程序提取，一个具体化就是只取对的第一个分量。例如，一个物种的居民：A。B.（Pxy）简化为一对其中f是A→B类型的提取程序，q是它的正确性是：A. （P x（f x））。为了开发一个程序提取的例子，我们首先要说明如何将sigma约简扩展到处理自然数。在[18]中，我们已经在归纳构造演算的一般设置中做了这种扩展。具有构造函数zero和zero的归纳数据类型Nat具有以下内容：4在[19]中，这个类型构造函数使用了一个不同的符号范拉姆斯东克和塞维里45∀ ∃→降低淘汰规则：中文（简体）如果s∈ {*d，*p，*s}，则Γ，x：Nat<$U：sr=u1：U[x：=n]（natrec）Nat. （U [x：= m] → U [x：= m]）Γ（natrecu1u2n）：U[x：=n]为了便于说明，我们省略了natrec对应于U型的第一个参数。钠曲肽的减少定义如下：（natrecu1u20）→ιu1（natrecu1u2m）→i（u2m（natrecu1u2m））当U是一个特例时，为了得到该算子的正确约化，我们必须将σ-约化的定义扩展到包括以下分配律。在该规则中，我们将使用以下缩写：P= λ n：Nat. （Pn（natrecAa1a2）n），p∈2= λ n：Nat. λq：（P<$n）。（p2n（natreca1a2n）q）（natrec在对上的（natreca1，p1a2，p2n）→σ（natreca1a2n），（natrecp1p2n）而不是对的谓词P的分量。事实上，谓词P应用于第一个我们现在准备给出一个在[18]的规范理论中的程序提取的例子，并说明在哪里需要从程序中擦除逻辑我们考虑这样一个规定：每个不等于零的自然数都有一个前趋数。 本规范编写如下：[18]如：S = Nat. Nat.n> 0 → Eq n（Nat.n）在一阶逻辑中，S可以写成n。 M. （n>0）（n=1m）。我们使用以下缩写和假设：• A= λn：自然小娜• P= λn：自然λm：Nat.n> 0 → Eq n（λ m），• U = λn：自然Nat. （P n m），• 存在项p0，pm，使得p0：P00和m：Natpm：P（pm）m，• q = λm：Nat.λx：（U m）。下午。范拉姆斯东克和塞维里46DDppDp下面的项是类型S：s = λn：Nat的居民。（natrec 0.00，p0.05）（λm：Nat.λx：（U m）。m，pmn）的利用[18]的σ-约化关系，我们可以分两个阶段约化s在第一阶段，s被简化为一个由程序及其正确性证明组成的对：s→σ_λn：Nat. natrec 0（λm：Nat.λx d：Nat.λx p：（P mxd）。m）n，λn：Nat. natrec p0q n这个对的第一个组成部分包含抽象λxp：（P mxd）.m，它需要（P mxd）的证明，并产生一个自然数m。这种抽象可以使用σ-归约定义中的一条从程序中删除逻辑部分的规则来去除：λn：Nat. natrec 0（λm：Nat.λx d：Nat.λx p：（P mx d）。m）n→σ（通过擦除，也→σ）λn：Nat. natrec 0（λm：Nat. λ x d：Nat. m）n =定义预测值最后一项pred是提取的程序。在本文中，我们不考虑对，而只考虑从程序中消除逻辑部分的子归约→归约。3简单类型的案例在这一节中，定义了λ→β演算，其中包含两种类型的λ-演算的操作：一种用于数据类型，一种用于命题。从数据类型到命题的功能通过归约关系→n来消除。λ演算的两个副本是从一组类型变量开始获得的，这些变量被分成两部分：Vartypes=Vartypes<$Vartypes和一组项变量，分为两部分：Varterms=Varterms<$Varterms。类型是以通常的方式从Var类型的元素和类型构造函数→构建的。类型写为U，V，. 这些术语是以通常的方式从Var术语、抽象和应用的元素中构建的。项写为u，v，。. .现在，类型集被分成一组数据类型和一组命题，直观地说，通过检查范围类型是在Var类型中，数据类型的变量集，还是在Var类型中，命题的变量集。类似地，术语集被分成一组数据术语和一组证明，直观地说，通过检查左脊上的变量是否在变量项，数据项的变量集，或变量项中的变量集D p为了证明 对于形式定义，我们需要心的概念[9]（p.116）。范拉姆斯东克和塞维里47DpDpDp→→定义3.1类型和术语的核心归纳定义如下：h（X）=Xh（x）=xh（U→V）= h（V） h（λx：U. u）= h（u）h（u v）=h（u）现在类型和项的划分如下。定义3.2(i) 数据类型d和命题类型p的集合定义如下：D型 ={U |h（U）∈ Var类型}类型p ={U |h（U）∈ Var类型}数据类型写为A、B、. . 和命题P，Q，. . .(ii) 程序项d（或数据项）和证明项p（或prop-terms）的定义如下：项d={u |h（u）∈ Varterms}项p={u |h（u）∈ Varterms}程序可以写成a，b，... 证明为p，q，.. . .我们假设在λx：U中。我们有x ∈ Var项和U ∈类型d或x∈Var项和U∈类型p。所以抽象直观上讲得很好-整理好了归约关系删除了数据类型中出现的命题和程序中出现的证明，因此它既根据类型又根据项来定义3.3类型上的约简关系，记作，是在类型的形成下封闭的最小关系，包含规则：（P→A）→A关于项约简关系，记作，是在项的形成下封闭的最小关系，并且包含以下两个规则：λx：P.a→P.a如果x/∈FV（a）ap→P.a例如，（λx：λ。zerox）p→n（λx：n. zerox）→（λx：. zero）→zero，其中是一个命题，p是一个证明。我们考虑一个受限β-约简，它由两个重写规则生成，取决于论证是程序还是证明。范拉姆斯东克和塞维里48→⊥定义3.4β-归约关系，记作β，是在项的构成下封闭的最小关系，包含以下内容（λx：A. u）a→βu [x：= a]（λx：P. q）p→βq[x：=p]注意以下项不是β-赎回：（λx：A. u）p（λx：P. p）a（λx：P. a）p前两个不是β-还原，因为它并不打算用一个证明来代替一个程序变量，也不是用一个程序来代替一个证明变量（它们在λ→β中是不可能的）。更进一步，如果第一个术语是β-redex，则n个一致性不成立;见备注3.5。如果最后一项是β-redex，则类型系统不满足主语归约和强规范化;见备注3.7和备注3.8。如果前两个不是β-redex，但最后一个被承认为β-redex，那么我们得到一个连续的弱正规化但不是强正规化的演算。注意，它没有完全扩展[10]。这就是在[18]中研究的规范理论注3.5为了方便起见，必须有一个形式为（λx：A. u）p不是β-redex。例如，我们有p β←（λx：Nat. x）p→λ（λx：Nat. x）。 上面给出的另外两个非β-还原不产生不连续的还原：形式为（λx：P. p）a的项不产生更关键的对，而形式为（λx：P. p）a的项不产生更关键的对。 a）p产生关键对，关闭（如果所有关键对都是开发关闭的，那么重写系统是连续的[22]）。简单类型λ-演算的一般类型系统与λ→β-演算的类型系统的区别在于，它的类型被认为是模-转换。 在环境Γ中，我们假设对于所有声明x：U，有x∈Var项和U∈类型d 或x∈Var项和U∈类型p。D p因此，环境直观地说是有序的。定义3. 6λ→β的分类系统由以下规则定义：（start）x：U∈ΓΓx：U（-conv）Γu：Uu：UJ其中U=UJ（abs）Γ，x：Uv：VΓ λx：U。v：（U→V）（app）Γv：（U→V）Γu：U中文（简体）例如，项（λx：. zero x）是可以使用转换规则来类型化的。这个术语在Coq中是不可类型化的，尽管存在从命题到数据类型的函数，例如f：bot → nat与bot：Prop和nat：Set。范拉姆斯东克和塞维里49→⊥ → ⊥ → ⊥ → ⊥ →注3.7对于主语归约，形式为（λx：P. a）p的项必须不是β-redex。假设n：Nat，令a = λx：λ。（λy：（λ → λ）.n（yx））x aJ=λx：λ.n（xx）显然，a→βaJ。 但是，a是可类型化的，而J不是。 要键入a，我们使用2016 年02 月03日@上午10 时30 分（Nat）和（（）Nat）=（Nat）。主语归约的证明（定理4.13）在应用规则中失效。从（（→）→Nat）=（→Nat）我们不能得出（→）=的结论。直觉上，问题在于方程P Nat=P，对所有命题P都成立。注3.8对于强正规化，形式为（λx：P. a）p的项必须不是β-redex。作为一个例子，我们重新考虑从备注3.7的条款，但现在有一个不同的类型。我们使用缩写A=A→ A。a= λx：自然（λy：（Nat→Nat）.n（y x））x aJ=λx：Nat.n（x x）我们有a→βAJ和a：Nat→Nat。此外，我们考虑以下术语：p=λx：Nat.x（（λy：（Nat→ Nat）.n（yx））x）pJ=λx：Nat.x（n（xx））我们有p→βpJ和p：Nat。 从ap：Nat开始，我们有：ap→βa Jp J→βn（p Jp J）→βn（p J（n（p Jp j）→β.下面列出了λ→βλ系统的一些性质。第一个和第二个属性的过程很容易。对于纯类型系统的情况，第三个问题的证明在附录中概述我们写→β表示→β和→β。定理3.9(i) 约化关系→ β在项集上是连续的。(ii) 归约关系→ β满足主体归约。(iii) 计算λ→βε是βε -强正规化的。4纯类型系统中的函数消去在本节中，我们将β-归约扩展到伪项，并定义了具有β-归约转换的纯类型系统（PTSβ-归约）。这种减少消除了PTSβ的某些功能。对于纯类型系统（pure type systems，PTS）的基本概念，我们参考[1]。范拉姆斯东克和塞维里50||||→定义4.1设Var为变量的集合，记为x，y，. 和集合S的排序，写为s，sJ.。. .伪项的集合由以下语法定义：PT：：= Var S（Var：PT。PT）（λVar：PT. PT）（PTPT）。伪项被写为u，v，U，V，. . .定义3.1中给出的类型和术语的心脏概念扩展到PTS的情况，如下所示。定义4.2[9]（p.116）伪项的核心由归纳法定义：h（x）= x，h（s）= s，h（x = U. V）= h（V），h（λx：U. v）= h（v）和h（u v）= u。在简单类型的情况下，心脏的概念用于将伪项的集合划分为两个集合：数据伪项和属性伪项。定义4.3设Vard和Varp是两个不相交的集合，使得Var=Vard<$Varp，Sd和Sp是两个不相交的集合，使得S=Sd<$Sp。 数据伪项的集合PTd和属性伪项的集合PTp定义如下：PTd={u|h（u）∈Vard<$Sd}PTp={u|h（u）∈Varp<$Sp}数据伪项被写为a、b、A、B、. 并且prop-pseudo-terms被写为p，q，P，Q，.。. .类似于简单类型的情况，我们假设在λx：U中。u和x：U。V我们知道x和U都属于同一个集合，要么PTd，要么PTp。伪项上的β-归约概念的定义与定义3.4中用“伪项”替换“项”一词定义4.4归约关系，记作，是在伪项的构成下封闭的最小关系，包含规则：如果x/∈FV（a），则λx：P.a→λa 如 果 x/∈FV （ a ）ap→λa，则λ x：P. a →λa我们将约化关系写成→β，它是→β和→的并集。注意，集合PTd和PTp在β-转换下是闭的。我们假设我们的规范是有序的：定义4.5一个纯型系统的具体化（S，A，R）被称为对偶的，如果S =S d <$Sp，其中S d和Sp是不相交的，A <$S d × S d <$Sp × Sp和R <$S × S（即如果（s1，s2，s3）∈ R则s2 = s3）。从现在开始，我们假设我们的规范是对偶的。纯类型系统是通过转换扩展的.类型系统像往常一样包含形式为Γu：U的判断。在环境中，范拉姆斯东克和塞维里51我们假设对于所有的声明x：U，我们有x和U属于同一个集合，或者是PTd，或者是PTp。因此，环境直观地说是有序的。定义4.6设S=（S，A，R）是一个对偶规范。一个具有β-转换 λ-S（PTSβ-）的纯类型系统是通过将λ-转换规则添加到纯类型系统的规则中来定义的（公理）S1：S2（S1，S2）∈A（start）r，x：U（weakening）（弱化）r，x：Uv：V（乘积）Γ<$U：s1Γ，x：U<$V：s2（x新鲜，用于Γ）（x新鲜，用于Γ）（s，s，s）∈RU. V：s3（抽象）Γ，x：Uv：VΓ x：U. V：sΓ λx：U。v：px：U. V（应用）Γv：x：U。 Vu：UV[x：=u]（β-转换）Γu：UΓV：s中文（简体）1 2 3U=βV实施例4.7(i) 设S=（S，A，R）是一个纯类型系统的特例。我们写sd表示符号s与d的连接，sp表示连接符号s和p的关系S的复制是一个特殊的2S =（2S，2A，2R），定义如下：(a)2 S ={sd，sp|s∈ S}，(b) 2 A ={（sd，s Jd），（sp，s Jp）|（s，SJ）∈ A}（c）2R={（sd，sJd，sJdJ），（sp，sJd，sJdJ），（sd，sJp，sJpJ），（sp，spJ，sJpJ）|（s，SJ，SJJ）∈R}.降阶关系删除了由形式（sp，sJd，sJdJ）的规则形成的函数。(ii) 在第3节中定义的系统λ→β可以看作具有以下规格的PTSβ（a）S={*d，*p，nd，np}，（b）A={（*d，d），（*p，p）}，(c)R={（*d，*d），（*d，*p），（*p，*d），（*p，*p）}。约简删除了由规则（*p，*d）形成的函数。 (iii)如果我们从[19]的规范理论中删除排序和排序范拉姆斯东克和塞维里52→D−pDDppDDDppDpp我们得到PTSβ，其规格（MLD）定义如下：（a）S={*d，*p，nd，np}，（b）A={（*d，d），（*p，p）}，（c）R={（*d，*d），（*d，*p），（*p，*d），（*p，*p），（*d，*d），（*d，*p），（*p，*p）}. 请注意，此规范不包含（*p，*d），因此它不是任何规格的重复。约简关系删除了由规则（*p，*d）形成的函数。(iv)如果我们从[18]的规范理论中移除规范的排序，我们得到一个PTSβ，其规范定义如下：（a）S ={* i，* i|i ∈ N}，（b）A ={（* i，* i+1），（* i，* i+1）|i ∈ N}（c）R={（*i ，*j），（*i ，*j），（i，*j），（*i ，*j）}，其中i≤j，或j= 0。这个系统是λC∞[17]的复制，λ C ∞ [17]是扩展构造演算[11]的一个子系统。减少关系删除这些函数是由（*i ，*j）形式的规则pd由于β-约化规则是正交的，β-约化规则和β-约化规则的并集也是正交的，我们有以下结果。定理4.8（推论）(i) 约化关系→(ii) 约化关系→ β与伪项集是连续的。由于伪项是连续的，并且它显然是强正规化的，我们得到伪项的伪正规型总是存在的，并且是唯一的。我们用nf∈（u）表示u的标准形式。P-normal形式移除出现在数据伪项内部的prop-pseudo-terms ，即a的P-normal形式不包含PTp中的子项。特别是，它不包含Varp中的变量。从类型的观点来看，这种归约方法去掉了由Sp×Sd规则构成的函数.换句话说，λ-范式将λ<$S中的可类型化项映射到仅具有β-约简的纯类型系统中的可类型化项，其规则集通过减去Sp×Sb获得。定义4.9设S=（S，A，R）是一个对偶规范。 我们记为S−指定S−=（S，A，R−），其规则集为R−=R−Sp×Sd。示例4.10(i) 在[19]中定义的验证演算是纯类型系统，其规范是MLD−= MLD（*p，*d），其中MLD是例4.7（iii）中给出的规范。(ii) 在[16]中定义的系统λω L是λω的复制，没有形式为（sp，sJd）的规则，并且具有extr规则（*d，p）以在程序上写入谓词s。所以λωL= λ2 ω−ε（*d，εp）。(iii) 在[18]中定义的验证演算是λ（2C∞）−，其中λ2C∞为范拉姆斯东克和塞维里53→►►实施例4.7（iv）.将这种简化扩展到环境中，而-通过对每个声明的类型应用numer-reduction。对于伪项，上下文的标准形式表示为nf（r）定理4.11（Sp×Sd中函数的消去）若Γ<$u：U在 λ<$S则nf<$（Γ）<$nf<$（u）：nf<$（U）in λS−.证据这是证明了归纳的推导。对于β-转换规则的情况，我们必须首先证明，如果uβ <$ uJ，则nf（u）→βnf<$（uJ），这是由u上的归纳得出的。✷推论4.12(i) （β-弱正规化的保持）如果系统λ S−是β-弱正规化的，那么λ S也是。(ii) （λS−上λ S的保守性）设Γ，u和U是λ S −中的正则项。 如果Γu：U在λ <$S中，则Γ u：U在λ S−。λε2S在λS或λ2S上不具有保守性。例如（P→A）→A在λ→β约化中是可解的，但在代数式λ演算中或在它的只有β约化的复制中是不可解的.这种类型被解释为一个命题甚至不是一个重言式！定理4.13（→ β的主语归约）若Γ <$u：U且u→βUJ，则Γ <$UJ：U.替换引理和通常的[1]一样被陈述并用于下面的证明。证据这是证明了归纳的推导连同一个类似的声明，环境如常。在应用程序的情况下，我们使用替换引理和以下观察：(i)如果（A. V）= β <$（λ x：A J.V J），则A = β <$A J且V = β <$VJ。(ii)若（Px：P，Q）= β（Px：P J. Q J），则P = β <$P J且Q =β <$Q J。这一观察结果不适用于形式为（P.A.）的产品（见重新标记3.7）。✷证明主归约的问题在于，当我们试图以通常的方式证明主归约时，我们陷入了循环：对于主归约，我们需要加强主变量，反之亦然。关键是找到一种方法来同时证明它们。55我们的系统不是代数类型系统的实例[2]，因此我们不能应用这是我们案例主体还原的一般结果范拉姆斯东克和塞维里54→定理4.14（对正整数的加强和主题归约）我们考虑一个单排序规范S。(i) 设x/∈ fv（u）<$fv（u）<$fv（U）.若Γ，x：P，u：U则Γ，u：U。(ii) 如果r u：U且u →uJ，则r uJ：U。证据为了同时证明这两个陈述，我们扩展了由环境和伪项组成的对的约简。 [Γu] →[ΓuJ]如果u→uJ[Γu] →[Γju]如果Γ → ΓJ[Γ，x：P，<$$>u]→<$[Γ，< $$>u]如果x/∈fv（<$）<$fv（u）然后我们证明了两种情况下的扩展→除法的主语归约：（i）数据伪项。若Γ_a：A且（Γ，a）→n（ΓJ，AJ）则ΓJ∈AJ：nf∈（A）.(ii)Prop-pseudo-terms.若Γ<$p：P且（Γ，p）→<$（ΓJ，PJ）则ΓJ<$PJ：PJ且PJ=β <$P.这两个声明，然后证明了归纳的推导。在产品和应用规则的情况下，我们使用以下观察结果：(i) 如果p→βs，则p→βs。(ii) 若P→β_（？）Q则P→β<$x：U。 Q.这个观察结果类似于[8]中的关键引理（引理3.4），用于证明η-归约的加强和主体归约。在我们的例子中，这个引理不适用于数据伪项的事实使问题复杂化。这迫使我们将定理的陈述分为数据伪项和属性伪项两种情况。 由于约简会破坏数据伪项A的形状，我们使用了约简下的不变量nf（A）。✷为了证明强规范化，我们可以将λ-兑换（λx：P. A）和（λx：P. a）编码为β-兑换，假设存在P的居民。定理4.15（强正规化）λ-立方体系统的复制是β-强正规化的。我的律师。 我从TheoremA. 3开始。特别地，例4.7（ii）和例4.7（iii）的MLD的λ→β是β-强正规化的。✷5相关工作在本节中，我们将[19]的规范理论与类型论中程序提取的其他方法进行比较。范拉姆斯东克和塞维里55→ER伊芙·R·在Coq 6.3版本之前[5]，提取过程是通过基于可实现性解释的外部函数来执行的[15，14]。σ-归约内化了这个函数。σ-归约的标准形对应于[15，14]中的函数E和R，它们分别计算所提取的程序及其正确性的证明。σ-约化将和推广到Fω和CC以外的类型系统[18].的定义σ-归约在程序抽取过程中引入了新的中间步骤。一个规范的居民s需要几个σ-归约步骤来达到规范形式，（s）。 在这些新的中间步骤中，我们必须从程序中删除逻辑部分。在[14]和[19]的数据类型中，命题和规范是不同的对象。然而，在Coq中，这些对象是在宇宙的层面上被识别的。我们不知道如何在这个级别上识别对象进行σ-约简而不把它弄得一团糟。Coq版本7 [20]中的提取过程是实验性的，也是基于约简关系的。由于几乎没有关于Coq的这种新特性的文献，因此很难将这种新方法与σ-约简进行比较。无论如何，到目前为止，在Coq的所有版本中，提取的程序都是在ML中给出的，并且β-约简只在σ-范式上执行。然而，对于特化理论来说，这个想法是不同的。基于规范理论的软件工具应该统一编程语言和逻辑。应将σ-减少作为评价机制的一部分纳入系统。因此，很自然地会想，就像我们在本文中所做的那样，将β-约化和σ-约化结合起来是否安全。在LEGO [12，21]中，基于可交付成果[3，13]的概念实现了一种具体化机制。在[3，13]中，考虑了一个范畴，其对象是规范，态射是所谓的一阶可交付物。在ECC [11]中，指定和它们的态射是使用双类型写的。如前所述，σ-归约为类-类型添加了一些特定的属性（如图1所示），使程序提取始终成为可能。此外，[19]的规范理论不需要像[3]那样区分一阶和二阶可交付成果。型为S. T用于表示规范S和T之间的函数空间，其中T可以依赖于S。一阶可交付成果不允许这种依赖性，因此必须引入二阶可交付成果的概念。一阶和二阶可交付物的类型是规范之间某些特定函数的σ当T不依赖于x时，（ST）的σ-正规形式给出了一阶可交付物的类型。类似地，忽略一些依赖关系，σ-正规形的σ x：S。（注：T。U）给出了二阶可交付成果的类型。[19]的规范理论与λωL[16]背后的主要思想一致：程序及其正确性证明是可以并行构造的不同对象。在λωL规范中，规范总是成对的（σ-范式），它们在元水平上被操纵。类型系统由成对给出的派生规则范拉姆斯东克和塞维里56不不⟨⟩→→以便同时构建两个组件。 对于每个构造函数，给出了两个推导规则：一个用于程序部分，一个用于证明部分。这种成对规则或耦合派生规则的概念是在元级别。在[19]中，[18]的具体化和[16]的对的概念在语法中是明确的。λωL的一对规则被编码为规范理论中规范之间的唯一规则。sigma约简关系捕获每个构造函数与对之间的关系的属性。应用于[19]的规范理论中规则的前提和结论的σ-范式给出了一个在λωL中对规则对进行编码的对之间的规则（耦合导出规则）。在[4]中，可实现性通过判断关系来表达。虽然这种判断使系统的可实现性内在化，但实现者的类型仍然由外部功能来定义。一个被称为“类型提取”的规则指出，任何实现者都是可类型化的，必须被添加以获得一个可证明性和Kreisel修改的可实现性相一致的系统。这条规则将可实现性的判断与外部函数联系起来。在[19]的规范理论中，类型提取规则是可导出的，并表示为：如果s：S则s→σa，p和S→σx：A.P，因此P的实现子a具有类型A。在规范论中，选择公理（AC）和前提独立性（IP）都是可导出的。AC是简单的推导，因为它是图1中的第一个σ-归约规则也可以推导出公理IP，因为我们可以证明（PΣ_x：A.Q）→σ_x：A. （PQ）使用第一规则图1中的第一组和第三组IP的公理是不可推导的，MartinLo？f的类型理论是可行的，但它是（Kreise l m o d i f i d）可实现的Harrop公式P。 在具体化理论中，没有必要假定P是哈罗普（或这表明[19]的规范理论并不保守于马丁·洛夫的规范理论。 这一明显的变化并不令人惊讶。保守性只适用于不包含依赖于证明的数据类型的系统。6结论对一个包含逻辑部分的程序进行评估--在本文中，我们已经表明，评估一个程序的逻辑部分的我们也可能会失去一些属性，如主语归约（注3.7）和强规范化（注3.8）。我们提供了一个解决这个问题的方案，其中包括限制β-还原。在[7]中，通过要求一项为σ-正规形式，使限制β-约化的解更强。这样，主体归约和强规范化就可以在整个规范理论中得到证明。范拉姆斯东克和塞维里57引用[1] H.P. Barendregt。Lambda结石的类型。 In S. Abramsky，D. M. Gabbay和T.S.E. Maibaum，编辑，Handbook of Logic in Computer Science，第2卷，第118-310页。牛津大学出版社，1992年。[2] G. 巴和帕。- A. 我也是。在这种情况下，可以为大型块型系统提供可靠的数据。在CSL '96会议记录Springer，1997年。[3] R. Burstall和J.McKinna。 可编译程序：一种在构造演算中进行程序开发的方法。在Proceedings of the First Workshop on Logical Frameworks，第113-121页[4] T. 克罗拉德一种类型理论，它对于Kreisel的修正可实现性是完备的ENTCS，23（1），1999年。可实现语义学和应用教程研讨会论文集，1999年。[5] B. Barras等人，Coq证明辅助参考手册。技术报告，INRIA，1999年。[6] M. 我的朋友。 Mackie，P. SeverindN. SZASZ。程 序抽取的一个统一体：具有超类型的纯类型系统. 预印本。[7] M. Ferna'ndezanddP. Severeri. 在构造演算中，一个不可避免的问题是如何处理逻辑抽象。发表于2002年LOPSTR'02会议记录[8] J.H. 吉弗类型lambda演算中βη-约化的Church-Rosser性质。在LICS '92的会议记录IEEE Computer Society Press，1992.[9] J.H.吉弗逻辑和类型系统。博士论文，奈梅亨大学，1993年。[10] M. Hanus和C.普雷霍弗用定义树进行高阶窄化在H. Ganzinger，编辑，RTA '96会议记录[11] Z.罗ECC，一种扩展的构造演算。在LICS '89的会议记录IEEE ComputerSociety Press，1989.[12] Z. Luo和R.波拉克LEGO proof development system：用户手册。技术报告，爱丁堡大学，1992年。[13] J.H.麦金娜类型论中的程序开发分类方法。爱丁堡大学博士论文，1992年。[14] C.波林-莫林从构造演算的证明中提取Fω在1989年的POPL '89的会议记录[15] C.波林-莫林结构计算程序摘录。1989年第7页。范拉姆斯东克和塞维里58Γβ⊃[16] E.民调一种基于类型理论的程序设计逻辑。埃因霍温理工大学博士论文，1994年。[17] P. Severi和E.民调有定义的纯类型系统。在LFCS '94的会议记录Springer，1994年。[18] P. Severi和N.萨斯归纳结构演算中的内部程序抽取阿根廷理论计算机科学研讨会论文集（WAIT[19] Severi和N. 萨斯研究具有内建程式抽取的规范理论。Journal ofAutomated Reasoning，27（1）：61[20] Coq开发团队。Coq证明辅助参考手册版本7.1 2001。网址：http://pauillac.inria.fr/coq/doc/main.html。[21] LEGO团队乐高图书馆，版本1.3，1998年。网址：http://www.dcs.ed.ac.ukwww.example.com/home/l ego/html/re leas e.html.[22] 范奥斯特罗姆。发展关闭关键对。在HOA '95会议记录Springer，1995年。一 强正规化在本附录中，我们概述定理4.15的证明。虽然对λ-立方体系统的重复进行β-强规范化的语义证明是可能的，但我们更倾向于做一个更一般的句法证明，即把λ-兑换编码为β-兑换。为了将（λx：P. A）和（λx：P. a）编码为β-赎回，我们假设存在一个函数，其中Γ：Ctx×PT→PT，使得inhΓ（P）给出P在Γ中的居民。定义A.1设inh：Ctx×PT→PT，且Γu：U或u=s。 然后[[u]]inh（我们省略下标并写[u]]r）由归纳定义，如图A.1所示。注意，[u]]r=u，如果u是n-正规形式。引理A.2如果u→β <$uJ则[[u]]Γ→+[[uJ]]Γ这个引理是通过归纳法证明的。定理A.3设SJ=（SJ，AJ，RJ）S =（S，A，R）. 假设满足以下条件。(i) 设λSJc有足够的函数来计算λ<$S的幂指数：对所有的（s1，s2）∈ R，有s3∈ SJ使得（s2，s3）∈ AJ和（s1，s3）∈ RJ.(ii) λ SJ是弱β-正规化的，并且满足类型的唯一性（直到β-转换）。(iii) inh是一个能产生λS的足够居民的函数，即 对于所有U使得Γ <$U：s，我们有Γ <$inhΓ（U）：U，并且这个函数在β-约化和稀疏环境下是不变的。范拉姆斯东克和塞维里59[[s]]r=s[[x]]r=xλx：[[U]] r. [[V]] Γ，x：U）inhnf（Γ）（nf（U））[美国] V]] r=C如果U∈PTp且V∈PTd（[[V]] r，x：U）否则，λx：[[U]] r. [[u]] r，x：U）inhnf（r）（nf（U））[[λx：U. u]] r=C如果U∈PTp且u∈PTdλx：[[U]] r. [[u]]r，x：U）否则，（λx：nfβ x（P）. [[v]] r）[[u]] r[[v u]]r=如果Γv：x：P. A和Γu：P[[v]]Γ[[u]]Γ否则，图A.1. 编辑电子书。那么以下陈述成立：(i) 如果r u：U in λS，则[[r]][[u]] r：[[U]] rin λSJ。(ii) 若λSJ是β-强正规化的，则λεS是β-强正规化的。证据注意，根据第二个假设和推论4.12，λS是β-弱正规化的，并且满足类型的唯一性（直到β-转换）。(i) 在推导过程中用归纳法证明了这一点。在乘积规则的情况下，我们需要使用第一个假设。为了输入编码乘积Pmax：P. A的β-redex，我们需要使用一个规则，该规则可能在S中不可用，但在SJ中可用。(ii) 使用前一部分。✷
我的内容管理
展开
