对称λμ-演算中约化规则的限制及标准化定理

理论计算机科学电子笔记140（2005）101-111www.elsevier.com/locate/entcs对称λμ-演算中约化的若干候选项不起作用的我不知道EquipedeLogique，Universit'edeSavoie73376 Le Bourgetdu Lac，法国卡里姆·努尔EquipedeLogique，Universit'edeSavoie73376 Le Bourgetdu Lac，法国摘要对称λμ-演算是Parigot引入的λμ-演算，其中约化规则添加μ，μ是μ的对称。 我们给出的例子解释了为什么该技术使用通常的候选还原剂不起作用。我们还证明了这个演算的标准化定理。关键词：λμ-演算，归约1引言由于Curry-Howard同构的证明和程序可以推广到经典逻辑中，因此引入了各种各样的系统：λ c-演算（Krivine [11]），λ exn-演算（de Groote[6]），λμ-演算（Parigot [17]），λ Sym-演算（Barbanera& Berardi[1]），λΔ-演算（RehofSorensen&[23]），λμμ-演算-演算（CurrienHerbelin&[3]），λμ -演算-1电子邮件：david@univ-savoie.fr2电子邮件：nour@univ-savoie.fr1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.06.020102R. David，K.Nour/Electronic Notes in Theoretical Computer Science 140（2005）101第一个尊重经典逻辑内在对称性的演算是λSym。它与以前的结石有某种不同，因为主要的连接器不是通常的箭头，而是连接器或和和。微积分的对称性来自德摩根定律。该计算结果表明，该对称性为λμμm。 逻辑部分是（经典的）微积分而不是自然演绎.自然演绎在本质上不是对称的，但帕里戈却提出了所谓的自由演绎[16]，它是完全对称的。λμ演算就是从这里产生的。为了得到一个连续的微积分，在他的终端学中，他必须修正左边的输入为了保持对称性，保留相同的条件，并增加一个新的约简规则（称为μJ-约简），它是μ-约简的对称规则，也对应于消除一个切口。 然后我们得到一个对称微积分，叫做对称λμ-演算Parigot考虑μJ-减少的原因如下。 λμ-演算（具有β-归约和μ-归约）具有良好的属性：非类型化版本中的一致性，类型化演算中的主题减少和但是，从计算机科学的角度来看，这个系统有一个缺点：数据表示的单一性丢失了。众所周知，在λ-演算中，任何N型（整数的通常类型）的项都β-等价于Church整数。这在λμ-演算中不再成立，我们可以找到N型的正规项，教会的整数。Parigot指出，通过添加μJ-约简和一些简化规则，恢复了数据表示的唯一性并且至少对于简单类型化系统，保持了主语归约，即使失去了连贯性。Barbanera Berardi通过使用约简的候选者证明了λSym Yamagata [24]使用了相同一种证明βμμJ-约化的强规范化的技术，其中类型是系统F和Parigot的类型，再次使用相同的思想，将Barbanera Berardi的结果推广到二阶量化逻辑。以下性质在λμ演算中平凡地成立：如果（λxM N P1. P n）D<$（λxM JN JP J. PJ）D（M J [x：= N J] P J. PJ），那么我们可以1n1n通过减少β redex开始减少，即（λxM N P1. P n）D（M [x：=N] P1. P n）D（MJ [x：= NJ] PJ... PJ）。这一点是两个证明中的关键1N这个演算的结果：(1) 如果N和（M [x：= N] P1. Pn）在SN中，则（λxM N P1. P n）。西姆-R. David，K.Nour/Electronic Notes in Theoretical Computer Science 140（2005）101103类似地，若N和（M [α = rN] P1. Pn）在SN中，则（μα MNP1. P n）。它们是类型化演算强规范化证明的基础。(2) 标准化定理。即使这个结果在对称λμ-演算中仍然（平凡地）为真，并且标准化定理在这个演算中仍然成立，(1)上面的话不再是真的。这仅仅是因为（λxM N）的无限约化不一定会减少βredex（对于（μαM N）也是如此），因为它也可以减少μJredex。类型演算强规范化证明的另一个关键点是以下性质，该性质在对称λμ-演算中仍然成立。（3）如果M1，.，M n在SN中，那么（x M1. M n）。本文的组织结构如下。第二节定义了对称λμ-演算及其约化规则。我们在第3节中给出了（3）的证明。第4节给出了（1）的反例。最后在第五节中证明了标准化定理。2对称λμ-演算λμ -项或简单项的集合（记为T）由以下语法定义，其中x，y，.。是λ-变量和α，β，. 是μ变量：不 * *= x| λxT | （T）的 T）|μαT | （αT）请注意，我们在这里采用了比原始演算更自由的语法（也称为deGroote尽管本文只讨论无类型演算，但λμ演算来自逻辑，特别是μ构造函数来自逻辑规则。为了帮助读者不熟悉它，我们在下面给出了类型和归约规则。这些类型是简单类型的λμ-演算的类型，即由原子公式和带有连接符→的常数符号构建。像往常<$A是A →的缩写。类型规则由下面的图1给出，其中Γ是上下文，即一组形式为x：A和α：<$A的声明，其中x是λ（或直觉）变量，α是μ（或经典）变量，A是公式。104R. David，K.Nour/Electronic Notes in Theoretical Computer Science 140（2005）101r，x：AM：Baxr，x：Ax：AΓM：A→BΓN：AΓλxM：A→B→iΓ，α：<$AM：ΓμαM：AeΓπ（M N）：B→eΓ，α：<$A<$M：AΓ，α：<$A（α M）：i图1.请注意，在这里，我们也改变了帕里戈而不是写M：（A×1，...， Axn<$B，Cα1，.， Cαm）我们已经写信1n1mx1：A1，.，xn：An，α1：<$C1，.，α m：<$C m<$M：B削减淘汰程序对应于下面给出的缩减规则。有三种削减。• 当连接词→的引入紧接着是它的消除时，逻辑切割就发生了。相应的归约规则（用β表示）为：（λxM N）DM[x：=N]•当a →e的左前提出现时，就发生了经典割。相应的归约规则（用μ表示）为：（μαM N）DμαM[α=rN]其中M[α=rN]是通过将形式为（α U）的M的每个子项替换为（α（UN））而获得的。• 对称经典割发生在当一个函数的右前提出现时，→e. 相应的归约规则（用μJ表示）为：（M μαN）DμαN[α=1M]其中N[α=1M]是通过将形式为（αU）的N的每个子项替换为（α（MU））而获得的。话在[17]中表明，βμ-约化是连续的，但μμJ和βμJ都不是。例如，（μαx μβy）既可简化为μαx又可简化为μβy。类似地，（λzx μβy）既约化为x又约化为μβy。R. David，K.Nour/Electronic Notes in Theoretical Computer Science 140（2005）101105下面的属性很简单。定理2.1若Γ <$M：A且M D MJ，则Γ <$MJ：A。3如果M1，.，Mn在SN中，那么（x M1. Mn）这些证据只是粗略的。更多的细节可以在[10]中找到，其中给出了简单类型演算的βμμJ定义3.1·cxty（M）是M中出现的符号数。• 我们记为N≤M（resp. N M）N是子项的事实（相应地，一个严格的子项）的M。• D的自反传递闭包记为D。• 如果M在SN中，即M没有无限约化，则η（M）将表示从M开始的最长约化的长度。• 我们用N<$M表示，对于某个MJ，N≤MJ，使得MD<$MJ以及MD+MJ或N MJ。 我们用≤表示n的自反闭包。引理3.2（i）若（M N）D <$λxP，则M D<$λyM1和M1 [y：= N] D<$λxP.(ii) 若（M N）D <$μαP，则要么（M D<$λyM1and M1 [y：=N] D<$μαP）要么（M D<$μαM1and M1 [α = rN] D<$P）要么（N D <$μαN1and N1[α = 1M] D<$P）。证明容易。Q引理3.3假设M，N∈SN且（M N）/∈SN。然后，或者（Md<$λyP and P[y：= N]/∈ SN）或者（Md <$μαP and P [α = rN]/∈ SN）或者（Nd<$μαPand P [α = 1M]/∈ SN）。证明通过对η（M）+η（N）的归纳。Q引理3.4项（x M1. M n）永远不会简化为以下形式的项：λyM。证明通过归纳n。 使用引理3.2。Q定义3.5·设M1，... M n是项且1 ≤i≤n. 我们将表示为M [α = i（M1.. Mn）]的项M，其中形式为（α U）的每个子项都被（α（x M1. M i−1UM i+1. M n））。• 我们将用x表示形式为[α1=i（M 1. M 1），.， α k= i（M k. M k）]。11nk1n引理3.6假设（x M1. Mn）DαM.然后，有一个i，106R. David，K.Nour/Electronic Notes in Theoretical Computer Science 140（2005）101M iD∈μαP和P [α= i（M1. M n）] dM.R. David，K.Nour/Electronic Notes in Theoretical Computer Science 140（2005）101107通过归纳证明n。 使用引理3.2和3.4。Q引理3.7假设M1，.，Mn∈SN且（xM1. Mn）/∈SN. 然后，存在1 ≤ i ≤ n使得MiD∈μα U且U [α = i（M1. Mn）]/∈ SN. 证明设k是最小的，使得（xM1. M k−1）∈SN且（x M1. M k）/∈SN。 使用引理3.3、3.4和3.6。Q引理3.8设M是一项，σ∈ α x.如果M [σ] D <$μαP（resp. M[σ]dλxP），则M D<$μαQ（resp. M D<$λxQ）对于某个Q使得Q [σ] D<$P。证明通过对M.Q下一个引理是定理3.10证明的关键。 虽然直观上很清楚（如果非SN的原因是替换δ = i（P1. Pn），这一定来自某个（δMJ）<$M），它的证明是相当技术性的。引理3.9设M是一项，σ∈ α x.假设δ在M中是自由的，但在Im（σ）中不是自由的。 若M [σ] ∈ SN但M [σ][δ = i（P1. Pn）]/∈ SN，存在MJ<$M和σJ使得MJ[σJ] ∈SN和（xP1. P i−1MJ [σJ] P i+1. Pn）/∈SN.证明见[10]更详细。Q定理3.10假设M1，. M n在SN中。 然后（x M1. Mn）∈SN.证明我们证明了一个更一般的结果。设M1，. M n是术语，σ1，...， σ n在Σ x中。 如果M1 [σ1]，...， Mn [σ n] ∈ SN，则（xM1[σ1]... Mn [σ n]）∈SN.这是通过对（Mi），（Mi））的归纳来完成的。假设（x M1[σ1]... Mn[σn]）/∈SN. 根据引理3.7，存在i使得Mi [σ i] D <$μα U和U [α = i（M1 [σ1]. Mn [σ n]）]/∈ SN. 根据引理3.8，MiD<$μαQ，对于某些Q使得Q[σi]D<$U。 因此Q [σ i][α = i（M1 [σ1]. Mn [σ n]）]/∈ SN. 根据引理3.9，设MJ<$Q ≤ Mi且σj使得MJ [σJ] ∈ SN且（xM1 [σ1]. M i−1 [σ i−1] M J[σJ] M i+1 [σ i+1]. Mn [σ n]）/∈ SN. 这与归纳假设相矛盾，因为（η（MJ），cxty（MJ））（η（Mi），cxty（Mi））。 n0，如果U=U0DU1D... D U n则U p=V对于某个p。• U a V意味着U只有一个redex和U D V。话108R. David，K.Nour/Electronic Notes in Theoretical Computer Science 140（2005）101很容易检查，如果U <$→V（相应地， UaV）且V∈SN，则U∈SN。定义4.2·设M0=λx（xP0）和M1=λx（xP1），其中0=λxλyy，1=λxλyx，P=λxλyλz（y（z10）（z01）λd1Δ Δ）和Δ =λx（xx）。• 设M=<$（xM1），（xM0）<$，MJ=<$（β λx（xM1）），（β λx（xM0））<$，其中<$T1，T0<$表示项对，即项λf（f T1T0），其中f是a新鲜变量• 设N=（α λz（α z））.引理4.3（i）（M1M0），（M0M1）/∈SN.(ii)（M0M0），（M1M1）∈SN.证明(i) 假设i j，则（Mi Mj）d（P P j i）D<$（j（i10）（i01）λd1Δ Δ）d（0λd1Δ Δ）D（Δ Δ）因此（Mi Mj）/∈SN。(ii) 很容易检验（Mi Mi）<$→（1λd1Δ Δ）a（λyλd1Δ Δ）a（λd1Δ）a1.Q提案4.4M [x：= μαN] ∈SN但（λxM μαN）/∈ SN.证明（a）由于M[x：=μαN]=<$（μαN M1），（μαN M0）<$，由定理3.10证明M[x：=μαN]∈SN，证明（μαN Mi）∈SN就足够了.（μαN Mi）aμα（α（λz（α（z Mi））Mi））aμα（Mi Mi）<$→μα（α（α1））（b）第（1）款（λxM μαN）D<$μα（α（λxM λz（α（λxMz）D<$μα（α（λxM λz（α<$（z M1），（z M0）<$）D<$μα（α<$（α<$（M1M1），（M1M0）<$），（α<$（M0M1），（M0M0）<$）<$）D<$μα（α<$（α<$1，（Δ Δ）<$），（α<$1，（Δ Δ）<$）<$）R. David，K.Nour/Electronic Notes in Theoretical Computer Science 140（2005）101109因此（λxM μαN）/∈SN。Q110R. David，K.Nour/Electronic Notes in Theoretical Computer Science 140（2005）101提案4.5MJ [β = rμαN] ∈SN但（μβMJμαN）/∈ SN.证明（a）（λx（x Mi）μαN）有两个赎回，因此，（λx（x Mi）μαN）D（μαN Mi）aμα（α（λz（α（z Mi））Mi））aμα（Mi Mi）<$→μα（α（α1））或（λx（x Mi）μαN）Dμα（α（λx（x Mi）λz（α（λx（x Mi）z）<$→μα（Mi Mi）<$→μα（α（α1））因此（λx（x Mi）μαN）<$→μα（α（α1）），根据定理3.10，可以得出：MJ[x：=μαN]=<$（β（λx（xM1）μαN）），（β（λx（xM0）μαN））<$∈SN.（b）第（1）款（μβMJμαN）D<$μα（α（μβMJλz（α（μβMJz）D<$μα（α（μβMJλz（α μβ<$（β（z M1）），（β（zM0））<$）D<$μα（α μ β<$（β（α μβ<$（β1），（β（Δ Δ））<$），（β（α μβ<$（β（Δ Δ）），（β1）<$）<$）因此（μβMJμαN）/∈SN。Q5标准化在本节中，我们给出了βμμJ-约化的标准化定理。它也适用于μμJ-约化，它的证明只是对另一个约化的限制。定义5.1（i）序列（Mi）1≤i≤n是标准i，满足下列情况之一：(a) 对于所有i，Mi=λxNi（分别为Mi=μαNi，Mi=（xNi），Mi=（αNi）），序列（Ni）1≤i≤n是标准的(b) 存在标准序列（Ni）1≤i≤k和（Pi）k≤i≤n，使得对于1≤i≤k，Mi=（NiPk），当k≤i≤n时，Mi=（NkPi）.(c) 存在一个标准序列（Ni）1≤i≤k和Q使得，或者，对于1≤i≤k，Mi=（Ni Q）且Nk=λxP且Nk−1不以λ开始且Mk+1=P[x：=Q]且序列（Mi）k+1 ≤i≤n是标准的。R. David，K.Nour/Electronic Notes in Theoretical Computer Science 140（2005）101111或者，对于1≤i≤k，Mi=（Ni Q）且Nk=μαP且Nk−1不以μ开始且Mk+1=P[α=rQ]且序列（Mi）k+1 ≤i≤n是标准的。或者，对于1≤i≤k，Mi=（Q Ni）且Nk=μβP且Nk−1不以μ开始且Mk+1=P[β=1Q]且序列（Mi）k+1 ≤i≤n是标准的。(ii)存在标准序列（Mi）1≤i≤n使得M=M1且MJ=Mn。备注和注释• 上面1中的子句对应于有序对（n，cxty（M1））上的归纳定义• 很容易检验，仅限于λ-演算，这个定义与标准归约的通常定义是等价的• 显然，如果MDst MJ，则MD<$MJ。在这种情况下，我们将用lg（MDstMJ）表示约简的长度。引理5.2假设M Dst P和N Dst Q。则：（a）μαM Dst μαP，（b）λxM DstλxP，（c）（M N）Dst（PQ），（d）M [x：=N] DstP [x：=Q]和（e）对于j∈ {l，r}，M [α= jN] DstP [α= jQ]。（a）、（b）和（c）的证明是即时的。(d)和（e）是通过对（lg（MdstP），cxty（M））的归纳和对从M到P的标准序列的定义的直接案例分析而得到的.Q引理5.3假设M Dst P和P D Q。然后是M DstQ。证明通过对（lg（MdstP），cxty（M））的归纳和对约化MdstP的实例分析，证明了这一点.唯一不直接的情况如下：M=（M1M2）D（N1M2）D（N1N2）=P其中M1DstN1和M2DstN2。 如果在PdQ中约化的redex在N1或N2中，则结果如下直接从归纳假设出发。否则，假设例如N1=μαR且Q=R[α=rN2]。设归约M1DstN1如下：M1DstμαR1DstμαR其中μαR1是以μ开始的归约中的第一项。从引理5.2 可以得出，下面的归约是标准的。M= （ M1M2） Dst（μαR1M2）DμαR1[α=rM2]DstμαR[α=rN2].Q定理5.4设M D≠P。然后是M Dst P。用归纳法证明了约化长度MD<$M1.结果直接由引理5.3得出。Q112R. David，K.Nour/Electronic Notes in Theoretical Computer Science 140（2005）101引用[1] F. Barbanera和S.贝拉尔迪一个用于经典程序抽取的对称的可达演算。在M. Hagiya和J.C.Mitchell，编辑，计算机软件理论方面的会议录LNCS（789），pp. 495-515.Springer Verlag，1994年。[2] R.康斯特布尔和C.穆尔蒂在经典证明中寻找计算内容。In G. Huet和G.Plotkin，editors，Logical Frameworks，pp.341-362，剑桥大学出版社，1991年。[3] P.L. Curien 和 H. 赫 贝 林 计 算 的 二 重 性 。 Proc. International Conference on FunctionalProgramming，September 2000，Montral，IEEE，2000.[4] J. - Y. 吉拉德 一种新的构造性逻辑：经典逻辑。 MSCS（1），pp. 255-296，1991年。[5] P. de Groote. 一 个 CPS- 翻 译 的 Escherida-mu-calculus 。 In S. Tison ， 编 辑 ， 19thInternational Colloquium on Trees in Algebra and Programming，CAAP'94，卷787计算机科学讲义，pp. 85-99. Springer，1994年。[6] P. de Groote. 异常处理的简单演算。In M. Dezani和G. Plotkin，编辑，第二届国际会议上类型λ演算和应用，TLCA'95，卷902计算机科学讲义，页。201-215. Springer，1995年。[7] R.大卫标准化而不简化。《纯逻辑与应用逻辑年鉴》（Annals of Pure and Applied Logic），107页。121-130，2001年。[8] R. 大卫和K。努尔简单类型lambda mu演算的强规范化的简短证明。《明史》卷12，页12。2003年第27-34号[9] R. 大卫和K。努尔经典自然演绎的强正规化的一个简短证明。《符号逻辑杂志》（Journal ofSymbolic Logic）68.4页。1277-1288，2003。[10] R. 大卫和K。努尔关于对称的强正规化结果的算术证明λμ-演算参加TLCA[11] J. - L.克里文经典逻辑、存储算子和二阶微积分。《纯逻辑与应用逻辑年鉴》（Annals of Pure andApplied Logic），第68页。53-78，1994年。[12] C.R. 穆尔蒂经典证明的求值语义。 在第六届年度IEEE计算机科学逻辑研讨会的会议记录中，pp。96-107，1991年。[13] K.努尔整个经典的价值在λμ -计算。Archive for Mathematical Logic（36），pp. 461-471，1997年。[14] K.努尔非确定性经典逻辑（λμ++-演算）。数学逻辑季刊（48），pp. 357-366，2002.[15] K. Nour和K.刀全命题经典自然演绎的强规范化定理的语义证明。2004年，曼彻斯特[16] M.帕里戈自由演绎：古典逻辑中的“计算”分析。诉讼计算机科学讲义，第592卷，施普林格出版社，页。361-380，1992年。[17] M.帕里戈λμ-演算：经典自然演绎的算法解释。在人工智能的讲义（624），页。190-201.Springer Verlag，1992年。[18] M. 帕里戈二阶经典自然演绎的强正规化。第八届IEEE计算机科学逻辑年会论文集，pp。39-46，加拿大蒙特利尔IEEE计算机学会出版社.[19] M.帕里戈经典证明作为程序。In G. Gottlob，A. Leitsch，和D. Mundici编，Proc. of 3rd KurtGodel Colloquium，KGC'93，vol. 713 of Lecture Notes in Computer Science，pp. 263-276.Springer-Verlag，1993.[20] M. 帕里戈 二阶经典自然演绎强正规化的证明。 Journal of Symbolic Logic，62（4），pp. 1461-1479，1997年。R. David，K.Nour/Electronic Notes in Theoretical Computer Science 140（2005）101113[21] E. 波罗诺夫斯基替代explicites，logique et normalisation. 博士论文，巴黎7，2004年。[22] W. 是的。 Concuruenceenλ μ-calcul. P h Dthesis，University of C h amb'ery，1998.[23] N.J. M.H.索伦森λΔ演算。In M. Hagiya和J.C. Mitchell，编辑，计算机软件理论方面的国际研讨会论文集，TACS'94，LNCS（789），pp. 516-542. Springer Verlag，1994年。[24] Y.山形二阶对称的Muda-mu演算的强正规化。TACS 2001，计算机科学讲义2215，pp。459-467，2001.