ATS/LF中强正规化的形式化及系统F的简化方法

理论计算机科学电子笔记174（2007）109-125www.elsevier.com/locate/entcs单纯型λ-演算的强正规化的形式化及系统F凯文·唐纳利1，2 和Hongwei Xi1，3美国波士顿大学计算机科学系摘要我们形式化的逻辑框架ATS/LF的Tait的方法的基础上在这种形式化中，我们采用高阶抽象语法来编码简化项和归纳数据类型来编码Tait方法中的简化谓词。与以前的形式化证明相比，所得到的证明特别简单和干净。此外，我们简要地提到如何证明基于吉拉德的方法关键词：逻辑框架，规范化，Tait1引言ATS/LF [4]是植根于应用类型系统[15]的逻辑框架，是ATS编程语言的一个纯粹的完整片段。它使用一种受限形式的依赖类型，其中类型只能由来自有限域的术语索引，其中等式是可判定的（并且也可以有效地推理）。ATS/LF支持使用高阶抽象语法（HOAS）[9]来编码对象语言。HOAS的使用，其中对象变量用元变量和β-归约模型替换来识别，导致特别简单和优雅的编码。 ATS/LF中的有限类型索引语言和强大的证明语言的结合，允许在完全高阶抽象语法上的元定理的归纳证明被直接编码为全1 这项工作部分由NSF拨款CCR-02294802 电子邮件地址：kevind@cs.bu.edu3 电子邮件地址：hwxi@cs.bu.edu1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.01.021110K. 唐纳利，H。Xi/理论计算机科学电子笔记174（2007）109递归函数使用具有否定出现的归纳数据集允许对归约谓词进行编码本文紧接着[ 7 ]中的证明，利用Tait方法给出了简单类型的可积演算（STLC）的强正规化证明一方面，我们使用HOAS来编码非线性项，避免了对这些项进行显式操作替换的需要。另一方面，我们使用一阶抽象语法（FOAS）在STLC中编码类型派生，这方便地支持类型派生的归纳推理。据我们所知，这是第一个使用Tait方法对HOAS定义的对象语言进行强规范化的形式化（或机械化）证明当与文献中强规范化的其他形式化证明相比时，我们的形式化证明的简洁性及其与[7]中简洁而优雅的证明的接近性产生了一些具体的证据来支持ATS/LF中STLC表示的有效性。为了进一步加强这一主张，我们还讨论了对系统F的情况的扩展，基于Girard的约简候选概念形式化了系统F的强正规化的证明我们希望这里开发的技术也可以允许通过逻辑关系形式化其他证明，同时仍然能够利用HOAS。2 ATS/LFATS/LF分为两个主要部分：类型和类型索引语言（称为静态）和证明语言（称为动态）。静态基本上是简单类型的带常数的微积分（但没有递归），静态中的项被称为静态项，静态中的类型被称为排序。有三个重要的内置基本排序：• prop：表示证明类型的静态术语的排序。• int：对静态整数项进行排序。 每个整数都有常量（...，-1，0，1，... ：int）和加法（+：（int，int）→int）和减法（-：（int，int）→int）。• bool：一种静态布尔条件的排序。真值（true，false：bool）和整数上的相等和不等式（=，：（int，int）→bool）有常量。静态常量可以有多个参数。静力学中的等式基本上是β-转换加上Presburger算术，并且它通过转换为βη长范式然后使用整数（不）等式的判定过程（在将布尔项映射到整数项之后）来判定。动力学是一种依赖类型的语言，具有良好的递归，详尽的案例分析和归纳数据库。使用程序员提供的度量检查终止，该度量是表示自然数的静态项的元组，并且根据标准的字典排序在每个递归调用中递减。请参阅[13]了解有关此类型终止检查的更多详细信息。通过要求任何未列出的病例引入K. 唐纳利，H。Xi/理论计算机科学电子笔记174（2007）109111语法：项t∈tm：：= x| λx.t|t1t2|c类型τ∈tp：：= B|τ1→τ2 contextΓ ∈ctx：：=·|r，x：τFig. 1. 单纯型λ-演算“假的，假的。在具体的语法中，proof（函数）声明看起来像：prfun proofName {x1：stx1，.，xn：stxn} .& lt;m1，.，我 的意思是。(p1：T1，.，pl：Tl）：[y1：sty1，...，ym：stym] T =.这个声明是针对一个名为proofName的全递归函数（prfun是引入证明函数的关键字），其类型为：stx1：stx1.，stxn：stxn. （T1，...，T1）→ sty1：sty1，...，Cherylm：stym.T该类型签名由四部分组成。首先，有n个stxi类的静态参数xi，用花括号括起来（把它们看作是通用量化的）。第二，有一个公制单位，附在。lt;和>。，它是表示自然数的静态项的k元组，并且可以包含x1，.，xn.第三，存在l个具有类型T i的动态参数pi，其可以包含x1，.，xn.第四，返回类型由m个存在量化的静态变量yi组成，styi和可以包含x1，...，xn，y1，.，ym.在声明的函数proofName不是递归的情况下，我们也可以使用关键字prfn并不给出度量。请参阅[4，5]中的ATS/LF形成的证明的一些例子3对对象语言进行3.1语法我们证明强规范化的对象语言是STLC，它有一个常数c和一个基类型B。 该语言的语法如图1所示。 我们将使用HOAS在静态数据中对语法进行编码。为了做到这一点，我们为每个语法类别声明一个静态排序。我们从一个sort开始，tm，为对象语言的每个术语构造函数提供构造函数：TMlam：（tm→tm）→tm TMapp：（tm，tm）→tm TMcst：tm对象变量被编码为元变量。 常量TMcst仅在lambda绑定器下递归时在形式化中用作占位符。对象函数由静态中的函数表示，这使我们能够在对象语言中使用元语言中的应用程序术语112K. 唐纳利，H。Xi/理论计算机科学电子笔记174（2007）1091212还原：t1−→t2t−→tJ（REDlam）t1−→tJ（REDapp1）λx.t−→λx.tJt2−→tJ（REDapp2）t1t2−→tJt2（REDapp3）t1t2−→t1tJ（λx.t1）t2−→t1[t2/x]图二. λ-演算的归约规则如果在静态流中对该对象进行了编码，则通过以下方式定义该对象xλx.t' = TMl a m（λx. t这是对象语言的术语之间的组合双射，n个自由变量和具有多达n个自由变量的排序tm的静态项。为了对类型进行编码，我们声明了一个sorttp，对象语言的每个类型构造函数都有构造函数TPbas：tp TPfun：（tp，tp）→tp在一些使用HOAS的编码中，在类型判断的表示中没有明确的上下文表示这种类型判断的高阶表示，如在B.C.[10]中经常使用的，受益于从元语言继承类型上的替换，因此不需要类型替换引理。另一方面，显式上下文的使用允许类型化派生的一阶表示。这一点，以及静态和动态之间的分离，使我们能够直接证明元定理，使用全递归函数，同时仍然利用HOAS的对象语法。必须证明类型派生的替换的不便是次要的，并且不像语法中涉及绑定的问题那样普遍。事实上，在强规范化的证明中，我们不需要在类型化推导上使用替换。类型为ctx的上下文由tm和tp对的列表表示：CTXnil：ctx CTXcons：（tm，tp，ctx）→ctx我们有时可以将CTXcons（t，T，G）表示为（t，T）：：G。实际上，这种排序表示显式类型的替换。一个ctx排序的项只表示一个格式良好的上下文，如果它的tm子项都是不同的元变量。我们将在编码类型化派生时回到这个问题。3.2减少图2给出了纯λ-演算的小步约简规则。Reduc- tion，t−→tJ，被编码为具有类型构造器RED的数据类型：（tm，tm，int）→prop（其中第三个索引测量派生的大小）和一个术语cont。结构体来编码图2中的每个规则。 最有趣的规则是RedlamK. 唐纳利，H。Xi/理论计算机科学电子笔记174（2007）10911312类型形成：τ型► B型（TPbas）► τ1型πτ2型► τ1→τ2型（TPfun）打字：Γt：τ（x：τ）∈Γ双τ型Γx：τ（DERvar）Γ，x：τ1t：τ2τ1型（DERlam）Γt1：τ1→τ2Γt2：τ1（DERapp）Γλx.t：τ1→τ2Γt1t2：τ2图三. Simple-typedλ-演算和REDapp3，它们对应于动态术语构造器：R EDlam：f：tm→t m. fJ：tm→t m。不，不。（x：tm. RED（f x，f Jx，n））→ RED（TMlam f，TMlam f J，n+1）R EDa第3页：f：tm→t m。你好。RED（TMapp（TMlamf，t），ft，0）因为规则本身是一阶的，所以充分性来自于类型索引中的高阶语法对应于正确的项这一事实。最有趣的规则是REDlam：从构造函数的参数中的量化（x：tm. RED（fx，FJX，n））以及在静力学模型中应用代换的事实，我们可以看到fx和FJX表示x的三项是自由的，并且TMlamf和TMlamFJ表示与x由lambda约束。3.3类型分配判断类型的规则如图3所示。我们首先定义上下文查找关系（x：τ）∈Γ。为此，我们使用一个数据类型，带有类型构造函数INCTX：（tm，tp，ctx，int）→prop，其中INCTX（t，T，G，n）表示（t，T）在G中的第n个索引处（缩写为（t，T）∈nG），以及两个对应于规则的术语构造函数：（INCTXone）（t，T）∈0（（t，T）：：G）（t，T）∈nG（t，T）∈n+1（（t′， T′）：：G）（INCTXshi）注意，如果INCTX（t，T，G，n）是有人居住的，那么它的成员是唯一的并且同构于n（因为它是深度为n的无分支树）。我们用一个数据类型来编码判断类型，其中类型构造函数是TP：（tp，int）→prop，术语构造函数表示以下规则（其中我们将TP（T，n）写成nT类型）：►n1T1typen2T2type►0TPbas类型（TPbas）（TPfun）►n+n+1TPfun（T1，T2）型虽然这种类型的构造函数与sorttp的术语具有相同的名称，但没有歧义，因为动态114K. 唐纳利，H。Xi/理论计算机科学电子笔记174（2007）109术语与静态术语严格分离。类型TP（T，n）包含一个同构于T的元素，如果T的大小为n。大小索引用于提供一个度量，以支持K. 唐纳利，H。Xi/理论计算机科学电子笔记174（2007）109115编码打字：Gnt：T（t，T）∈nG <$T型G0t：T（DERvar）STUCT1型（STUCTx. （x，T1）：：Gnfx：T2）Gn+1TMLamf：TPfun（T1，T2）Gn1t1：TPfun（T1，T2）Gn2t2：T1Gn1+n2+ 1TMapp（t1，t2）：T2（DERlam）（DERapp）见图4。 编码打字规则类型的结构。为方便起见，我们定义TP 0（T）n=nat.TP（T，n）（我们将其定义为n=T类型）。类型判断的编码是依赖数据类型DER：（ctx，tm，tp，int）→prop，其中最后一个索引是类型派生的大小的度量。构造函数对应于图4中的推理规则（其中Gnt：T表示DER（G，t，T，n））。变量的类型规则由术语构造函数编码：DERvar：BLOG：ctx. tmd. ：tp. n：nat.（INCTX（t，T，G，n），TP0 T）→DER（G，t，T，0）上下文被表示为一个列表，因此变量查找识别列表中对应于给定变量的索引下面的构造函数编码了一个抽象的类型规则DERlam：D.G.：ctx. f：tm→tm。1：tp. 2：tp. nat. 天然的（TP0T1，天然的） DER（CTXcons（x，T1，G），f x，T2，n））→DER（G，TMlam f，TPfun（T1，T2），n+1）请注意，在这个构造函数的第二个参数中对x的量化（CXX.DER（CTXcons（x，T1，G），f x，T2，n））保证x是一个不出现在G中的元变量，因此如果G是，CTXcons（x，T1，G）是一个良构上下文。应用程序的类型规则由以下构造函数编码：DERapp：DERG：ctx. 第1章：我的天第二章：TM。1：tp. 2：tp.nat1：nat Nat2：nat.（DER（G，t1，TPfun（T1，T2），n1），DER（G，t2，T1，n2））→DER（G，Tapp（t1，t2），T2，n1+n2+ 1）为方便起见，我们还定义了DER0（G，t，T）nat。 DER（G，t，T，n）. 这种类型化派生的表示非常有趣。数据类型DER 0（G，t，T）中的动态项同构于Church-style的简单类型的非线性项，其中变量表示为de Bruijn指标。 上下文G是一个类型化的替换，我们可以将其分解为替换Θ=1，. ..，Tm.数据类型DER0（G，t，T）实际上代表了一个假设的判断，即如果我们有i：Ti的派生（对于1 ≤i≤m），那么我们可以形成► t：T。只要Θ是不同元变量的列表（比如θx1，...，xm），这是通常类型判断x 1的适当编码：T1，...，xm：Tmt：T.我们可以通过这种方式保证上下文在为空或116K. 唐纳利，H。Xi/理论计算机科学电子笔记174（2007）109它出现在作为具有空上下文的一的子派生的派生中。 我们能够证明在空上下文中类型化的术语的强规范化，并且由于允许在lambda下归约，这意味着包含自由变量的术语也具有强规范化4强正规化证明在本节中，我们基于Tait方法[ 12 ]形式化了STLC的强规范化证明形式化的证明与[7]中的证明几乎相同，唯一的例外是我们在[7]中的证明使用变量的某些地方使用常数c 这个异常的直接原因是选择HOAS来表示非线性项（从而使得操作对象变量变得困难）。最后几个引理和强规范化定理的证明在附录A中给出，整个证明可以在线找到http://www.cs.bu.edu/hwxi/ATS/EXAMPLE/LF/STLC-SN-hoas.dats定义4.1[强正规化]项t是有界n的强正规化项，记为SNn（t），如果对于所有tJ使得t−→tJ，对于某个自然数nJ.(tp：TP（T，n），r：R（t，T），rd：RED 0（t，t'））：R（t'，T）=//[case*]的case*r表示穷举模式 匹配| Rbas（sn）=> Rbas（forwardSN（sn，rd））| Rfun{_，T1，_}（fr）=>令prvalTPfun（_，tp2）= tp在Rfun（lam {t1：tm}（r：R（t1，T1））=>cr2（tp2，frr，REDapp1rd））端这个证明函数是一个相当简单的参数编码，它使用TP（T，n）类型的额外参数来提供一个终止度量。这个证明有一个稍微不寻常的功能：Rfun情况绑定了静态参数T1，以便能够为绑定到数组的变量r提供类型。引理4.7（CR 1，3，4）证据通过对τ的归纳，我们证明了CR1，CR3，CR4. CR 3的论证使用了嵌套归纳，CR 4在每个水平上都直接从CR 3得出情形：τ=B.在基类型上的Reduction只是强规范化。CR 1：直接来自RB（·）的定义。CR 3：根据引理4.3。情况：τ=τ1→τ2。K. 唐纳利，H。Xi/理论计算机科学电子笔记174（2007）109119CR 1：设t是Rτ1→τ2（t）的项。 根据CR4诱导假说，Rτ1（c），120K. 唐纳利，H。Xi/理论计算机科学电子笔记174（2007）10911因此Rτ2（tc）。通过CR 1诱导假设tc是SN，并且任何t的减少都会导致tc的减少，因此t是SN。CR 3：设t是中性的，使得对于所有tJ，当t−→tJ时，我们有Rτ1→τ2（tJ）。设t1是一项，使得Rτ1（t1），我们需要证明Rτ2（tt1）。通过CR 1归纳假设，我们知道对于某个n，SNn（t1），并且我们继续通过嵌套归纳，n. t t1是中性的，如果我们证明它所约化的所有项都是可约的，那么我们就可以用CR 1归纳假设得出Rτ2（t t1）。 假设t t1−→t2：t2=tJt1，其中t−→tJ。 我们知道Rτ1→τ2（tJ）和Rτ1（t1），所以我们有Rτ2（tjt1）。情况：t2=t tJ，其中t1−→tJ。 通过CR 2诱导假设Rτ1（tJ），1 1 1引理4.2，SNnJ（tJ）对于某个nJ

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