在线获取理论计算机科学电子笔记319（2015）103-119：聚焦线性逻辑与λ演算

可在www.sciencedirect.com在线获取理论计算机科学电子笔记319（2015）103-119www.elsevier.com/locate/entcs聚焦线性逻辑与λ演算Taus Brock-Nannestad陶斯布罗克-南内斯塔1，3INRIASaclayLIX，E'colePolytechniqueNicolas Guenot尼古拉·格诺2，4哥本哈根IT大学摘要线性逻辑具有继承自经典逻辑的强对称性，同时提供了一个可与直觉主义逻辑相媲美的构造性框架。然而，线性逻辑的微积分表示的计算解释仍然存在问题，主要是我们解决这个问题，提供一个简单的解释集中的证明，一个完整的子类的线性证明有一个更强大的结构比标准的线性逻辑演算。 尽管经典的设置，解释相关的证明，以一个细化的线性λ演算，我们调查其性质和关系，其他演算，如通常的λ演算，λμ演算，以及它们的变种的基础上，λ演算。关键词：线性逻辑，聚焦，λ演算，Curry-Howard对应1介绍在直觉主义自然演绎与简单型λ演算之间的Curry-Howard对应中发现的“证明作为程序”的思想是一个强大的叙事，导致函数式编程的发展，其表达类型系统和程序行为的强有力的保证。在经典逻辑的基础上，已经提出了许多变体和扩展，例如λμ-演算[20]。在围绕逻辑系统的计算解释的许多发展中，线性逻辑[11]已经占据了重要的位置，这一领域提供了一个精炼的观点，逻辑和它们的计算意义。然而，它主要被视为一种工具，一种方法论的工具[3，14]，而不是1电邮地址：taus. inria.fr2电子邮件：ngue@itu.dk3由ERC Advanced Grant ProofCert支持。4由丹麦战略研究理事会向Demtech项目提供的赠款10-092309支助http://dx.doi.org/10.1016/j.entcs.2015.12.0081571-0661/© 2015作者。出版社：Elsevier B.V.这是CC BY许可下的开放获取文章（http://creativecommons.org/licenses/by/4.0/）。104T. Brock-Nannestad，N.Guenot/Electronic Notes in Theoretical Computer Science 319（2015）103比计算解释的对象，至少在其标准形式-它的直觉变体已被用来描述线性λ-演算[7]。问题在于描述它的λ演算的框架，它的结构太松散，不能方便地通过任何类型的λ项来表示。这个基本问题从一开始就使用证明网的形式主义来解决，被描述为线性逻辑的自然演绎[11]，但这是对传统证明语法的根本背离，意味着使用图形作为表示，以某种方式来编写程序。保持证明树的标准语法需要改变所考虑的程序类型，并且已经提出了基于模式匹配[22]或过程[1，6，23]的解释。在另一种情况下，聚焦[4]已经被开发出来，通过识别具有强结构的证明的完整子集来改进线性逻辑中的证明搜索。随着这种范式的详细研究，很明显，极性的概念和相关的可置换性属性导致了聚焦系统是线性证明理论的一个重要方面[15]。然而，线性逻辑的聚焦演算，就像它的非聚焦变体一样，并没有出现在库里-霍华德传统中作为直接计算解释的选择框架在本文中，我们提出了一个简单的解释，最标准的重点介绍MELL，显示如何结构的重点证明可以描述的细化线性λ项中发现的直觉设置，尽管连接。这种解释的关键是使用显式极化的语法，其中负公式类型计算，而正公式类型值，如按推值调用框架[17]中所做的那样此外，我们考虑一个强集中的系统，其中反转是最大限度地进行，并在一个有序的方式，从而产生正常的形式，其中没有两个推理规则的实例可以置换，但整个集中的阶段仍然可以置换。我们称之为λπ的演算没有显式的控制运算符，但它的类型系统允许通过相对简单的转换来编码带有控制的演算，例如λμ。我们在第2节中提出了MELL的集中证明系统以及一个术语分配，并讨论了它的基本性质。在第3节中证明了两个基本结果，割消和聚焦，我们讨论了这两个定理的计算解释，当把它们的证明看作λπ-演算中的项的变换时。削减的减少，在大的步骤中完成，对应于减少的预期概念聚焦对应于项的重组，通过重新排列其子项的位置来简化项的结构，合并先前被不相关的计算阶段分开的值。最后，我们在第4节讨论λπ-演算的表达性，通过考虑片段和已知演算到这些片段的编码。特别令人感兴趣的是简单类型的λ演算和λμ-演算与其起源密切相关，T. Brock-Nannestad，N.Guenot/Electronic Notes in Theoretical Computer Science 319（2015）103105►►►B► Γ， Δ，A<$B演绎请注意，λπ有丰富的结构：它是λμ的一个基于序列的变体，带有线性的概念，其中的项可以应用于树而不仅仅是参数列表。我们在第5节中总结并讨论进一步的研究，从概括到更丰富的逻辑到实际适用性。相关工作。如前所述，“经典”线性逻辑的标准系统的计算意义关于直觉逻辑中聚焦的详细描述，以及证明项，可以在[21]中找到。在经典环境中，对λμ演算[9]中的计算的研究导致了一个称为L的系统，该系统以对称的方式提供了扩展λμ演算的语法，并且该系统已经在线性环境中进行了研究[19]。然而，该系统一般不集中，并且不能全部消除切割，执行选择要集中的公式。相关的还有极化线性逻辑的工作[15]，特别是在极化证明网中编码λμ演算[16]。我们将在第4节讨论这种联系。2聚焦证明与线性λ-项聚焦可以被看作是一种构造证明的方式以线性逻辑乘法部分的标准规则为例−−−−► 一个一个一► Γ，A，B−−Γ−，−A−Γ，AΔ，B−− − − − − − − −这个片段中的证明除了子公式关系所强制的结构之外，几乎没有什么结构。聚焦使我们能够以两种方式加强进一步的结构。首先，引入连接词的规则是可逆的（即结论隐含前提），因此我们可以假设这种反演性质总是在证明中最大限度地应用。换句话说，如果在剩余的上下文中有，则没有分解。第二，也许是最重要的一点是，可将矩阵的分解重新排列成矩阵-分解的极大链。请注意，该规则是不可逆的，因为它要求线性上下文被分成两部分，并且这种划分可能事先不知道。 因此，分解，比方说，A（BC）的结果在分别包含A和B的子导子中，在聚焦法则中，我们要求B_（10）C也立即分解我们通过将同步器分成两部分来强制反转（或异步）和链接（或同步）阶段的最大化。在求逆过程中，我们维护了一个潜在可逆公式的列表，并且总是分解这个列表的第一个元素。如果最上面的连接词是a，我们将两个子公式放回列表中，否则我们将公式移到列表的另一部分。通过这种方式，我们确保上下文中的每个公式都被分解，如果可能的话。在链接阶段，我们维护一个包含单个公式的stoup，称为“焦点”。当分解一个子公式时，两个子公式被放在前提中的这个stoup中，从而确保这些公式被依次分解，如果可能的话。我们考虑线性逻辑的乘法指数片段[11]，106T. Brock-Nannestad，N.Guenot/Electronic Notes in Theoretical Computer Science 319（2015）103−x−;−x−：−a−−at-1-Nt;r，x：↑AS►↑⇓ ↓−− − −− −− − −−[t;ΓN−−−−−− −−−−− − −−−−−λx.t; Γ↑A，S−t−−p−t;rN，Sp;ΔN► ; Γ，Δ−− − − − − − − − − −−p; rPxp;r，x：↑P·....................................................................−−−−−−−−−−−−−π。−t−t; rN，M，S−p;ΓPq; ΔQ- −► [医]甲状旁腺素M、S....................................................................（p，q）; Γ，ΔP<$Qλ−！X. t− −t，x：？P; rS−−−t;·N► 是吗？P、S- -−− − − − − −−p，x：？P;Γ-P！你好！N−− − − − − − − − − −−−！xp，x：？P; I;Fig. 1. 具有λπ项的聚焦MELL的推理规则纯线性连接词还 有 指数模式还有！以及明确的极性变化↑和↓-作为正负之间的线性中介[15]。我们还假设给定一个可数原子集ffi，它被划分为使得任何原子a在ffi中有唯一定义的负对应原子a。 语法在MELL的这种极化变体中的公式被分为两类：P，Q：：= ↓a| ↓N|PQ|！NN，M：：= ↑a| ↑P |NM|什么？P其中P和N分别表示正公式和负公式。对偶（·）的概念将a和a之间的关系扩展到所有公式，在线性逻辑中通常定义。请注意，在我们的语法中，原子总是在极性转换后立即出现：这是对偏置的解释，即对给定原子极性的选择。因此，极化公式包含所有所需的极性信息。在下文中，我们用↑A表示↑a或↑P，用↓A表示↓a或↓N。上面图1中所示的微积分是MELL聚焦系统[4]的标准三元形式，通过使用极性变化变得更加精确它对两种序列进行操作：⎧⎨⎩► ; Γ► ; Γ其中，x和r是包含命名公式的多集，记为x：？P和x分别为↑A。像往常一样，我们假设这些公式中的变量是不同的。列表S可以是空的，并且表示在反转阶段中处理的上下文的部分，而另一个列表中的P是在聚焦阶段中分解的正-关于这个系统的更多细节可以在[4]中找到。请注意，公式中有弱化和收缩，因为它们是指数的。图1中的微积分带有一个术语赋值：它是T. Brock-Nannestad，N.Guenot/Electronic Notes in Theoretical Computer Science 319（2015）103107线性λ演算将项与值分离。考虑到专注于计算的已知影响，这种区别并不奇怪[10]，但是直接类型化通过线性逻辑的“经典”证明来证明λ事实上，尽管直觉线性逻辑已经通过线性λ-项[7]解释，但在微积分中使用的标准线性逻辑只与过程[6，23]或模式匹配[22]有关。这是一个说明的能力，focalisation阐明的计算意义的证明，在微积分。我们将用于表示聚焦MELL证明的语言称为λπ-演算：它可以被看作是Herbelin [12]提出的代表LJT证明的λ-演算的线性变化。然而，它使用对和解对运算符π，而不是参数列表术语和值的语法是：t，u：：= λx.t |XP |TP |π .t |λ！X.T|！xpp，q：：= x| [t|（p，q）|！不其中t和p分别表示项和值。 除了具有用于抽象和应用的构造之外，λπ-演算的特征是将项转换为值，例如在call-by-push-value[17]中可以找到。此外，由于核心语言是线性的，λπ具有抽象、变量应用和形实转换程序构造的复制变体。 证明和术语之间的关系是紧密的：在MELL覆盖的片段中存在一一对应。高度对称逻辑的证明和相对标准的λ演算之间的这种强联系是通过聚焦获得的额外结构而成为可能的身份扩张。在线性逻辑中，适用于复合公式的恒等公理的更一般形式在这个系统中是容许的。 然而，由于极化设置，这需要精确定义负公式N的展开，用N表示，定义如下：（↑A）<$= ↑A（NM）<$=N<$，M <$ （？P）=？P因此我们可以通过扩展将任何N与持久上下文和线性上下文（r， r）的对联系起来。在下文中，我们写[r|对于包含在r中的公式集。现在我们可以用一个相互归纳法证明下面两个引理，证明恒等式公理的推广。引理2.1数列;x：↑PP和，x：？P;·P是可证明的。证据在第一种情况下，我们可以急切地分解P，直到我们得到一个形状为Ω， Ω;Γ，x：↑P，Ω·的前提，并专注于P，因此我们得出引理2.2。另一种情况以同样的方式处理，但使用指数焦点规则。Q引理2.2（恒等式展开）如果N =[π，Γ|然后我们有，Ω; Γ <$N<$。证据我们用归纳法来推导公式N.在基本情况下，N的形状为↑a，我们使用公理规则得出结论。在一般情况下，如果N的形状M L，我们适用于M和L的归纳假设分别和合成的证明使用的规则。如果N的形状为↑P或？P，然后我们使用引理2.1对P进行推论，并且使用↓规则或统治Q最后一个引理的直接结果是，恒等式公理现在可以108T. Brock-Nannestad，N.Guenot/Electronic Notes in Theoretical Computer Science 319（2015）103► ⇑ ►⇓归纳为以下两条规则：==x;x：↑P↓P===！x，x：？P;·！P（一）如果添加这样的规则，我们可以键入本质上不是η长的项。此外，恒等式扩展的证明为我们提供了一种与η-扩展相当的项转换规则是：x→η[λz]。（x z）如果x：↑↓N，则为x→η[π.λy.λz.x（y，z）<$if x：↑（P<$Q）x→η[λ！z. （x！z）如果x：↑，则为零！N！x→η！λz。（！xz）if x：？↓N！x→η！π λ y λ z ！x（y，z） 如果x：？（P/CN.9/2004）！x→η！λ！z. （！x！z）if x：？！N当把引理2.2的结果分解成小步骤时。 在下文中，我们将只考虑η-long范式中的项，也就是说，上面的规则都不适用，因此对应于原子恒等式公理的证明3削减消除和聚焦作为转换我们现在转向系统的动力学，通过考虑证明变换及其对相应项的影响像往常一样，割消被解释为实现计算的重写系统，在我们的系统中，聚焦结果也被解释，对应于简化λπ项的重组。在聚焦微积分中，割消通常表现为割规则集合的可容许性切割缩减的步骤包括使切割与直接出现在其上方的规则交互，或者置换所述规则上方的切割，或者将切割分解成更小的实例。然而，这种呈现方式有几个缺点。首先，“交换割”没有计算意义，并且仅用于置换推理规则，直到下一个计算步骤可以发生。此外，削减的这种小步性质几乎总是导致相关的削减系统无法实现强有力的正常化。由于我们对削减消除的动态感兴趣，我们将选择一个非常保守的观点。我们建议只有一个相关的cut规则实例，如图1所示：; ΓN，S−− − − − − − − − − − − − − − − −► ; Γ，Δ注意，因为微积分强制最大同步和异步相位，公式N和N都是前提中的主要公式。换句话说，这条割规则恰好代表了割消论证的主要情形为了处理主公式没有被分解的情况，我们将具有非主公式的派生看作是上下文和再次是主的子派生的组合。为了可读性，我们暂时省略了证明项：在本节的后面，我们将展示一组约简，T. Brock-Nannestad，N.Guenot/Electronic Notes in Theoretical Computer Science 319（2015）103109形成以下定理的计算内容。为了便于记法，我们使用;Γ作为;ΓP或;ΓS的简写。第一步是基于导子结构的实例分析证明一系列分解引理。我们省略了最基本引理的证明，涉及形状为↑a的公式。引理3.1（原子分解）对于任何证明E：：; Γ，x：↑a，存在从; x：↑a ↓a到; Γ，x：↑a的开导子G。引理3.2（线性分解）任何导子E：：;Γ，x：↑P可以分解为导子F：：，Ω;ΔP和开导子G，► ，Ω; Δ的！ 在开放假设和结论之间的规则。证据证明过程是通过对导数E的归纳进行的。如果E以一个规则结尾，该规则在其前提中不关注x：↑P，则我们将该规则置于开导子G之上。如果规则关注x：↑P，那么这就是期望的求导F，我们就完成了。在任何时候我们都不会遇到！规则，因为这个规则需要一个空的线性上下文，这是不可能的，因为x：↑P的存在。Q要求G不包含！ 规则很重要，因为它 只是将线性上下文均匀地扩展到开导数上：如果G是满足要求的从Ω，Ω; Δ，Φ，Ω;到Ω，Ω; Γ，Φ，Ω;的开导子，则它也是从Ω，Ω; Δ，Φ，Ω; Γ，Φ，Ω;的开导子。当公式的形状？P，并且在持久上下文中以x的名义出现，我们定义多重性|X|Eof x in a derivation E as number of times x：？P是E中焦点规则中的principal-在x上开始了多少个焦点阶段。这需要考虑模α-等价的通常概念的证明引理3.3（持久分解）对于任何证明E：：n，x：？P; Γ，则要么我们有E：：;Γ，要么存在导子F：：，Ω;ΔP和从， Ω; Δ·到，x：？P; r = 0，使得|X|G<|X|E.证据同样，我们在给定的导子E上通过归纳法证明了这一点。直觉上，我们使用x：？P，得到导数F。剩余的导子，其中x必然具有较低的重数，则成为G。Q在这些分解引理的基础上，我们可以完成我们的割消论证。 我们在这里简单地将其陈述为弱规范化论证，尽管我们期望微积分也承认强规范化论证，因为它与线性替换微积分相似[2]。定理3.4（剪切消除）以下两个剪切原则适用于MELL，假设衍生物D和 E是自由切割的：(i)若D：：;ΓP，S和 E：：;ΔP，则存在 F：：;Γ，ΔS，(ii)如果D：：n，x：？P;Γ <$S和E：：<$N;·<$P <$，则存在F：：<$N; Γ <$S.证据第一个陈述是通过归纳P的结构而建立的。请注意，通过设计，P和P必须是假设中的主要因素，因此110T. Brock-Nannestad，N.Guenot/Electronic Notes in Theoretical Computer Science 319（2015）103JJ公式的结构也迫使D和E中的最终规则必须是什么派生• 如果P=Q，则R：D第一季第二集► ;Δ1QR−− − − − −−⊥− − −−⊥− −−− − − − − − − − − − − − − − −−►Ψ; Γ⇑QR,S►Ψ;Δ1, Δ2⇓Q⊗R我们需要构造一个导子F：：Δ 1，Δ 2Δ S。 我们通过在D和E1上应用归纳假设来获得DJ：：R; Γ，Δ 1<$R，S，然后再次在D和E2上应用归纳假设来产生所需的推导R; Γ，Δ 1，Δ 2<$S。• 如果P=↓a：D► ; r，x：↑a−− − − − − − − − −−► ;−− − − − − − − −► ;y：↑a其中第二个推导是强制的，因为语法不允许原子没有一个极性的转变我们需要构造一个推导F：：;Γ，y：↑aS：如果我们只对可证明性感兴趣，我们可以简单地重用D。 为了使项约简的行为符合预期，我们改为如下推理：通过在D上应用引理3.1，我们得到一个开导子G，它是从Ω，Ω; x：↑a ↓a到Ω，Ω;r，x：↑a S，我们将它与E组合以产生期望的结果。• 如果P=↓Q↓：D► n; r，x：↑QS−− − − − − − − − − −► ;E► ; Δ−−−−−−−−−► Q; ΔQ ↓Q我们需要构造一个导子F：：Δε; Γ，Δ εS。通过在D上应用引理3.2，我们得到了一个导子D J：：，Ω; Γ jQ和一个从，Ω; Γ J·到;ΓS的开导子G。然后通过对D J和E的归纳假设，我们得到了一个关于D j，Ω; Γ J，Δ τ·的导子，并将它与G合成，得到一个关于D j，Ω; Γ，Δ τ·S的导子. 注意，线性上下文已经从Γ J变成了Γ，Δ，但是线性上下文的这种扩展是在开导数上一致完成的，因此不是问题。• 如果P=！Q：D► x：？Q;rS−− − − − − − − − − −► 是吗？Q、SE► ;·−−−−−−−−► 你好！Q我们可以直接将第二个归纳假设应用于D和E。对于第二个陈述，我们通过多重性的归纳法进行|X|D的x：？P在D中。给出以下两个推导：D► x：？Q;rSE► ;·E：⊥⊥T. Brock-Nannestad，N.Guenot/Electronic Notes in Theoretical Computer Science 319（2015）103111我们需要构造一个导子F：：r; rS。通过将引理3.3应用于我们可以从下式获得导子DJ：：Ωi， Ω i，Δi，Q和开导子G：► ？？Q; r∈S。 通过D j和E上的第一个归纳假设，我们产生了一个导数，Ω;Δ·，并将其与G合成，以获得一个导数，x：其中x具有较低的重数，最后通过应用第二个归纳假设，我们得到所需的导子。Q为了描述引理和割消证明所指定的过程的计算行为，在λπ的语言中，我们分别为项上下文和值上下文引入以下符号T：：= −| λx.T|XV| Tp|电视|π.T|λ！X.T|！xV V：：= 0|[T|（V，q）|（q，V）|！不我们使用这个定义来给出两种上下文，这取决于“洞”是−还是−。我们用Tt和T [p]分别表示用t和p替换−和的结果，其中括号中的差异表示要使用哪种孔。分解引理现在可以根据上下文来陈述推论3.5（项分解）良型λπ-项是这样的：(i)一个包含一个自由的线性变量x的项t可以被分解为上下文T − t和一个值p，使得t=T x p，或者分解为上下文T[t]，使得t=T [x]。(ii)对于一个项t和一个自由指数变量x，要么x不出现在t中，要么t可以被分解为上下文T − t和值p，使得t = T！xp。当约简项（λx.t）[u]时，我们首先将t分解为Txp，然后创建内部切割（up），最后再次将其插入上下文中，得到Tup-注意，这相当于在t中用u代替x。使用上下文编写，λπ的完整归约规则集是：（λx.T[x]）y→T[y]（λx.T）[u（π.t）（p，q）→（t p）q（λ！X.T！xp）！u→（λ！x.Tup）！u（λ！x.t）！u→t如果x/∈fv（t）其中fv（t）通常表示t的所有自由变量的集合。所获得的重写系统与Accattoli等人 [2]定义的线性替换演算有着惊人的相似之处，后者本身基于线性逻辑和证明网的思想。 我们把对这种联系的研究留到将来的工作中去：为了这个演示的目的，它应该注意到，上述对λ和λ的约化！实现通常的捕获避免替换的概念。因此，我们可以使用隐式替换来总结λπ的约化，这产生了包含以下内容的系统：112T. Brock-Nannestad，N.Guenot/Electronic Notes in Theoretical Computer Science 319（2015）103四条规则：（λx.t）y→t{y/x}（λx.t）[u→ t{u/x}（π.t）（p，q）→（t p）q（λ！x.t）！u→t{u/x}（二）我们观察到前两个对应于MELL的基本极化子系统，而另外两个则分别对应于乘法子系统和指数子系统。请注意，我们在这里考虑的是语言的类型化片段-在非类型化的情况下，可以接受更多的术语，并且可以将形实转换程序[u]插入值中。除了削减消除，像我们这样的聚焦和显式极化系统可以被赋予另一种形式的动力学，它不像β约化那样代表计算，而是对应于一种形式的项简化。事实上，明确的极性偏移可以用来引入延迟，由一对相反的偏移形成的复合物，可以打破聚焦相位或防止最大反转。这可以解释为将一段计算放在一个值上，该值分为两部分：因此，去除延迟有助于产生具有不同计算行为的更简单、更紧凑的项从相反的观点来看，很明显，任何未聚焦的证明都可以映射到延迟的、聚焦的证明。 有了这个，我们现在可以根据延迟消除的可接受性来重述聚焦结果[8，24]，而不是根据非聚焦参考系统的完整性来陈述它。 在陈述结果时，我们使用公式上下文的概念，写作<${−}。公式{P}应解释为子公式P线性出现的公式（正或负）。 外部上下文<${−}则表示通过<${P}的路径，该子公式出现在该路径上。引理3.6（正延迟消除）对于任意D：：π; Γ，x：↑π{↓↑P} πS无割的，存在一个导子E：：<$; Γ，x：↑<${P}<$S.证据 在我们证明这个陈述之前，我们将做一些简化的假设。首先，请注意，只有当公式成为焦点时，上下文中的公式的性质才变得相关因此，我们假设在最上面的连接词和子公式↓↑P的位置之间，<${↓↑P}只包含正公式。当选择f{↓↑P}作为焦点时-我们可以假设这在D中表现为最终规则-我们因此可以将导子D分解为子导子DJ：：f; rJ F↓↑P和从f; rJ F↓↑P到f的开导子G。► ;r，↑ 注意，由于G只能分裂上下文，因此对于某个上下文Δ，我们必须有Γ = ΓJ，Δ。此外，用这个开导组成任何证明<$; ΓJJ<$Q将产生一个证明<$;ΓJJ，Δ<${Q}。通过在DJ上求逆两次，我们得到一个导子DJJ：：;ΓJ，↑P·，并且通过应用线性分解引理，这可以被分解成一个导子F：：，j; ΓjjP和一个从，J; ΓJJ·到，J;ΓJ·的开导子GJ，因此现在可以将这些导子串在一起从F和G，我们得到了一个导数，即，，J; ΓJJ，Δ{P}，因此我们得到了一个导数，即，T. Brock-Nannestad，N.Guenot/Electronic Notes in Theoretical Computer Science 319（2015）103113与GJ合成得到<$r; r，↑<${P}<$·，其中我们使用等式r = rJ， Δ。Q引理3.7（负延迟消除）对于任意D：：N;ΓS1，N{↑↓N}，S2无割的，存在一个导子E：：Γ; Γ S1，S{N}，S2。证据证明以类似的方式进行，我们只是概述论点。首先，我们可以假设在反演上下文中，n{↑↓N}是第一个公式，并且只有负公式出现在通往↑↓ N的路径上。然后我们做一个分解，直到↑↓N被放置在无序的上下文中，并找到它再次聚焦的子派生。这个子推导必须立即分解N，因此我们可以向下传输这个分解，并将其与上下文{−}组合以获得所需的证明。Q焦点化的结果是通过迭代应用前面的引理得到的：特别是，去除负延迟迫使连接词被急切地分解，去除正延迟组的实例的规则。在计算层面上，这两个引理的证明所指定的过程对应于λπ-项的某种重组，它删除了一个不必要的中间名。为了精确地描述消除延迟的效果，我们需要为了改进我们的语境语言，考虑单极语境，它只能包含一个极点，这是一层连续的负或正连接词：A：：= −|（A，p）|（p，A）B：：= − |λ x.B |λ！十.B|π B使用这些上下文的概念，我们可以分别精确地描述正延迟消除和负延迟消除的效果：y A→T λx.T →B通过重写规则来体现，这些规则可以应用于T上下文中的任何地方。 注意，在A为空的基本情况下，第一个规则就是y[λx.Tx p→Typ，这对应于一个聚焦阶段的开始立即中止。4线性逻辑的片断及其λ演算我们已经在前一节中看到了极化MELL的聚焦λ演算如何对应于精化的线性λ演算。然而，通过考虑由有效公式和序列的特定子集或规则的限制生成的子演算，可能更容易掌握λπP450线性片段。可以考虑的最简单的片段是通过忽略指数和持久化上下文获得的。 这产生了一个子集λπ可以与纯线性λ-演算相关，也就是说，λ演算中变量只能使用一次。 更准确地说，是Herbelin提出的λ-演算的线性版本的相对简单的编码，作为LJT聚焦直觉主义λ-演算的解释[12]。114T. Brock-Nannestad，N.Guenot/Electronic Notes in Theoretical Computer Science 319（2015）103|||⊥（）（）（2）（）（）（）（2）r，x：Bxk：a−λ−c−−。（−x−−p−）−Γ−，−x−−：−−B−aΓλx.t：A−B-π-。−λ−x−。−u−Γ−−A −B−−（−−u−−，−p−）−Γ−， − −Δ−，−c−：−−a−B−C−Γ， Δ， [B-C]t：：k：art：NΔ， [N]k：a−− − − − − − − − −−⊥− − − −−⊥− − − − − − − − −−−Γ，Δtk：au<$N）p<$<$Δ）n，c：<$a<$N）n该演算在应用程序中有参数列表，并基于以下语法：t，u：：=xk λx.t tk k，m：：=ε t：：k其中ε表示一个空的参数列表，需要恢复简单变量x，这里编码为x ε，而：：是列表构造函数。这种演算的线性形式的类型系统由LJT的线性变体给出，我们称之为IMLLT，其中区分了两种序列：我们写ΓN表示未聚焦的π，而Γ，[N] πa表示聚焦在N的左侧的π，其中右侧仅限于一个原子，因为我们考虑了η-长项。 编码基于非极化直觉线性公式的简单转换，我们用A或B表示：<$a）= ↑a<$A − <$B）= ↑<$A）（乙）其可以逐点扩展到上下文。翻译中最重要的部分是将IMLLT的序列与我们的系统系统的序列联系起来，其中持久上下文始终为空，因此被省略：其中按照惯例，我们选择c作为任何聚焦IMLLT的原子右侧的名称-这个变量将表示空列表。然后，类型化派生的转换基于这些转换，如下所示：−[−a−]−−ε−：−a~JT−c−−c−：−−a−−a►↑⇓ ↓Γ， [B]k：ap↑Γ，c：↑aB组−−−−−−−⊥−−−−−−−⊥−−−−−−−− − − − − − − −−~JTxp↑ <$r），x：↑<$B），c：↑a·► ↑ <$）↑ <$）⇑ ↑r，x：A，t：Bu↑Γ，x：↑AB−−−−−−−−⊥−−−−−⊥−−−−−− − − − − − − − −~JTλx.u↑ <$<$r）↑<$A），<$B）► ↑ <$）⇑ ↑ ¢）（Ⅲ）Γt：BΔ， [C]k：au↑ΓB−−−−−−−⊥−−−−−⊥ ⊥−− − − − − − − − − − − − −−~JT[u↑ <$<$r）↓ <$B） p↑ <$$> Δ），c：↑a<$C）[↑<$$>]↑ <$⇓ ↓ ¢）（三）其中p是k的平移，u是t的平移。语法↑Γ表示上下文Γ，其中公式用负移位注释。这种转换将参数列表转换为右关联的thunk对，而转换抽象需要π运算符。因此，这些结构之间存在匹配，并且我们可以用切割规则以预期的方式组合这些项，对应于LJT的线性形式的主要头部切割−− − − − − − − − − − − − −−~JTup<$↑<$r），↑<$Δ），c：↑a<$·−λ−c−−。（−u−−p−）−Γ−，−−Δ−a► ↑<$） ↑ <$）⇑ ↑T. Brock-Nannestad，N.Guenot/Electronic Notes in Theoretical Computer Science 319（2015）103115因此，通过在我们的聚焦MELL系统中的约化来模拟该线性λ -演算中的约化。更具体地说，我们用于IMLLT的归约系统→JT是基于隐式替换而不是LJT中的原始显式替换[12]：（λx.t）（u：：k）→JTt{u/x}k（λx.t）ε→JTt（t k）m→JTt（k@m）（三）其中@表示列表的级联。在λπ-演算中，我们考虑紧凑形式的归约规则，如（2）所示。结果，我们得到了由下面的定理描述的λπ中的线性λ-演算定理4.1若t ~JTu且t →JTv，则存在w使得v ~JTw且u → JT w。证据我们继续对项t进行结构归纳，扩展语句以处理列表作为λπ-项的转换。在基本情况下，它是一个空列表，没有任何归约规则适用，所以我们完成了一般来说，除了redextk之外，所有的情况都直接依赖于诱导假说。在最后一种情况下，我们考虑可能的约简，使得复合约简：λc. （（π.λx.t）（[u∈，q））→<$ λc.（t{u/x}q）λc。（（λx.t）c）→<$λc.t{c/x}λc. （（λd.up）q） →λc。（up{q/d}）是（3）中所示的归约规则的翻译。第一个约简很简单，依赖于对：：构造函数进行编码的对的分解和一个替换。第二个约简只是执行了一个替换，但是应该注意的是，在约简之后，c不再是右边的标记，而只是x的重命名。最后，最后一个约简依赖于将列表编码为右关联对，使得p{q/d}恰好是λ π中k@m的编码。Q注意，这种编码将λ中的原始构造转换为λπ演算的复合构造。我们演算中的某些术语在解释IMLLT时没有等价物：我们在这里只捕捉到了MLL的一个直观片段。这在我们的翻译中可以很清楚地看到，因为它对应于在上下文中具有形状↑a类型的单个变量c的存在，它代表了一个唯一的右手边。我们可以捕获更大、更经典的微积分片段，但使嵌入稍微复杂一些虽然我们可以研究λμ演算的线性变体的编码，但我们选择使用指数来表示λμ的完整的基于序列的变体。指数碎片。除了上面讨论的纯线性片段之外，一个明显的感兴趣的子系统是与LLP相关的没有极性变化的子系统[15]，人们可能想进一步推动这一点，并试图完全消除对线性上下文的需求。这是有问题的，因为公理规则仅在线性上下文不为空时才适用，但是可以通过考虑从恒等式扩展结果获得的指数公理规则来解决这个问题：==！x，x：？P！P116T. Brock-Nannestad，N.Guenot/Electronic Notes in Theoretical Computer Science 319（2015）103（）（））（）（）Γ，[N] a |Δ~Δ θθr），？△）， c：？↓aN）KT（）（）（）（）（）|（）（）（2）（）（）−！-c-！u− Γ−，−？−Δ− −，−c−：−？−！−N−Γ [α] t|α：]N，Δ-λ-！-c-。-（-！−x−p−）− Γ− −，−x− −：−？-N--N-，-？−Δ−？−−ar，x：]Nxk：a|Δ-π-- λ−！-x-。-u--−Δ−？−N−−N−−M−−Γλx.t：]N M |Δ然而，在我们的系统中完全避免极性转移是不可能的，因为没有极性转移就不能处理原子。我们考虑Herbelin [13]的λμ-演算，它是LKT的一种解释，可以通过将λμ的控制规则添加到LJT系统和项分配中来获得。 由于MELL中的极化设置，我们使用这种演算的显式极化版本，其中μ和命名规则通过移位反映在类型上-我们写为]和²以将它们与MELL的移位区分开来。公式的翻译则定义为：a=？↓aP N=？ PN=！ N²P=？PLKT系统有两种序列，就像LJT一样，它们是通过添加其他右侧的上下文Δ而获得因为我们使用了极化公式，所以左手边的上下文Γ总是包含形状为]N的公式，就像Δ一样。然后使用公式的翻译对序列进行编码，如下所示：ΓN |Δ~KTτ τ）τ，？<$Δ）<$N）其中，聚焦的MELL序列在没有线性上下文的情况下被写入，因为它在该转换中总是空的。事实上，在线性背景下引入公式所需的极性变换只用于原子，因此它们不能脱离公理规则。在我们的系统中，关于μ伊特|α：]N，Δ−Γ− − −μ−α−−。−t−：−<$−]−~KT你说呢？ Δ，c：？！ N⇑·−−−−−−−⊥−−−−−−−−−►N|Δλ！c.ur），？？？（N）t：N |α：]N，Δu你呢？ Δ，c：？！ N中国−−−−−⊥−−−−−−−−−−−−−−−− − − − − − − − − − −~KT！ur），？？Δ），c：？！-不！（N）► （）（））其中c是LKT中标记为α的标记的名称，u是翻译中医 其他规则的翻译方式与LJT的编码方式非常相似，但它们都对右侧上下文Δ进行了一般化处理−Γ−，[a−]−−ε−：−a−−Δr，[N] k：a |Δ~KT=============================！什么？ Δ，c：？↓a！↑apr，x：？不，？Δ，c：？↓aN−−−−−−−⊥−−−−−−⊥−−−−−−−−−−−−− − − − − − − − − − −−~KT！xp_r），x：？（N）、、怎么样？△），c：？↓a·► （）（））↓r，x：]N，t：M|Δu你呢？ Δ，x：？ NM−−−−−−−⊥−−−−−−−−−⊥−−−−−− − − − − − − − − − − −~KTλ！x.ur），？（Ⅲ）？<$N），<$M）► （1））（Ⅲ）（ Ⅲ）T. Brock-Nannestad，N.Guenot/Electronic Notes in Theoretical Computer Science 319（2015）103117（）（）（）−（−！-u-，-p-）-Γ-，-？−Δ− −，−−c−：−？--a--！−N−M−t：N |Δr，[M] Δ k：a|