可在www.sciencedirect.com在线获取理论计算机科学电子笔记300（2014）89-103www.elsevier.com/locate/entcs证明的直觉假言逻辑Gabriela Steren加布里埃拉·斯特伦1，2布宜诺斯艾利斯大学计算机科学系阿根廷Eduardo Bonelli3UNQ和CONICET阿根廷摘要我们研究了一个直观的片段的逻辑证明（LP）的长期分配LP是模态逻辑S4的一种改进，其中断言QA被[[s]]A所取代，其预期的阅读是我们首先介绍了一种基于假设判断的自然演绎法，然后介绍了它的术语赋值，它产生一个连续的和强规范化的类型lambda演算λIHLP。 这项工作是一个正在进行的努力的一部分，以重新制定LP在假设推理方面，以探讨它在编程语言中的应用。关键词：Curry-Howard，逻辑证明，Lambda演算，编程语言1引言本文是我们正在进行的探索谢尔盖·阿特莫夫的逻辑证明LP [ 2，4 ]在编程语言和类型论的基础上通过Curry-de Bruijn-Howard同构的应用的一部分LP是S4的一个细化，其中QA被[[s]]A取代，其预期的阅读是它起源于可证明性逻辑，并且是一种可能的方法来形式化直觉主义逻辑的BHK解释，因为（1）它实现了所有的S4定理;（2）是算术可靠和完备的。LP的一个有趣的特征是它能够反映它自己的推导，在这个意义上，如果公式A是可证明的，那么[[s]]A也是可证明的，其中s编码A的推导。的1这项工作部分得到STIC-AmSud项目12 STIC-04 -“计算机程序和应用的正式开发”和布宜诺斯艾利斯技术研究所的支持。2电子邮件：gsteren@yahoo.com3电子邮件：ebonelli@unq.edu.ar1571-0661 © 2013 Elsevier B. V.在CC BY-NC-ND许可下开放访问。http://dx.doi.org/10.1016/j.entcs.2013.12.01390G. Steren，E.Bonelli/Electronic Notes in Theoretical Computer Science 300（2014）89AB∪关于我们======\{==一一上述探索旨在提出LP的自然演绎表示及其相应的项分配，希望获得在统一设置中同时满足项和类型推导的计算形式主义这项工作增加了以前的结果，我们已经开发[6，10，12]。在这里，我们基于模态逻辑的判断分析[15，16，21]提出了ILP的自然演绎表示，ILP是LP的直观片段，其中包括LP的加证明多项式构造器，并且还探索了[6]的术语分配的变体ILP的判断采用形式Θ; ΓA|s（读“A是真的，有证据证明s在真理假设Θ和有效性假设Γ下”）。它们的意义由适当的公理和推理方案给出。本文的结构如下。秒2介绍了ILP的一种自然演绎表示形式IHLP。然后，我们研究的对应与ILP在第二。3 .第三章。秒4给出了术语赋值λIHLP，然后显示了主题缩减、强规范化和一致性。秒五是做好相关工作。最后，我们总结并提出进一步研究的途径。详情请参阅[25]。2IHLPIHLP的公式和证明证据由以下文法给出：A，B：：= P |A组B组|A组B组|A组B组|[[s]] Ar，s，t：：= xA|vA|λxA.s |s·t|阿斯特尔|fst（s）|新南威尔士B|印度卢比|case r [ x ] .s [ y ] . t|！|! S|L ET B v BEr，s INt |S + t其中P，Q，. 在一组命题变量xA，yA，zA，.上的范围。在一组真值变量和uA，vA，... 一组有效性变量。公式可以是命题变量、蕴涵AB、合取AB、析取AB或模态A。一个证明证人可以是一个真值或有效性变量，一个抽象λxA.s，一个应用程序s·t，一对pxs，tx，投影fst（s）和snd（s），注入inl（s）和inr（s），一个casecaser [x].s[y].t，一个bang！s，一个unboxLET BvA是r，sINt或a +s+t。 我们写A{xA：=r}（ A{vA：=r}）用于捕获避免替换真理（分别）。validity）变量;类似地，对于证明项s xA：=t（resp. s vA：=t）。证明证人s上的有效性FVV（s）和真实性FVT（s）的自由变量是果然下文举例说明了一些定义条款的示例，其中FVT（t，s）取代了FVT（t）FVT（s）。这些定义以明显的方式延伸到公式。FVT（xA）定义FVT（vA）定义FVT（！s）def{xA}∅FVT（s）FVV（xA）定义FVV（vA）定义FVV（！s）def∅{vA}FVV（s）FVT（LETBvAdefBEu，sINt）=FVT（t，s）FVV（LETBvAdefBEu，sINt）=（FVV（t）v}）FVV（s）FVT（λxA.s）defFVT（s）\{xA}FVV（λxA.s）定义FVV（s）判断采用的形式是Θ; ΓA|s，有效性上下文Θ =v1A1，.，vmAm，真值上下文r = x1B1，...，xnBn，A是公式，s是证明证人。我们在空的上下文中写“·”。在判决书中，除了一G. Steren，E.Bonelli/Electronic Notes in Theoretical Computer Science 300（2014）8991►|►|Θ;r，xA |XAVarΘ，vA; ΓA|vAVarMΘ; r，xAB|SΘ;ΓA B| λxA.sΘ;Γ A B|s Θ; r θ A|不EΘ;γ B |s·tΘ; γA|SΘ; γB|不IΘ;Γ A B|阿斯特尔Θ;ΓAB|SΘ;γ A |fst（s）联系我们Θ;ΓAB|SΘ; γB|新南威尔士第二章Θ;γA|SΘ; ΓAB |inl（s）A1Θ;γB|SΘ; ΓAB|印度卢比1000万Θ;Γ A B |r Θ; r，xAC |s Θ; r，yB<$C|不Θ; γC|情况r [x ].s[yBE].tΘ;·θA|sΘ;·s t：AΘ; Γ [[t]]A|！不Θ;Γ θ [[r]] A |s Θ，vA;Γ θC|不QEΘ;r ∈ C{vA：= r}|让B vA成为r，sINtΘ; ΓAsPlusLΘ;γ A |S + tΘ; Γ的tPlusRΘ;γ A |S + tFig. 1. IHLP（1/2）的公理和推理方案除了要求vAi和xBi是不同的之外，我们还要求它们是新鲜的（即，我我它们不会出现在A1，...， Am和B1，...， Bn）。如果一个判断可以用图1中的公理和推理方案来推导，那么这个判断就是可推导的。注意，如果一个判断的导数π Θ;|s是使用这些公理和推理方案获得的，那么s不一定确定π（由于QI，PlusL和PlusR）。大多数这些公理和推理方案是不言自明的。例如，公理VarM指出，如果假设A有效，那么我们可以得出A为真的结论。突出的方案是QI和加的方案。前者是以下简单方案的推广，后者是判断设置中Q模态的标准引入方案的自然明确对应物[15，16，21]。Θ;·θA|sQI0Θ;Γ θ [[s]] A|！S虽然QI0是合理的，但从归一化的角度来看，它并不令人满意的派生。例如，考虑图2左边的导数，其中π1，2是Θ的导数; xA<$B|s和Θ;·θA|t，相应地。 π3是由适当的替换原理得到的。标准化步骤将产生右边的一个。然而，这种推导是无效的，因为在QI0的假设中的证明证据必须与在“！”的论证中的证明证据相同。在结论中事实上，情况并非如此，因为一方面我们有s{xA：=t}，而另一方面我们有（λxA.s）·t。用于模态的引入方案Q1通过获得推导来补救这种情况我一∨QI92G. Steren，E.Bonelli/Electronic Notes in Theoretical Computer Science 300（2014）89π1Θ;xAB|SΘ;·A B|λxA.sπ2Θ;·θ A |t→π3Θ;·θ B |s{xA：= t}Θ;·θ B |Θ;·θ B|（λxA.s）·tΘ; Γ [[（λxA.s）·t]] B|！（（λxA.s）·t）EQI0Θ; Γθ[[（λxA.s）·t]] B|！（（λxA.s）·t）QI0图二、QI0存在时SR失效Θ; r，xAB|s Θ; rθA|不Eq-βΘ;r（λxA.s）·t s{xA：=t}：BΘ;·θA|SΘ，vA;Γ C|不Eq-γΘ; r∈LET BvABEs，（！s）INt t{vA：=s}：C{vA：=s}Θ;ΓA B|RΘ;γA|不等式-ΔLΘ; r（r+s）·t（r·t）+s：BΘ; Γ A B|s Θ; r θ A|不Eq-ΔRΘ;r（r+s）·t r·（s+t）：BΘ; Γ θ [[r]] A|S Θ，vA;Γ C|QΘ; r∈LET BvABEr，（s+t）INq∈ LETBvABEr，sINq+t：C{vA：=r}Θ;Γ θ [[r]] A|不Θ，vA;Γ C |QΘ; r∈LET BvABEr，（s+t）INq∈ s+LET BvABEr，tINq：C{vA：=r}图3.第三章。IHLP（2/2）的公理和推理方案π3Eq-φLEq-φRΘ;·θB|s{xA：= t}Θ;·s{xA：= t}（λxA.s）·t：AΘ;Γ [[（λxA.s）·t]] B|！（（λxA.s）·t）图3中描绘了定义判断Θ; Γεsθt：A的公理和推理方案的示例（完整集合见[25]）。 这些计划是紧密联系在一起的正规化关系的衍生物。事实上，由于LP能够反映它自己的导子，并且这些导子通过规范化而相等，导子之间的导出关系也必须在逻辑本身中形式化。应该指出的是，LP最初是在希尔伯特式的陈述中表述的，这不允许做出这样的观察关于加的方案，它们是LP是多结论逻辑的事实的结果，在这个意义上，证明证人可以证明不止一个公式。事实上，请注意以下在LP中成立：[[s]] A <$[[t]] B <$[[s +t]] A <$[[s + t]] B，因此s + t证明了A和B。在A和B重合的特殊情况下，s+t表示A的两个证明。这种证明的非确定性结合是必要的，以便能够实现IS4的所有定理（参见。第5节）。通过实现[4，Def.9.2]，我们的意思是装饰IS4定理的盒子，使所得公式在ILP中可证明。作为一个例子，我们展示了IS 4定理QA<$QB<$Q（A<$B）如何在IHLP中实现为[s]]A<$[[t]]B<$[[inl（s）+inr（t）]]（A<$B），对于任何s和t。⊃我QIG. Steren，E.Bonelli/Electronic Notes in Theoretical Computer Science 300（2014）8993∨|例2.1设Θ1d=efvA，Θ2d=efuB， Γd=efz[[s]]A[[t]]BΓ1d=efz[[s]]A[[t]]B，x[[s]]A和Γ2d=efz[[s]]A[[t]]B，y[[t]]B，其中两个导数为π1，2：Θ1;·θA|vAΘ 1;·θAθB|inl（vA）Θ1;·θAθB|inl（vA）+inr（t）PlusLQI·;Γ 1π [[s]] A|X[[s]]AΘ1;r1θ[[inl（v）+inr（t）]]（A B）|！（inl（v））+inr（t））QE·;Γ 1<$[[inl（s）+inr（t）]]（A<$B）|L ET B v是s，x[[s]]A 进去！（inl（vA）+inr（t））Θ2;·θB|uBB2[[s]]BΘ2;·θAθB|在r（u）中Θ2;·θAθB|inl（s）+inr（uB）BPlusRQIB·;Γ 2π [[t]] B|yΘ2;r2=[[inl（s）+inr（u）]]（AB）、！（inl（s）+inr（u））QE·;Γ 2<$[[inl（s）+inr（t）]]（A<$B）|L ET B vBEt，y[[s]]B 进去！（inl（s）+inr（uB））最后，对于π3，考虑以下定义r1d=efLETBvABEs，x[[s]]AIN！（inl（vA） +in r（t）），r2d=efLETBuBBEt，y[[t]]BIN！（inl（s） +in r（uB）），以及r3d=efcasez[[s]]A<$[[t]]B[xA]. r1[yB]. R2.π1π2·; r [[s]]A[[t]]B|z[[s]]A<$[[t]]B·;Γ1<$[[inl（s）+in r（t）]]（A<$B）|r1·;r2<$[[inl（s）+in r（t）]]（A<$B）|R2·; r[[inl（s）+inr（t）]]（A <$B）|R3请注意，需要在π1中使用PlusL，在π2中使用PlusR，以便将A的两个替代证明合并为唯一的非确定性证明，并允许在π3中应用BEE。注2.2人们可能想知道，对于蕴涵片断，是否可以在保持所有S4定理实现的同时，省略加号。如果在LP的术语中，允许所谓的非内射指定集和非正规实现，则情况就是这样（参见[18]和[5，Sec.11.2]）。下面的基本结果是通过归纳证明的推导。引理2.3• 如果判断是Θ; r A |s是可导的，那么θ ∈θ J也是可导的;一|S.• （加强）如果判断Θ; r A |s是可推导的，那么判断也是可推导的。θ FVV（s）; Γ FVT（s）A |S.• （真值变量的替换）如果Θ; Γ，xA<$B |s和Θ; r A |t是可导的，那么Θ也是可导的;|s{xA：= t}。• （有效性变量的替换）如果Θ，vA; Γ B |s和Θ;·θ A |t是可导的，则Θ也是可导一一一一E94G. Steren，E.Bonelli/Electronic Notes in Theoretical Computer Science 300（2014）89的;|s{vA：= t}。G. Steren，E.Bonelli/Electronic Notes in Theoretical Computer Science 300（2014）89953ILP和IHLP的关系本节讨论ILP和IHLP之间的关系。我们首先回顾ILP的定义，然后陈述所需的结果，将我们的注意力限制在蕴涵片段上。然后证明了所有的ILP定理在IHLP（Prop.3.1）中都是可导的，反之，所有的IHLP中可导的判断都可以转化为ILP（Prop. 3.1）中可导的判断3.9）。假设给定一组证明常数C且c∈ C。ILP的公式是IHLP的公式，除了证明证人编码希尔伯特风格的证明，并称为证明多项式[2，4]：s，t：：= xA|C |s·t|！S|S + tILP的公理和推理方案如下，其中上下文Γ是形式为xA的假设的集合，并且我们假设4对于公理方案A0-A5的每个实例，C包括至少一个常数：A0. ILP语言中的最小命题逻辑公理。A1. [[t]]AAA2. [[s]]（A B）（[[t]] A [[s·t]] B）A3. [[t]]A[！[[t]]AA4. [[s]] A [[s + t]] AA5. [[t]] A [[s + t]] AR1 Γ<$A<$B和Γ<$A蕴涵Γ<$B。 （MP）R2. 若A是公理A0-A5，且c∈ C对应于A，则Γ<$ [[c]]A.（Neces- sitation）从ILP公式和证明多项式到IHLP公式和证明证人的转换简单地是结构保持映射，其用证明相应公理的IHLP证明证人替换所有出现的证明常数（参见图10）[25]）。一些示例定义条款如下：A0甲乙丙A1t，AA2s，t，A，BA3年代A4s，t，Ad=ef（λxA.λyB.x）d=efλx[[t]]A. 设BvA为t， x在vd=efλx[s]]A<$B.λ y[[t]]A. LETBvABEt， yINLETBwABBEs， xIN！（w·v）d=efλx[[s]]A. LETBvABEs，x[[s]]AIN！！vAd=efλx[[s]]A. 让BvA是s， xIN！（v+t）它自然地扩展到具有以下性质的任何文本： xA∈Γ}。命题3.1如果Γ <$F在ILP中可导，则·;Γ<$F在ILP中也可导|在IHLP寻找一些证据证人。4更一般的假设是可能的。参见[2，4]。CCCCC96G. Steren，E.Bonelli/Electronic Notes in Theoretical Computer Science 300（2014）89defR=ct，As，t，A，Bt，As，t，As，t，A1nA0注3.2在PlusL中，t的真值或有效性变量不需要与上下文Θ和Γ相关。PlusL的另一种推理方案（PlusR也是如此）可能是：Θ; γA |sFVV（t）Δ Θ FVT（s）Δ ΓPlusLΘ;γ A |S + t然而，这个方案不允许命题3.1的证明在公理A4的情况下通过，因为在那个公理中没有先验地对t施加限制，并且QI要求没有真值依赖。通过从语境情态类型理论中汲取思想，也许可以保留上面提出的替代方案[19]。假设r是上下文{xA1，...，xAn}且s = s1，. .sn. 然后我们写[s]] r1N对于上下文{x[[s1]] A1，...，x[[sn]] An}。定义3.3设π是[s]]Γ<$F的ILP中的导子。提取的π的见证，下面记为r，通过π的长度n的归纳法定义。 假设n= 1。则F要么是公理的instance要么是Γ中的hypothesis。在前一个案例中，我们分析了每一个案例：• F=A<$B<$A或F=（A<$B <$C）<$（A<$B）<$A<$C，则r=A B或def A0A、B、C，相应地。• F=[[t]]AA，tenrd=efcA1。• F=[[s]]（A<$B）<$（[[t]]A<$[[s·t]]B），则rd=efcA2。• F=[[t]]A[[！t]][[t]]A，tenrd=efcA3。• F=[[s]]A[[s+t]]A，thenrd=efcA4。• F=[[t]]A[[s+t]]A，tenrd=efcA5。在后一种情况下（即 F是一个hy命题，s ay[s]]Bin[s]] r），我们设rd=ef！S. 对于归纳的情况，我们考虑最后一步的每种可能情况• 这是一个公理或假设，那么我们继续如上所述。• F由公式F1，2使用MP获得。设r1，2是从以F1，2结尾的导数中提取的证明。 Setrd=efr1·r2。• F是从必然性的应用中得到的：F = [[c]] F1，其中F1是公理A的一个实例。 然后我们设rd=e f！cA。下面的结果，通过对[s]]ΓA的归纳证明，说明ILP可以内在化它自己的导子。引理3.4（内在化）设[[s]] Γ A是ILP中的一个可导判断，其导子为π。 [[s]] r ∈ [[r]] A是可导的，其中r是从π中提取的证明。CG. Steren，E.Bonelli/Electronic Notes in Theoretical Computer Science 300（2014）8997λ一让我们写π（ΓA）来表示π是ΓA的ILP-导子。下面的结果显示了演绎引理是如何被内在化的。它的证明依赖于一个名为剥离引理的引理，如下所述引理3.5（λ-抽象）如果[[u]]Γ，y[[xA]]A<$ [[s（u，xA）]]B是可导的，xA∈/Γ，B，则re存在tA<$B（[[u]]Γ）使得[[u]]Γ<$[[tA<$B（[[u]]Γ）]]（A<$B），λ λAB（[[u]]Γ）是A B在[[u]]Γ中的提取证据。引理3.6（剥离）假设π是Γ的ILP-导子，x[[yA]]A<$B，并且yA∈/Γ. 则re是Γ，yA<$BJ的导子，其中reBJre由B，y生成对于每个包含yA的证明项t（包括包含y A的公理的实例的常数），将[[ t ]] A的所有出现替换为A。最后一个结果将需要证明我们的主要结果（Prop。3.9）。引理3.7（替换）Γ<$[[s]]A和Γ，y[[xA]]A<$B和xA∈/r ∈B{xA：= s}。Γ蕴含一个证明证人s是可证的，如果对某些Θ，Γ和A，判断θ; Γ <$A |S是可导出的。从IHLP公式和证明证据到ILP公式和证明多项式的转换如下，其中cA1是表示A1的任何实例的证明常数：Pd=efP（AB）d=efABxAd=efxAs（s·t）d=efs·t⎧⎨[[s٨]]A٨,ifsisprovablevAd=efvAs（！s）d=ef！（s）（[[s]]A）d=ef[[cA1·cA1]]AEscherdef٨As٨（s+t）d=efs+t（LETBv是r，s在t中）=t{v：=r}一个 新的定义AsBsA（λx .s）=tλ（Θ <$r），如果Θ，r s. t. Θ; Γ AB |λx.s可导def·٨ =·AdefAs（Θ，v）= Θ，[[v]]AAdefAs（r，x）= r， [[x]]A（Θ;Γα）|s）d=efΘr[[s]]A注3.8有时候，一个证明证据或一个公式有不止一种可能的翻译（例如，λxA）。（yB+ zB）和[[λxA. （yB+zB）]]AB）。这只会发生在当证据证人的问题，或一些证人在 这个公式包含了抽象概念。通过内化，如果Θ <$$><$<$A<$$>B <$<$是可导出的，则A <$$>B <$在Θ <$$><$中的任何提取的见证t将出现以导出Θ <$$><$<$A <$$>B<$。这意味着t可以在所有可能提取的证人中自由选择。因此，每当一个公式或证明证据在一个推导中出现不止一次，并且存在多个翻译时，它总是可能的。98G. Steren，E.Bonelli/Electronic Notes in Theoretical Computer Science 300（2014）89A B A BCA[s] AAABB{v：=r}在所有案件中使用相同的翻译，以相同的方式选择被提取的证人。如果在每个情况下使用不同的上下文来获得公式/证明证据，我们可以使用弱化来使上下文重合（通过取所有情况下使用的上下文命题3.9对于每一个可导判断Θ; Γ <$A| s在IHLP中，ILP-判断Θ <$$> Γ<$<$[[s <$]]A<$可在ILP中导出。推论3.10如果·;·A |s在IHLP中是可导的，则·[[s <$]] A<$和·A<$可在ILP中导出。4λIHLP我们研究了IHLP的一个术语分配，称为λIHLP，以及在一组术语上的归约规则，这些规则模拟了IHLP中推导的规范化，并解决了主题归约，强规范化（SN）和一致性。IHLP的术语定义如下：M，N：：= xA|vA|（λxA.M B）A B|（M A BNA）|（M，N）|fst（M A B）A| snd(M)|INR（M）|（情况M[x].P[y].Q）|(case M [x ].P [y].Q)| （！M）的|（L ET Bv是r，M（N）A A B B| （百万美元）+Ls）| (s + R N)术语的有效性和真实性的自由变量的定义类似于证明证人的自由变量。字体的装饰通常在安全的地方被省略。对于已经引入的替换概念，我们增加了用证明证人/项替换真值/有效性变量：MB{aA：=NA}和MB{vA：=NA}。类型判断具有形式Θ; ΓMA|S. 图中的打字规则4（通过将项分配给IHLP的公理和推理方案而获得）定义了类型判断何时是可导出的。以下类型[s]]A<$[[t]]B<$[[inl（s）+inr（t）]]（A<$B）的示例项说明了分配给Exm的推导的项。2.1：λz [[s]] A [[t]] B. A [x] A [x] B [x] A [x]设B vA是s，x [[s]] A IN！（inl（vA）+inr（t））[y[[t]]B]。LETBuBBEt，y[[t]]BIN！（inl（s） +in r（uB））备注4.1同样在λIHLP中（如已提到的IHLP），由于QI类型规则，术语不确定完全推导。对于此属性确实适用的变体，请参见第2节中的讨论五、λIHLP-归约被定义为以下两组归约规则的相容闭包。第一组规则，即主要规则，产生于推导规范化的主要情况一G. Steren，E.Bonelli/Electronic Notes in Theoretical Computer Science 300（2014）8999⊃一一LΘ;r，xA<$xA|XAT-VarΘ，vA;Γ，vA|vAT-VarMΘ;r，xA<$M B|sΘ; r M AB|s Θ; Γ N A|不Θ; Γ θ（λx .M）A组B组 |λxT-我.s个字符串Θ; Γ θ（MN） |s·tT-环戊烯Θ;Γ-α|s Θ; r N B|不A组B组T-IΘ;r M AB|S一T-1001Θ;r M AB|SBT-1002Θ; Γ θ M，N θ|阿斯特尔Θ; r=fst（M）| fst (s)Θ; r=0（M）| snd (s)Θ;Γ-α|SA组B组T-101Θ;Γ-B|SA组B组T-102Θ;Γ-谷氨酰胺（M）|inl（s）Θ; r = 0（M）|印度卢比Θ;r M AB|r Θ; r，xAP C|sΘ; r，yB<$QC|不B C BΘ; Γ θ（情况M [x ].P [y].Q）| case r [x ].s[y].tT-环戊烯Θ;·λ A|s Θ;·s θ t：AΘ;Γ θ（！M）[[t]]A|！不T-QIΘ;ΓM [[r]]A|s Θ，vA; rN C|不Θ;Γ（LETBvABEr，MINN）C{vA：=r}|让BvA成为r，sINtT-QEΘ;Γ-α|SΘ;Γ θ（M +L t）A|S+ tT-PlusLΘ;Γ-N B|不Θ;Γ θ（s + R N）B|S+ tT-PlusR见图4。 打字方案β：（λxA.MB）NA→MB{xA：=NA}βQ：LET BvA是r，（！NA）[[t]]AINMB→MB{vA：=NA}ρ1：fst（<$MA，NB <$）→MAρ2：snd（NMA，NBN）→NBδL：l（MA）A <$B[xA].PC[yB].QC→PC{xA：=MA}的情形δR：情况inr（MB）A <$B[xA].PC[yB].QC→QC{yB：=MB}第二组规则，置换规则，产生于规范化的置换他们只是置换所有的术语结构，编码一个实例的消除方案与加号。L：（MAR：（s+RMA <$B）A <$BNA→s+R（MA <$BNA）BA AφL：LETBvABEr，（M[[r]]A+Lt）INNB→（LETBvABEr，MINNB）B{v：=r}+tA AφR：LET BvABEr，（s+RM[[r]]A）INNB→s+R（LET BvABEr，MINNB）B{v：=r}πL：fst（（MA <$B+Ls）A <$B）A→（fst（MA <$B）A+Ls）AπR：fst（（s+RMA <$B）A <$B）A→（s+Rfst（MA <$B）A）AσL：snd（（MA <$B+Ls）A <$B）B→（snd（MA <$B）B+Ls）B一一B100G. Steren，E.Bonelli/Electronic Notes in Theoretical Computer Science 300（2014）89σR：snd（（s+RMA <$B）A <$B）B→（s+Rsnd（MA <$B）B）BκL：case（MA <$B+Ls）A <$B[xA].PC[yB].QC→（caseMA <$ B[xA].PC[yB].QC）C+LsκR：case（s+RMA<$B）A<$B [xA].PC[yB].QC→s+R（caseM A<$B[xA].PC[yB].QC）CG. Steren，E.Bonelli/Electronic Notes in Theoretical Computer Science 300（2014）89101⟨|·|⟩⊃ ⟨||⟩⟨|·|⟩vβ我们要解决的第一个问题是主体还原。引理4.2（主语归约）如果Θ; r ∈ M B|s可导且M B→ NB′，则BJ= B且Θ;|sJ对于某个见证sJ是可导的，使得Θ; r ∈s∈sJ：B。这将是诱人的期望，|s可导且MB→NB，则Θ; Γ <$NB|s也应该是可导出的。然而，事实并非如此。例如，·;·<$（（λxA <$A.x）λyA.y）A <$A|（λxA <$A.x）·λyA.y是可导的，但·;·<$（λyA.y）A <$A|（λxA <$A.x）·λyA.y不是。然而，上述结果适用于具有a！作为他们最外层的操作员推论4.3如果Θ; Γ θ（！MB）A|t是可导的且MB→ NB，则θ;NB）A|不是可导出的。上述结果在使用证明智慧作为证书的编程环境中具有重要意义（例如，参见[12]），所有代码都必须经过证书才能执行。在这种情况下，程序可以被外部！，从而实现完全的对象减少关于强规范化，我们定义了一个从λIHLP-项到简单类型lambda演算λ1，×，+（1表示单位类型）项的映射，它保持了某些约简性质。结果是由λ1，×，+是强正规化的这一事实得出的[22]。该映射将λ IHLP中的类型（公式）和项（证明）与λ1，×，+中的类型和项相关联。它保留了公式的结构，除了模态类型[s] A被映射到其域是单位类型1并且其上域是A的映射（即1）的函数类型的情况之外A）。 正确的一面有效性变量被转换为项变量λ1，×，+。[25]详细内容请见。引理4.4（|·|如果Θ; Γ ≠ M A，|s在IHLP中可导，则|M|：|Θ |⟩ ∪ ⟨| Γ |⟩ ► ⟨|一|在λ1，×，+中可导。2.5张晓波（真值变量替换的交换）对于所有λIHLP项M，N，对于每个真值变量xA：⟨|M|{x|一|：=|N|}=|M{xA：= N}|- 是的虽然，| · |由于有效性变量的替换不对易，因此下面的结果满足我们的目的。引理4.6对于所有λIHLP-项M，N，对于每个有效性变量vA和每个真值变量y1/∈FVT（n|N|）：|M|{x1|一|λ：=λ y1。⟨|N|}−−→|M{vA：=N}|- 是的引理4.7如果在IHLP中M→N而不使用置换规则，则⟨|M |→ +|N |λ1，×，+中的λ引理4.8如果在IHLP中仅使用置换规则M → N，则|M |= |N|- 是的通过以下多项式解释（·）A在N≥2中，使用自然数的标准阶，我们可以显示置换约简的SN102G. Steren，E.Bonelli/Electronic Notes in Theoretical Computer Science 300（2014）89一一012xB=vBd=ef2A A（MC<$BNA）Bd=efMC<$B×NAA A a（λxA.MB）ABd=ef2×MBA AM，Nfst（M）A=snd（M）Ad=ef2×MAA Ainl（M）AB=inr（M）ABd=efMAA A（caseM[xA].P[yB].Q）Cd=ef2×MA+PA+QA（！MB）[[s]]Bd=ef1+MBA A（LETBvCBEr，MINNB）B{vC：=r}d=efNB×M[[r]]B+ 1A A a（MB+t）Bd=ef2×MB+ 2LA A（s+MB）Bd=ef2×MB+ 2RA A引理4.9置换约化是SN。现在我们可以得到λIHLP的SN。命题4.10每一个可分类的IHLP-项都是SN。证据矛盾。假设有一个无穷约化序列从一个可类型化的λIHLP-项M0开始。我们将在这个序列中区分主约简（→B）和伪变约简（→P）。因为根据引理4.9，置换归约是SN，我们的序列必须包含无限个主归约步骤。在任何两个主要步骤之间，可能有0个或更多的置换步骤（总是有限个）。因此P B P B约化序列具有以下形式：M0−→→MJ→M1−→→MJ→M2−→→MJ→···此外，根据引理4.8，|Mi| = |MiJ|每一个i。此外，根据引理4.7，我们知道，对于每个i，|Mi| →+|Mi+1|λ1，×，+中的λ因此，我们可以构造一个无限λ1，×，+-约化序列：|M0| →+|M1| →+|M2| →+···。然而，M0在λIHLP中是可类型化的，根据引理4.2，每个Mi也是可类型化的。 由于映射保持了可类型性（引理4.4），那么我们有一个可类型λ1，×，+-项的无限约简序列这是荒谬的，因为可类型化的λ1，×，+-项的约化是SN。Q最后，由于λIHLP是一个正交高阶重写系统（它没有临界对），并且是左线性的，所以它是连续的。这是从高阶重写中的标准结果得出的[20]。5讨论和相关工作LP通过Curry-de Bruijn-Howard的镜子已经提出了一些有趣的编程习惯。例如，在[6]中，G. Steren，E.Bonelli/Electronic Notes in Theoretical Computer Science 300（2014）89103ee还原历史是该术语的一部分。使用以下方案来恢复受试者减少（如第2节中所讨论的，其对于初始方案失败）。2），e对判断的推导进行编码;|E：Θ;Γ-α|sΘ; r s θ t：A|e EQD M A|S使用高阶重写的技术，从弱归一化推导出所得项分配λI的此外，Church-Rosser定理产生λ I的连续性。请注意，由于术语携带关于如何计算结果的信息（在重写中与L'evylabel一致），CR结果可以被认为是类型化lambda演算的标准CR结果的加强。在[10]中，允许通过引入跟踪变量来检查历史或计算跟踪;这允许演算对基于历史的访问控制[1]和基于历史的信息流[9]进行建模。在这项工作中，提出了QI的以下项赋值，其中Δ是一组跟踪变量（为了检查计算跟踪，最多可以读取一次Θ;Δ;·λ M A|sΘ; Δ;·s θ t：A|e QIΘ; ΔJ;Γj（！ΔM）[[t]] A|！不一个名词的形式！ΔM作为经审核的计算单元运行，其中所有计算都经过审核，并在M内局部范围内。此外，在[12]中，通过将QA解释为A类型的移动代码，LP提出了一种认证移动单元的演算，它用证书（表示类型派生）丰富了移动代码这样的单元采用盒子sM的形式，s是证书，M是可执行文件。组合经过认证的移动单元允许人们从其他移动代码片段中构建移动代码，以及也由其他证书组成例如术语λ a.λ b. unpackatou·，uin（unpackbtov·，vin（boxu·vu·v·））下面写着：“给一个移动单元a和一个移动单元b，从b中提取c o de v ·并证明v，从a中提取c o deu ·并证明u。新证书通过将u·应用于v·来生成u · v ·，并为此生成新证书。最后，包装把这两个人都提升到一个新的移动单位。类型系统确保证书总是对应于它所包含的移动代码与[6]相反，这项工作包括加号，并探索了一个更宽松的术语分配（证明证明等式的推导不包括在术语分配中）。放松术语赋值的原因是将分析的重点放在加号上，从而简化它所操纵的术语。话虽如此，根据目前的初步结果，加号的主要作用是它本身的类型，如Exm所示。2.1.它似乎没有运行时效应。然而，需要做更多的工作，以获得更深入的了解。104G. Steren，E.Bonelli/Electronic Notes in Theoretical Computer Science 300（2014）896结论我们研究了ILP的一个自然演绎表示，它是LP的一个直觉片段，以及它相应的项赋值，它是第一作者已经介绍过的并在前一节中讨论过的主体还原、强规范化和连续性的基本性质很容易证明是成立的。我们认为，在IHLP的背景下实现IS4的新面貌可能是一个有趣的探索途径。应该注意的是，这是一个非平凡的问题，在推理方案的存在下，混合极性，如EEE，因此，第一个这样的证明[2，4]依赖于LP的无割微积分表示。事实上，所有已知的（作者的这项工作）实现的证据依赖于演示文稿，其中相关的5次出现的Q不发生在积极和消极的立场。我们认为，将成熟的类型推理技术投入工作可能会很有趣，但只是推断盒子的装饰，而不是推断类型。在此过程中，可能会出现更高阶的统一关系。在[7]中，发展了所谓的基本直觉主义证明逻辑引入了一个形式为[u]]A的模态，其中u是一个证明变量，并给出了关于该模态的一些公
我的内容管理
展开
