理论计算机科学电子笔记155（2006）169-189www.elsevier.com/locate/entcs弱头规范化Mal-gorzata Biernacka、Olivier Danvy和Kristian Støvring金砖国家1丹麦奥胡斯大学计算机科学系，地址：Aabogade 34，8200 Aarhus N，摘要我们形式化了两个证明弱头正规化的简单类型的一阶最小逻辑演算：一个正常的顺序减少，和一个对象语言中的应用顺序减少随后，我们使用Kreisel关键词：程序抽取，求值归一化，弱头归一化。1导言和相关工作在90年代早期，Berger和Schwichtenberg在证明论环境中引入了通过评估的规范化[5]。Berger然后通过使用Kreisel的修改的可实现性解释[ 10 ]从强规范化的证明中提取它来证实他们的规范化函数[2]在他们自己的研究中，也被证明是通过评估[6，7]进行的规范化，Coquand和Dy-bjer构建了规范化函数，用于解释所谓的胶合模型中的源项。他们还概述了一个“程序提取”的过程，1计算机科学基础研究（www.brics.dk），由丹麦国家研究基金会资助。1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.11.056170M. Biernacka等人/理论计算机科学电子笔记155（2006）169一个n或malization proo的，由于马丁-洛夫，并注意到与伯杰的工作的联系。在本文中，我们使用Berger框架的一部分来形式化Coquand和Dybjer所确定的胶合模型和Martin-Lüf所使用的T_ait_style_p_o_of之间的一些关系。我们讨论了简单类型λ -演算弱头正规化的直观证明：Martin-Loüf的本质正规化的一个正规阶，Hofmann的一个应用正规化的对应[11，152页]。我们的结果可以非正式地描述如下：将修改的可实现性应用于Tait风格的归约谓词的定义，给出了胶合模型的定义。应用修改的可实现性来证明一个特定的简单类型项t的规范化，给出了一个λ项，表示在这个胶合模型中对t我们执行的程序提取可以直观地解释为为了从这样一个规范化证明到一个只返回范式的函数，我们可以删除代表可转换性公理的冗余部分，并相应地简化类型[6]。这就是伯杰在一阶逻辑中使用修正的可实现性解释的工作原理Coquand和Dybjer这并不奇怪，因为我们这里的重点是对证明进行形式化，并考虑对象语言中的两种不同的评估策略，而不是优化提取的程序。我们的帐户有以下限制：• 像Berger一样，我们只是部分地形式化了规范化证明。由于证明的一部分是在元级上进行的，我们不能正式提取一个归一化函数，而只能提取一个λ项，表示对每个特定项t的t的粘合解释。• 为了简单起见，我们只考虑闭项的归一化。有了这个限制，我们不需要形式化绑定变量的重命名• 我们只处理简单类型的λ-演算的情况，其中有一个未解释的基类型，而Coquand和Dybjer考虑了各种更高级的在本文的其余部分，我们首先回顾修改后的可实现性-M. Biernacka等人/理论计算机科学电子笔记155（2006）169171解释（第2节）;然后我们指定λ演算的弱头规范化问题，并提取按名称调用λ解释器，然后提取按值调用λ解释器（第3节）。附录A中给出了所提取的规范化程序的ML实现。2预赛我们首先回顾Berger用于从证明中提取规范化函数的技术[2]。关键概念是Kreisel我们的介绍是基于Berger2.1一阶极小逻辑我们在一阶逻辑M1中形式化了规范化证明。M1的语言是带有合取的多排序一阶最小逻辑的语言，以标准的方式定义。具体来说，这样的语言由下式给出：• 排序i，11，12，.• CONS TANTSCI，FUNCTION SYMBOolsFI1X.. . ×ιn→ι。• Predicat e symbo l sPι1×.. . n.(We将看到M1的种类是提取程序的基本类型。M1的项和公式为：Termsti：=xi|ci|f1×.. . Xn→i（ti1， . . . ，tn）1N对于φ，φ：=P11×... . Xn（t1， . . . ，tn）|φ∧ψ|φ→ψ|你好。 φ|你好。 φ1NM1的一个自然演绎证明系统如图1所示.我们不以图形的方式给出证明规则，而是直接将公式φ的证明定义为依赖类型的λ-项dφ。在定义中，FV（φ）表示公式φ中的自由变量集，而FA（d）表示证明d中的自由假设集。只显示了FA（d）的有趣的定义情况。我们还将使用符号u1：101， . . . . ，un：nM1d：φ表示dφ是集合{u∈1， . . ，un}。1N2.2改进的可实现性在演示文稿中，我们使用Troelstra的修改后的可实现性的变体之一218]。172M. Biernacka等人/理论计算机科学电子笔记155（2006）169（屁股。）uφ（→+）（λuφ.d<$）φ→φ（→−）（dφ→εeφ）ε（+）（−）1（−）2（+）（−）（+）（−）（dφ，e）φ(fst d φ）φ（snd φ）<$（λxι.dφ）<$xι. φ(pr设xi∈/FV（v）为v vvu∈ FA（d））（d∈xi. φti）φ[t/x]t，dφ[t/x][e] φ，u φ.d [φ](pr设x∈/FV（V），和x∈/FV（χ）forrveryvχ∈FA（d）你好φ其中FA（uφ）={uφ}FA（（λuφ.dφ）φ→φ）= FA（dφ）\{uφ}FA（[e. φ，u φ.d φ]φ）= FA（eφx. φ）φ（FA（dφ）\{uφ}）等Fig. 1. 证明系统M1从证明中提取的程序是具有乘积和单位类型的简单类型λ-演算的项，并以M1的排序作为基类型：类型σ：= 1 |ι1|ι2|......这是什么？| σ1× σ2|σ1 ×σ2项t：= x σ|t1 t2|λx σ。不|第一次试验|snd t|（t1，t2）|∗|C|f（t1，.，t n）注意，λ项的语言包括M1的常数和函数符号.此外，范围在λ-项上的元变量用罗马字体（t）表示，因此与M1（t）中的逻辑项的符号不同。在下文中，我们所说的只有在附录A中才是实际的编程语言实现。考虑的问题定义2.1[程序提取]给定φ的M1-证明d，我们定义类型τ（d）和类型τ（d）的λ-项[d]]如下：M. Biernacka等人/理论计算机科学电子笔记155（2006）169173u1111τ（P（t，.，t））：= 1[uφ]：=xτ（φ）1nuτ（φ）：=τ（φ）×τ（）τ（φ→τ）：=τ（φ）→τ（τ）[λuφ.d]：=λ xτ（φ）。[日][dφ→eφ]：=[d]][[e]τ（τx ι. φ）：= i→τ（φ）[[（dφ，eφ）]]：=（[d]，[e]]）τ（τx ι. φ）：= i × τ（φ）[[fstdφ]：= fst[d][[snddφ]：= snd[d][λ x1.d φ]：= λ x1。[日][d]x。 φti]：=[d]t[t，dφ[t/x] n]：=（t，[d]]）[[[是的。φ，uφ.d]]：=[d]][fst[e]/x， snd[e]/xu]然后，利用同构A×1λ= A，1×Bλ= B，A→1λ= 1，1→Bλ= B，隐式化了这些额外项. 2这意味着所提取的项的ypeτ（φ）将要么是1要么根本不包含1。第一个案例当φ是Harrop公式时，我们就可以非正式地说，“has no computational2.2.1提取的可靠性现在我们简单地考虑从φ的证明中提取的λ可实现性的概念被形式化为M1的有限型扩张M−（λ）[2]。每一个字，都是一个字，一个字，都是一个字。M−（λ）。定义2.2[Modified Realizability]通过对M1-公式φ的归纳，我们定义了一个M−（λ）-公式tτ（φ）mrφ如下：t1mrP（t 1，.，t n）：= P（t 1，.，t n）tσ1×σ2mrφ：=（fstt）mrφ（sndt）mrtσ1 →σ2 mrφ→σ：=σyσ1。（ymrφ→tymrφ）t i→σm r φz i。 φ（z）：= φz i。 t z mr φ（z）你好，先生。 φ（z）：=（snd t）mr φ（fst t）给定φ的M1-证明d，因此目标是给出φ的M−（λ）-证明[d]φ。证明d允许包含自由假设Harrop公式[2]在修正的可实现性的原始版本[10]中，以及在更新的变体[4]中，这种“优化”是内置的。174M. Biernacka等人/理论计算机科学电子笔记155（2006）169我们使用更简单的版本用于演示目的。M. Biernacka等人/理论计算机科学电子笔记155（2006）16917511定理2.3（修改的可实现性的合理性）设1，... ，它不是Har rop公式。 Ifu1：01， . . . ，un：n1d：φ，ten1， . . ，n<$M−（λ）[d] φ。证据 标准[2，13]。Q作为一个示例，suppose_hat_d是一个M1-prof_of_x_n。 2. P（x，y）仅将Harrop公式作为自由假设。则定理2.3给出了f λ x ι 1的M−（λ）-pr o。P（x，f st（[d]x））的解。 通过这种方式，自由Harrop假设可以被认为是“ 公 理 ” ， 对 提 取 的 程 序 没 有 影 响 。2.2.2消除计算冗余变量提取过程可以进行改进，以保持所得程序简单。我们提出了Berger[2，3]的一个改进，它允许从提取的程序中消除计算冗余的通用变量为此，我们添加了一种新的公式，形式为{xi}.φ，具有以下引入和消除规则：（λ+）（{λ xi}.dφ）{λxi}. φ(pr设xi∈/FV（v）forveryu∈F A（d））andx∈/CV（d））（v−）（d{vxi}. φ{ti}）φ[t/x]，其中计算相关变量的集合CV（d）被定义为在存在性量化器的见证中自由出现的所有变量的集合，或者在任何术语中实例化d中的泛量化器。一个普遍量化的变量被称为冗余的，如果它不是计算相关的。新公式的实现器的类型简单地忽略了冗余变量：τ（{x i}。φ）：= τ（φ）。修改后的实-i是tmr{txi}。 Φ：=ΦXι。tmrφ（其中x∈/FV（t））。如所期望的，提取的程序不包含冗余变量：[{λxi}.d]]：=[[d][d{t}]：=[d]修改的可实现性的可靠性证明可以扩展到处理这种情况[2]。3弱头归一化我们现在指定λ-演算的弱头部正规化问题。在演示文稿中，我们假设所有术语都是良好类型的，但为了清楚起见，176M. Biernacka等人/理论计算机科学电子笔记155（2006）169我们省略所有的键入注释。 我们只考虑封闭条款。通过归一化，我们理解了将一个项归约为一个标准形式的过程，其中基本的归约步骤是β-归约[1]：（λx.t）s → t [s/x]。β-约化的相容闭包产生一步约化关系。弱头规范化是规范化的一种限制形式，它产生弱头规范形式中的项，对于闭项，它在λ-抽象处停止，而不规范其主体。因此，任何λ-抽象都在弱头范式我们考虑了导致弱头正规形的一步约化的两个确定性限制：正规序约化策略和应用序约化策略。由于弱头规范化与被视为编程语言的λ演算中的求值密切相关，其中计算不在λ抽象下执行，因此我们也将上述归约策略分别称为按名称调用和按值调用求值策略[12]。定义3.1[正规阶归约]正规阶归约策略通过将其限制为以下规则从一步归约中获得：（β）（λx.r）s→r[s/x]r→rJ（v）rs→rJs定义3.2[应用阶约简]（从左到右）应用阶约简策略通过将其限制为以下规则从一步约简获得：（βv）（λx.r）s→r[s/x]如果s是一个值r→rJ（v）（μv）值是λ-抽象。rs→rJss→sJrs→r sJ如果r是一个值这些赋值策略的具体化可以直接在逻辑M1中使用Harrop公式进行公理化，如下节所示。我们要证明的定理可以非正式地表述如下：定理3.3（弱头归一化）减少一个封闭的M. Biernacka等人/理论计算机科学电子笔记155（2006）169177不：Λ不根据上述任一策略的良型λ-项以（弱头）范式终止。证明过程首先在类型良好的封闭项上定义一个合适的逻辑关系接下来，我们证明每一个类型良好的项都满足这个关系。显然，证明的确切形式依赖于所选择的归约策略（正常顺序或应用顺序），因此提取的程序根据对象语言中的相应策略（按名称调用或按值调用）产生结果。在本节的其余部分中，我们首先将这一定理形式化为两种求值策略，然后我们使用修改的可实现性来提取底层程序。在按值调用的情况下，我们的开发形式化并扩展了Pierce书[11]，页。149-152]。3.1客体语言本文考虑简单类型λ -演算的一个显式类型版本，其变量包含在可确定的集合V=xT1，xT2， . . （无限多）1 2每种类型）。 这种语言现在被编码在一阶最小逻辑中。 的变量用于索引逻辑的排序和常量，如下所示：• 排序：对于每个类型T和有限个变量集X，我们有排序ΛX类型T的对象级λ-项包含完全自由的变量X。• 常量：λ-term构造函数是：{x}VARxT（对于每个变量xT）LAMx，T，T，X：ΛX→ΛX\{x}（其中x的类型为T1）1 2T2T1→T2APPT，T，X，Y：ΛX→ΛY→ΛXY1 2T1→T2T1T2• 谓词符号：用于按名称调用和按值调用计算的谓词符号集，我们分别在3.2节和3.3记法。为了便于表达，我们在构建对象术语时使用了许多符号缩写，例如，我们省略了λ-term构造函数的类型注释--在大多数情况下，它们可以从上下文中推断出来;我们使用“uncurried”版本的term构造函数;我们还写LAMxi.t，而不是LAMxi，T1，T2，X（t）和VARxi，而不是VARxi。我们将各种闭项ΛT表示为ΛT。 在本报告所用的公式中，在本文的其余部分，我们只对各种封闭术语进行量化178M. Biernacka等人/理论计算机科学电子笔记155（2006）169我不T2我们用同样的方法来治疗λ-t检验中的小病灶。 对于可变xT1和对数周期sΛT1和tΛT2，我们定义[s/VARxi]，其中每个较小的VARxi不是由s表 示 的LAMxi的系数。 AsΛT1是封闭的λ-t erms的一个排序，由于这种形式的替换，所以从来没有捕获过对象级变量。对于t[s/VARxi]的这个定义，为了忠实地编码替换，我们进一步要求t中的所有自由逻辑变量的范围都在各种封闭的对象级项上。因此，替代的正式定义如下：T1<$<$X定义3.4设xi是一个变量，设sT1 和tT2 是逻辑术语使得t中的所有自由逻辑变量属于（可能不同的）类N个被分类的对象项。我们定义了s或tΛX\{xi}的t[s/VARxi归纳地：∅T[s/VARxi]=y（其中y是逻辑变量）VARxi[s/VARxi]=sVARxj[s/VARxi]=VARxj（j i）APP（t1，t2）[s/VARxi]=APP（t1[s/VARxi]，t2[s/VARxi]）（LAMxi，Xt1）[s/VARxi]=LAMxi，Xt1（LAMxj，Xt1）[s/VARxi]=LAMxj，X\{xi}（t1[s/VARxi]）（ji）3.2按名呼叫评估首先，我们给出了λ-演算中按名调用求值的公理化。我们使用两个基本谓词：Ev（t，s），理解为按名称调用求值的过程是通过以下公理定义的：（A1）{s}。Rd（APP（LAM x i. t，s），t [s/VAR x i]）（A2）{rst}. Rd（r，s）→ Rd（APP（r，t），APP（s，t））（A3）{rst}. Rd（r，s）→ Ev（s，t）→ Ev（r，t）（A4）Ev（t，t）对于所有项t = LAM x i. S第一个和最后一个公理在逻辑项t中是示意性的，它的自由对数变量必须在各种封闭的对象级项上变化。如上所述，这一限制是必要的元水平的定义是正确的替代。这些公理形式上捕捉了这样一个思想，即（按名称调用）求值是上面定义的（正常顺序）一步归约的自反的、传递的闭包归约的概念是β-归约（公理（A1））;它可以应用于yΛM. Biernacka等人/理论计算机科学电子笔记155（2006）16917955到最左边的赎回（公理（A2））产生一个一步还原关系。当达到λ-抽象时，求值停止（公理族（A4））;否则它被定义为一步归约的传递闭包（公理（A3））。在证明中，我们将使用与上述相应公理相对应的自由假设变量A1，A2，A3，A4由于所有的公理都是Harrop公式，这些自由变量将不会出现在提取的程序中3.2.1形式化证明证明中使用的逻辑关系定义如下：Rb（t）：Ev（t，v）RT1→T2（t）：E v（t，v）=0. RT1（s）→RT2（APP（t，s））满足关系式RT的箭头类型的项不仅需要评估为值（或这个更强的条件允许为按值调用和按名称调用求值策略证明所需的定理。如果我们只对基类型的求值感兴趣，一个较弱的条件实际上足以证明按名称调用求值的规范化定理（见3.4节），但对于按值调用的情况，我们仍然需要这个更强的定义。现在我们形式化关于关系RT的三个引理，使用符号pi作为对应于“引理3”的形式证明的证明项i首先，我们立即看到，满足关系RT的每一项都求值为a数值：引理3.5. RT（t）→ λv。Ev（t，v）.证据通过Meta级别上的类型归纳。相应的证明条件是：pb={λt}.λuRb（t）.upT1→T2 ={λ t}.λ uRT1→T2（t）. fstuQ为了证明正规化定理，我们还需要以下两个引理。引理3.6. Rd（r，s）→RT（s）→RT（r）。证据 通过Meta级别上的类型归纳。B案 假设Rd（r，s）和Rb（s）。 根据引理3.5，我们得到了Ev（s，v）180M. Biernacka等人/理论计算机科学电子笔记155（2006）169n+1个从Rb（s）然后利用公理（A3）推导出一个新的公理. Ev（r，v）.对应于这种情况的证明项如下：pb={λ rs}.λ uRd（r，s）vRb（s）. [pbv，wEv（s，vJ）. vJ， A{rsvJ}u w6 53如T1→T2。 假定Rd（r，s）和RT1→T2（s）。 我们得把它弄出来。Ev（r，v）和Et. RT1（t）→RT2（APP（r，t））。第一个条件与基础条件相似。 对于第二种情况，一个包含RT1（t）的值为第一种情况。 由x-iom（A2）得到Rd（APP（r，t），APP（s，t））.接下来，解开RT1 →T2（s）的定义，得到RT2（APP（s，t））。 因此，通过归纳，这些结论包括：RT2（APP（r，t））。以下是该公司的核心内容：pT1→T2 ={λ rs}.λuRd（r，s）vRT1→T2（s）. （pT1→T2，pT1→T2）6哪里六、一六、二pT1→T2 =[pT1→T2v，wEv（s，VJ）. vJ， A{rsvJ}uw六、一、五、三pT1→T2=λ t<$T1zRT1（t）. pT2{APP（r，t）APP（s，t）}（A{rst}u）（sndv sz）六，二六二Q引理3.7对于类型T的任何项t，其中FV（t）={x1，.，xn}，则以下公式是可证明的：→河。 （RT1（r1）） . <$RTn（rn））→RT（t[→r/→x]）（其中，tΛ T是t作为线性代数的编码，并且其中，对于t[r1/VARx1]· · ·[rn/VARxn]，使用抽象通孔t [ → r / → x]）。证据通过归纳法在类型推导上（或者，在t的结构上，由自由变量集参数化）。C aset=VARxT。 O BVIOU S. pVARxi，→x=λ→r→u。乌岛I7C aset=APP（s1T1→T，s2T1）。我们应用归纳法原理，对两个子项进行归纳，得到RT1→T（s1[→r/→x]）和RT1（s2[→r/→x]）.不考虑以下定义RT1→T（s1[→r/→x]）n产生sRT（ APP（s1 ，s2 ） [→r/→x]）（使用 APP（s1[→r/→x]，s2[→r/→x]）=APP（s1，s2）[→r/→x]）。pAPP（s1，s2），→x=λ→r→u.s1，→x→r→u）（s[→r/→xs2，→x→r→u）。7日星期四（小72）（小7C aset=LAMxT1 . rT2（T=T1→T2）。 我们得把那辆车开走。Ev（t[→r/x]→，v）和一个。 RT1（s）→RT2（APP（t[→r/→x]，s））。第一个因素如下所示，从a xom（A4）的（一个非正切）开始，因为（LAMxn+1. r）[→r/→x]是一个λ-α-吸引子。FM. Biernacka等人/理论计算机科学电子笔记155（2006）169181或R182M. Biernacka等人/理论计算机科学电子笔记155（2006）16911第 二 个是RT1 （ s ） 为某 些 人 保 留 的 。通 过 归 纳 hypo-sis ， RT2（r[→r/→x][s/xn+1]）成立. 我们现在正在研究RT2（ APP（ LAMxn+1 ） ）。r[→r/→x]，s）），并利用公理（A1）和引理3.6给出了证明.相应的证明条款如下：pLAMxn+1。 r，→x=λ→r→u。（p，p）七七，一七，二哪里p7，1= n（LAMxn+1. r）[→r/→x]，A4πp=λsΛT1 vRT1（s）。pT2{tt}（A{s}r，→xxn+1（→rs）（→uv）七、二61 21）第7页与t1= APP（LAMxn+1. r[→r/→x]，s）t2=r[→r/→x][s/VARxn+1]Q规范化定理现在可以正式表述如下。理论m3.8对于T型的任意闭合，其中tΛT，Δv。Ev（t，v）是可以证明的证据通过引理3.7，RT（t）是可证明的。因此，根据引理3.5，Ev（t，v）是可证明的。p = pT（ptε ε），5 7其中ε表示空元组。Q3.2.2提取程序由于引理3.7的证明中关于项的结构的归纳是在Meta层次上进行的，所以从定理3.8的证明中我们没有得到一个实现m ula t Λ T的typeΛT→ΛT的优化程序.vΛT. Ev（t，v），而是-对于每一项tΛT-，我们可以传输一个程序图（2）（1）（2）（3）（4）（5）（6）（7）（8）（9）（10）（1我们首先考虑从引理3.7中提取的程序的类型τ（RT（t））（对于s个特殊项tΛT. ）我们认为，类型τ（RT（t））独立于t，并且它们可以归纳地表征τ（Rb）：= Λbτ（RT1→T2）：=ΛT1→T2×（ΛT1→τ（RT1）→τ（RT2））这种归纳刻画定义了一个胶合模型的语义域，类似于Coquand和Dybjer所考虑的那些（相对于M−（λ）的任何特定模型M. Biernacka等人/理论计算机科学电子笔记155（2006）1691837666121让我们引入符号evalt for [[pt]]。从引理3.7中提取的项然后可以归纳地描述如下（它们通过可变量s→x的更新来参数化）：e valVARxi，→x=λ→t→u。ui即APP（r，s），→x =λ→t→u. snd（evalr，→x→t→u）（s[→t/→x]）（evals，→x→t→u）评估LAMxn+1个. t，→x=λ→t→u。（LAMxn+1。 t[→t/→x]，λsv. [[pT]]（evalt，→xxn+1个（→ts）（→uv）与[[pb]=λu.u[[pT1→T2]=λ x. （f stx，λsv. [[pT2]（（sndx）sv））6 6（注意，[[p T]]是βη×-等价于恒等函数。对每一个闭项tΛT，evalt，ε表示由ytΛT表示的任意一个闭项的胶合模解释.从引理3.5中，我们得到了↓b=λu<$b.u↓T→T =λ uΛT1→T2 ×（ΛT1 →τ（RT1）→τ（RT2））。fstu完整的程序是两个函数的组合，因此它是通过求值进行（弱头）规范化的实例[[ptT]]=↓T（evalt，ε）在评价函数的这种表示中，存在两种环境，由s→t和→u的向量表示，其中可以用元素替换r→x的向量中的可变量（通过转换，所有向量的长度相同）。 程序产生弱头范式，根据公理给出的按名调用策略，在这样的情况下，f或mlaEv（t，[[ptT类型T的简单类型项t。]]）在M−（λ）中是可证明的，对于每个闭184M. Biernacka等人/理论计算机科学电子笔记155（2006）16923.3按值调用评估封闭项的按值调用评估过程通过以下公理定义：（A1）{s}。V（s）→ Rd（APP（LAM x i. t，s），t [s/VAR x i]）（A2）{rst}. Rd（r，s）→ Rd（APP（r，t），APP（s，t））（AJ）{\displaystyle {\mathrst}}。 V（r）→ Rd（s，t）→ Rd（ APP（r，s），APP（r，t））（A4）对于所有项t =LAMx i. S与按名称调用的情况类似，这些公理直接编码了一步按值调用评估策略的定义。同样，第一个和最后一个公理在逻辑项t中是示意性的，它的自由逻辑变量必须在各种封闭的对象级项上变化。 然而，为了在按值调用的情况下进行证明，我们需要一种方法来对归约序列的长度为此，我们引入了原始的谓词Rd是一步归约谓词Rd的自反传递闭包。我们使用以下公理来表示Rd：（R1）{t}. Rd（t，t）（R2）{\displaystyle {\frac {2}。 Rd（s，t）→ Rd（t，v）→ Rd（s，v）（R3）（{\displaystyle {R}}. φ（r，r））（{rst}. Rd（r，s）<$φ（s，t）→ φ（r，t））→{rs}。 （Rd<$（r，s））→ φ（r，s）（其中φ是Harrop）公理（R3）是一个归纳公理.通过要求（R3）中的公式φ是Harrop，我们保证公理的每个实例都是Harrop公式。假设另外两个公理(Det){rst}. Rd（t，r）→ Rd（t，s）→ r = s(Val){\fnSimHei\bord1\shad1\pos （ 200 ， 288 ） }V（v）<$Rd<$（v，t）→ t = v为了使用这两个公理，我们用通常的等式公理扩展了逻辑M1（修改的可实现性的可靠性在这种扩展中得到了保留[13]）。最后，我们可以将求值谓词定义为一个缩写：Ev（t，v）：= Rd<$（t，v）<$V（v）.M. Biernacka等人/理论计算机科学电子笔记155（2006）1691853.3.1形式化证明如前所述，证明中使用的逻辑关系被定义为按名称调用的情况，除了现在它可以被细化-通用变量在按值调用下变得计算冗余（我们提前宣布它，但这个观察只能在我们实际写下证明之后才能进行）：Rb（t）：Ev（t，v）RT1→T2（t）：E v（t，v）<${s}. RT1（s）→RT2（APP（t，s））引理3.5的按值调用类似物以同样的方式陈述和证明：引理3.9. RT（t）→Ev（t，v）。为了证明定理3.8的按值调用版本，我们需要更多的求值性质，如引理3.10-3.16所述。引理3.10. Rd（r，s）→ Rd（s，t）→ Rd（r，t）证据使用归纳公理（R3）和公式φ（r，s）={φt}. Rd（s，t）→ Rd（r，t）Q引理3.11. Rd（r，s）→Rd（APP（r，t），APP（s，t））证据使用公理（R3）和公式φ（r，s）={φt}. Rd（APP（r，t），APP（s，t））Q引理3.12. Rd∈（r，s）→RT（s）→RT（r）.证据正如在点名的情况下，一个形式证明是由T上的归纳构造的。Q在证明的按值调用变体中，我们还需要证明公式{\fnSimHei\bord1\shad1\pos（200，288）} 对于每个类型T，Rd∈（r，s）→RT（r）→RT（s）。这是在接下来的三个引理中完成的。引理3.13. V（v）→Rd（s，v）→Rd（s，t）→Rd（t，v）.证据使用公理（R3）和公式φ（s，v）= Rd<$（s，v）<${t}. Rd（s，t）→ Rd（t，v）186M. Biernacka等人/理论计算机科学电子笔记155（2006）169Q引理3.14. V（v）→ Rd（s，v）→ Rd（s，t）→ Rd（t，v）。证据使用公理（R3）和公式φ（r，s）={φv}. V（v）→ Rd（r，v）→ Rd（s，v）Q引理3.15. Rd（r，s）→RT（r）→RT（s）证据利用前面的两个引理，通过T上的归纳构造了一个形式证明Q在主引理的证明中需要另一个关于约简序列的引理：引理3.16. V（v）→ Rd（s，t）→ Rd（APP（v，s），APP（v，t））.证据使用公理（R3）和公式φ（s，t）={φv}. V（v）→ Rd（APP（v，s），APP（v，t））Q引理3.7的按值调用类似于前面的陈述，它的证明依赖于引理3.9-3.16：引理3.17对于类型T的任何项t，其中FV（t）={x1，.，xn}，则以下公式是可证明的：→河。 （RT1（r1）） . <$RTn（rn））→RT（t[→r/→x]）（其中，tΛ T是t作为线性代数的编码，并且其中，对于t[r1/VARx1]· · ·[rn/VARxn]，使用抽象通孔t [ → r / → x]）。证据通过归纳法在类型推导上（或者，在t的结构上，由自由变量集参数化）。我们再次使用符号pi作为对应于“引理3”的形式证明的证明项iC aset=VARxT。 O BVIOU S. pVARxi，→x=λ→r→u。乌岛i17C aset=APP（s1T1→T，s2T1）。就像这种情况一样：我们应用归纳法，通过对两个子项的推导，得到RT1→T（s1[→r/→x]）和RT1（s2[→r/→x]）.在缠绕RT1→T（s1[→r/→x]）的定义时，给出RT（APP（s1，s2）[→r/→xpAPP（s1，s2），→x=λ→r→u.s1，→x→r→u）（s[→r/→xs2，→x→r→u）。17日星期四（p172]）（p17M. Biernacka等人/理论计算机科学电子笔记155（2006）169187n+1个117， 2 9 12 1617，2，1n+1个C aset=LAMxT1 . rT2（T=T1→T2）。 我们得把那辆车开走。Ev（t[→r/x]→，v）和一个。 RT1（s）→RT2（APP（t[→r/→x]，s））。第一个因素从a xi om（R1）开始，连同axiom（A4）的（一个常数），因为（LAMxn+1. r）[→r/→x]是一个λ-α-分式。 对于第二种情况，假设RT1（s）为某些m提供了数据。然后由引理3.9，存在一个v使得Ev（s，v）成立，即，使得Rd≠（s，v）≠V（v）成立。然后根据引理3.15，RT（v）成立。现在，通过对s的归纳，RT2（r[→r/→x][v/xn+1]）成立。公理m（A1）和引理3.12在10 ~ 20 μ M范围内，n=1.25，P= 0.001。 r[→r/→x]，v））。 使用Lemma3.16和Lemma3.12，其中RT2（APP（LAMxn+1））。 r[→r/→x]，s）），其中包括公式。相应的证明项如下（省略一些计算）：为简洁起见，不相关的引理实例化pLAMxn+1。 r，→x=λ→r→u。（p，p ）1717， 117， 2哪里p17，1= n（LAMxn+1. r）[→r/→x]，则R1{（LAMxn+1. r）[→r/→x]}，A4πp={λs}.λe. [（p{s}e）Ev（s，v），f. p（p{s}{v}A4（fstf））p]，其中p = p（R（A）（sndf）r，→x，xn+1（→rv）（→ue）（p{s}{v}（fstf）e））十七，二，一12211）（第17页和第15页Q主要定理也如前所述进行陈述和证明3.3.2提取程序我们再次看到类型τ（RT（t））与t无关。他们描述了胶合模型的域如下：τ（Rb）：= Λbτ（RT1→T2）：=ΛT1→T2×（τ（RT1）→τ（RT2））与前面的情况类似，我们得到的按值调用的程序是从引理3.9中提取的项（与按名称调用相同）和从引理3.17中提取的项的组合。这个词是从引理3.17看起来如下（使用符号evalt表示[[pt]]）：17e valVARxi，→x=λ→t→u。ui即APP（r，s），→x=λ→t→u. snd（evalr，→x→t→u）（evals，→x→t→u）评估LAMxT1. tT2，→x=λ→t→u. （（LAMxn+1）。 t）[→t/→x]，λe. evalt，→xxn+1（→t（↓T1e））（→ue））188M. Biernacka等人/理论计算机科学电子笔记155（2006）169这个程序也线程两个环境，但其中第一个（由向量或r→t表示）在一个简单的环境中运行。 对于闭项tΛT，ε表示由tΛT表示的闭项的胶合模型解释。注3.18在Pierce的书[ 11]中引理3.17的原始公式第151页]，在给定项中，要替换自由变量的项必须是值。然而，这个限制对于证明来说是不必要的，并且所得到的程序与这里得到的程序完全相同。3.4基型闭项的弱头部正规化我们现在展示弱头规范化证明的一个变体，其中我们只对计算基本类型的项感兴趣。为了能够观察程序的行为，我们用整数扩展了对象语言，以通常的方式用零常数0和后继常数S形成。 基本类型的集合现在包括用于整数的类型i。如前所述，对于按名称调用求值，我们可以简化关系RT的定义，从而得到一个更简单的提取程序，我们将在下面展示。我们添加以下两个公理，指定新项的求值策略：（A5）Ev（0，0）（A6）卫星电视。 Ev（t，v）→ Ev（S t，S v）逻辑关系的定义现在对更高类型的限制更少Rb（t）：Ev（t，v）RT1→T2（t）：={s}. RT1（s）→RT2（APP（t，s））定理3.19对任意类型为ι的闭项t，Ev（t，v）成立。该证明几乎像以前一样进行，并且它依赖于引理3.5的基类型版本、引理3.6和引理3.7的基类型计数器部分，引理3.7的基类型计数器部分现在读作如下（注意，项的向量→r是计算上不冗余的（nt）：引理3.20对于类型T的任何项t，其中FV（t）={x1，.，xn}，则以下公式是可证明的：{n→r}。 （RT1（r1）） . <$RTn（rn））→RT（t[→r/→x]）。
我的内容管理
展开
