经典逻辑连接词的影响和计算内容研究

理论计算机科学电子札记171（2007）85-109www.elsevier.com/locate/entcs经典逻辑联结词Jayshan Raghunandan和Alexander J.萨默斯伦敦帝国理工学院计算机系，180 Queen's Gate，London SW7 2RH，UK摘要许多编程演算被设计成与经典逻辑具有Curry-Howard对应关系。我们研究了逻辑连接词的不同选择对这种演算的影响，以及由此产生的计算内容。我们确定了两个连接词“if-and-only-if”和“exclusive or”，它们的计算内容并不为人所知，并且它们的切割消除规则对于定义来说是不平凡的。在前者的情况下，我们定义了一个术语演算，并表明其他几个连接词的计算内容可以模拟。 我们表明，这是可能的，即使是连接词逻辑上不能表达的保留字：Curry-Howard对应，逻辑演算1引言有许多编程演算已经被设计成具有与逻辑证明系统的Curry-Howard对应。近年来，这种演算已经被设计来探索经典逻辑的计算内容（例如[2，4，6，8，11，12，14]）。不同的作者选择了不同的逻辑连接词集合作为蕴涵是连接词中最受欢迎的选择，因为众所周知，它的计算行为与函数抽象和应用有关。有些演算不使用蕴涵，例如Wadler的演算[14]。微积分存在使用合取，析取，否定，甚至更深奥的连接词，如差异[1，2]和真与假的常数。本文考虑具有不同本原联结词的逻辑，并讨论设计相应项演算的我们把注意力集中在1 电邮地址：jr200@doc.ic.ac.uk，ajs300m@doc.ic.ac.uk1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.12.03986J. Raghunandan，A.J.Summers/Electronic Notes in Theoretical Computer Science 171（2007）85命题逻辑连接词;在[10]中研究了使用量化器的各种方法。我们在微积分的逻辑背景下工作，在第2节中给出了简要介绍。 我们的术语演算的风格是基于X-演算[12]，它与经典的蕴涵演算有Curry-Howard对应X-演算在第3节中给出.第4节，我们将X的设计推广到基于类项演算的类不同的逻辑连接词。第5节确定了一类要研究的逻辑连接词，并为每一类逻辑连接词展示了如何导出合适的项表示和相关的归约规则。我们发现，计算内容的“如果和只有如果”（Participate）和“排他性或”（Exclusive or）连接词没有得到很好的理解。第六节是对“if-and-only-if”连接词的研究，其归约规则是非平凡的定义。我们定义了一个术语演算仅基于这个连接，我们称之为X参与，并研究其计算表达性。作为一个令人惊讶的结果，我们表明，这种新的演算可以，在一定的限制，模拟减少几个著名的逻辑连接词本身不是逻辑上可表达的参与。作为一个例子，我们给出了X-演算到X-Participant的解释.第2章顺序演算近年来，已经提出了各种基于Curry-Howard对应的编程演算，这些演算与逻辑演算证明系统，而不是自然演绎系统。 在这样一个证明系统的经典逻辑，一个处理序列的形式A1，...，AmB1，.，Bn，其应被读作“如果A1，.，Am都为真，则B1，.，Bn为真”。证明规则被定义为在一个集合的左边和右边都引入一个逻辑连接符（与自然演绎系统相反，不使用排除规则）。在本文中，我们把一个导数的左、右公式的集合看作集合，并允许在一个导数的叶子（公理）上包含任意的额外公式，这是Kleene [5]的风格。这就避免了在原始微积分[3]中使用的结构规则的需要，这使得证明系统可以专注于公式本身的结构。在微积分中，有一个特殊的规则叫做截集，它把两个证明连接在一起。根岑在他的微积分中指出，尽管切割规则可能对简洁有用，但它是多余的，因为任何包含切割规则实例的证明都可以转换为同一个端点的无切割证明。Gentzen定义了一组切割消除规则，这些规则是不一致的，并且是标准化的，但不是强标准化的。图1给出了一个只具有蕴涵连接符的逻辑的微积分的例子。事实上，这个特殊的微积分是X-微积分的基础，这将在下面的章节中描述。J. Raghunandan，A.J.Summers/Electronic Notes in Theoretical Computer Science 171（2007）8587Γ，A<$A， Δ（Ax）ΓΔ，A A，ΓΔ（切）Γ► ΔΓ<$A，ΔB，Γ<$Δ Γ，A→B<$Δ（→L）Γ，A<$B，ΔΓ<$A→B，Δ（→R）Fig. 1.一个蕴涵3X-微积分我们的工作是基于X-演算[12];经典蕴涵演算的无类型术语注释。我们在这里回顾一下基本的定义。定义3.1[X-术语]X-演算的术语由以下语法定义，其中x，y在无限套接字集合上变化，α，β在无限插头集合上变化（套接字和插头一起形成连接器集合）。P，Q：：=1x。α⟩|y^Pβ^·α |Pβ^[y]x^Q|Pα^<$x^Q|Pα^x^Q|Pα^x^Q胶囊出口介体切割左切割右切割这个定义是这样的：在一个子对象中绑定了一个连接套接字-绑定套接字被写为该术语的前缀，而绑定插头被写为那就好。对于在Pβ^[y]x^Q中执行的方法，子项P和x的出现次数在Q中有界。不出现在活页夹下的连接符称为自由连接符。我们将使用fp（P）来表示P的空闲插头，类似地，fs（P）表示空闲插座。我们进行模α转换（关于α转换的问题已在[13]中研究减少规则如下所述。定义3.2 [逻辑规则]逻辑规则表示为：（cap）：ciry。αα^<$x^x。ββ→βγ。β⟩（ex p）：（y^Pβ^·α）α^fx^fx. γα→γ^Pβ^·γα/∈fp（P）（med）：darry. α<$α^<$x ^（Pβ^[x]z^Q）→Pβ^[y]z^Qx/∈fs（P，Q）⎧ ⎫^<$Qγ^<$y^（Pβ^<$z^R）α/∈fp（P），（exp-med）：（y^Pβ·α）α^fx^（Qγ^[x]z^R）→α（Qγ^<$y^P）β^<$z^Rx/∈fs（Q，R）上面的前三个逻辑规则指定了重命名（重新连接）过程，而最后一个规则指定了基本的计算步骤：它允许主体从导出的函数中插入到中介体的两个子项之间（所产生的剪切可以以任何方式括起来，如图所示）。定义3.3[激活规则]我们定义了两个切割激活规则。88J. Raghunandan，A.J.Summers/Electronic Notes in Theoretical Computer Science 171（2007）85（act-1）：Pα^fx^Q→Pα^（act-R）：Pα^fx^Q→Pα^x^QifPdoesnotintroceax^QifQdoesnotintrocexJ. Raghunandan，A.J.Summers/Electronic Notes in Theoretical Computer Science 171（2007）8589其中：Pint roduces x：Ei therP=Qβ^[x]y^Randdx/∈fs（Q，R），或P=∞x。α⟩P∈ f p（Q），或P=fx. α⟩一个激活的切割是通过在匕首倾斜所指示的方向上系统地“推动”它通过电路的句法结构来处理的。每当活动切割遇到展示其试图与之通信的连接器的电路时，新的（非活动）切割被“沉积”，表示在该级别上通信的尝试。继续推动活动切割，直到达到胶囊的水平，在那里它被停用或销毁。 同样，非活动切割可以通过逻辑规则减少，或者可以在另一个方向上继续推动。此行为由以下传播规则表示。定义3.4【传播规则】左传播：（†）：y。α<$α^x^P→βy。αα^<$x^P（cap）：darry. β<$α^x^P→βy。β⟩βα（exp-uts）：（y^Qβ^·α）α^（exp-ins）：（y^Qβ^·γ）α^x^P→（y^（Qα^x^P→y^（Qα^x^P）β^·γ）γ^^x^P， γfreshx^P）β^·γ，γi=α（m ed）：（Qβ^[z]y^R）α^x^P→（Qα^x^P）β^[z]y^（Rα^x^P）（cut_ca_p）：（Q0）y_p。α）α^x^P→（Qα^x^P）β^<$x^P（cut）：（Qβ^fy^R）α^x^P→（Qα^x^P）β^<$y^（Rα^x^P），R/=y. α⟩右传播：（†）：Pα^ x^αx。β→Pα^<$x^<$x。β⟩（cap）：Pα^ x^y。ββ→βγ。β1，y/=x（exp）：Pα^x^（y^Qβ^·γ）→y^（Pα^x^Q）β^·γ（med-outs）：Pα^x^（Qβ^[x]y^R）→Pα^<$z^（（Pα^x^Q）β^[z]y^（Pα^x（R）），ZFresh（med-单位：s）：Pα^x^（Qβ^[z]y^R） →（Pα^x^Q）β^[z]y^（Pα^x^R），z x（cut-cap）：Pα^x^（？x. β<$β^<$y^R）→Pα^<$y^（Pα^x（R）90J. Raghunandan，A.J.Summers/Electronic Notes in Theoretical Computer Science 171（2007）85（cut）：Pα^x^（Qβ^<$y^R）→（Pα^x^Q）β^<$y^（Pα^x^R），Q/=πx. β⟩对于由逻辑、传播和激活规则生成的归约关系，我们写→。以下是可接受的规则（见[12，13]）。引理3.5（垃圾收集和重命名）（gc-1）：Pα^（GC-R）：Pα^x^Q→P，如果α/∈fp（P）x^Q→Q，如果x/∈fs（Q）（ren-1）：Pδ^tz^tz. απ，→P[α/δ]（ren-R）：πz.α<$α^<$x^P，→P[z/x]J. Raghunandan，A.J.Summers/Electronic Notes in Theoretical Computer Science 171（2007）85914连接词的计算表示在本节中，我们概述了本文其余部分中使用的一些技术，用于导出合适的证明规则，相应的语法表示和归约规则，以表示包含特定的逻辑连接词。我们用A，B，. 作为命题变量和<$来表示逻辑否定，这比任何其他连接词都更紧密我们用和·来表示任意的二进制连接词（逻辑连接词，有两个参数）。对于公式F1和F2，我们写F1<$F2（并说公式在逻辑上是等价的），如果对于命题变量的所有真值赋值，F1和F2具有彼此相同的真值。4.1顺序规则我们将假定公理的规则（参见X中的胶囊），并且切口在我们讨论的所有系统中都存在且不变（见图1）。对于每个感兴趣的逻辑连接词，必须提供（或导出）合适的证明规则，以在一个逻辑连接词的左侧和右侧引入连接词（参见1999年的《逻辑连接词的证明规则》）。图1的L和R）。重要的一点是，对于各种逻辑连接词，可以选择要合并多少个证明规则。这在对配对的不同处理中最容易看到，典型地与连接词有关（尽管这个概念在第5节中被概括）。通常提供一个术语来构建一个对，但是处理配对问题的不同方法（利用其单独的组成部分）。一种方法是提供两个突出部，这将一对减少到其组成元件中的一个或另一个。另一种方法有时被称为“模式匹配”方法，其中两个组件都被替换为某个接收项。这两种方法在我们的框架中可以被证明是相互衍生的，并且使用哪种方法的决定在很大程度上是一个品味问题作为例如，对于连词（conjunction），可以指定左介绍以下两种方式之一：Γ，A，B<$ Δ.（英文）或Γ，AΔ（第1页）和Γ，BΔΣ（第2页）Γ，A<$B<$ ΔΓ，（A<$B）<$ΔΓ，（A<$B）<$Δ在本文中，我们选择了“模式匹配”的风格，也就是说，我们将始终选择只有一个左，右介绍规则的二元连接。对于一个特定的连接词来说，一组合适的防错规则并不总是显而易见的。在这种情况下，可以如下进行以导出对于二元连接词，合适的规则是，选择公式F，使得FAB和F使用连接词，人们已经知道合适的证明规则。现在，试着构造一个“一般”的推导，它在这个公式的左边和右边引入了这个公式。一旦F中的所有连接词都被引入，就不可能在推导中进一步进行。所有剩余的子推导都被转换为派生规则中的子证明，而公式F被AB替换为最终的证明。这个过程92J. Raghunandan，A.J.Summers/Electronic Notes in Theoretical Computer Science 171（2007）85将给出适当的证明规则的连接符。这种技术将在第5节和第6节中进一步说明和开发。4.2Term语法我们以X演算的风格工作，因为这给出了语法中存在的输入和输出的简单和对称的处理。当导出表示特定证明规则的语法时，出现在一个数组左边的公式将成为输入（套接字）x，y，z，.。而右边的公式将是输出（插塞）α，β，γ，.. . .规则中出现的任何子证明都将被表示为语法的子项。通过应用证明规则而从这样的子证明中消失的公式（被该规则约束的公式）将对应于子项上的约束连接符，而由该规则引入的新公式对应于适当种类的自由连接符有了这些想法，就应该清楚地看到，图1中的微积分的术语表示可以很好地被选择为X的语法（见定义3.1）。例如，→R规则有一个子证明，它对应于一个子项P。它在这个子证明中绑定了两个公式，一个在左，一个在右，因此P的插座和插头应该被绑定（分别说x和α该规则在项的右边引入了一个新的公式，这导致了项表示中存在一个自由塞（比如β）。实际上，可以简单地对X计算器的表达式进行分析，writtenx^Pα^·β是一种表示，其中·是不活动的语法，旨在使项更容易解析。作为另一个例子，考虑→L规则。这有两个子证明，它们成为子项P和Q。每一个都有一个公式，分别在序列的右边和左边。因此，一个插头α被束缚在P中，一个插座y被束缚在Q. 总之，一个新的问题将被解决。Pα^[x]y^Q中的一个项是选择n，x出现在两个项之间只是为了更好地直观地了解该项的行为;它充当两个子项之间的“洞”，可以插入另一个项以在P和Q之间进行4.3减小规则无论使用什么逻辑连接词，我们都将始终保持以下X减少规则（处理削减和胶囊）：cap，act-L，act-R，†，盖，切盖，切，†，盖，切盖，切割被引入的插头或插座的概念可以推广为P引入x（分别为α）ix在P中是自由的，但在它的任何真子项中都不是。必须定义传播规则，以通过每个语法结构传播左切割和右切割。如果一个新的语法结构对应于一个左引入规则（即，它的自由连接符是一个套接字），则必须给出两个规则来在它上面传播一个右切割（取决于自由连接符是否是切割所在的位置诱惑连接到），和一个用于传播左切（c.f.Med-out，med-ins，医学）。J. Raghunandan，A.J.Summers/Electronic Notes in Theoretical Computer Science 171（2007）8593一般的方法是将剪切的副本推入子项中，如果所需连接符出现在此级别，则在外部（比照Med-out）。 在构造上传播的适当规则，引入一个插塞可以对称地导出（两个用于左切割，一个用于右切割）。这使得适当的额外逻辑归约规则有待定义。每个新的语法结构都保证一个逻辑规则来指定通过一个带有胶囊的切割来重命名它引入的连接器（例如，参见规则exp和med）。最后，对于每一个逻辑连接词，必须定义一个逻辑规则，以表明连接词的右引入和左引入之间的切割是如何被减少的（参见1999年）。规则exp-med）。我们称之为连接词的主要逻辑规则，因为它是规定如何从证明中删除这些结构的规则，在它们的子项之间创建新的切割，并简化切割消除的任务。主要规则是唯一不能独立于有关的特定连接词而有条不紊地推导出来的规则。因此，当研究一个特定连接词的表示时，就归约规则而言，我们只关心连接词的主要逻辑规则5比较逻辑连接符在本节中，我们比较了各种逻辑连接词，重点是它们之间的关系以及这如何影响它们在术语演算中的包含。对于每个连接词，我们对以下三个问题感兴趣：(i) 什么是它的证明规则的合适的术语表示？(ii) 它的主要归约规则是什么？(iii) 通过包含它获得了什么计算内容？5.1列举连接词可能的逻辑连接词的数量是无限的，因为连接词可以应用于任意（但通常是固定的）数量的参数（在此它的arity）。 在实践中，作者很少使用arity大于2的连接词（尽管有一个例子，见[7]）。为了决定我们研究的一组连接词，我们发现了以下三个有趣的问题(a) 有多少个逻辑连接词的元数为n（n≥0）？(b) 其中有多少依赖于所有n个输入（我们说这些输入有真元n）？(c) 其中有多少总是依赖于所有n个输入？为了解释第二个问题，以二元连接符为例，它的输入是A和B，并且总是计算为A（忽略B）。在某种意义上，我们可以将其视为一元连接词，因为它只使用一个输入。这给出了一种方法来识别那些元数为n的联结词，我们把它们看作是退化的情况。第三个问题涉及一个更强的概念;连接词的值应该在每个输入状态中取决于它的所有输入。作为非示例，94J. Raghunandan，A.J.Summers/Electronic Notes in Theoretical Computer Science 171（2007）85我合取（conjunction）的求值可能是“捷径”;如果它的第一个参数被证明是假的，那么第二个参数就不需要考虑了。因此，合取不满足第三个问题中概述的标准。这些问题的答案由以下结果给出：定理5.1（枚举逻辑连接符）对于任意整数n≥0：(a) 有22n个元数为n的逻辑连接词。(b) 依赖于所有n个输入的这些数（真元n的那些），t（n）由以下公式给出：t（n）= 22nn-1。−i=0时Σn t（i）。我(c) 正好有两个n元的连接词总是依赖于所有n个输入;这是奇偶函数（当它的参数是偶数时正好为真），以及它的否定。证据(a) 每个连接词都由一个“真值表”精确地指定计算所有这些真值表的结果如下。(b) 通过计数;从所有n元的连接词开始，减去o那些依赖于严格较少输入的连接词。由于这些中的每一个都可能取决于不同的代替了你。输入一个可用的值，以便用户将其用于操作准备子组（即n）。(c) 设f是这样一个n元的连接符，我们将其表示为n个输入的函数，f（i1，i2，.，in）。我们写0表示假输入，1表示真，i表示这些输入的否定（即1 = 0等）。我们对f的条件是，给定一组输入值i1，.，in，f（i1，i2，.，in）取决于所有i1，..，in，或者等价地，如果我们改变（否定）输入中的任何一个，则f（i1，i2，. i n）必须改变。 现在考虑将所有输入设置为0，并且假设f（0，. ，0）= a，其中a = 0或a = 1。 根据f的条件，如果我们现在对输入中的任何一个求反，f（i1，i2，. ，in）必须是a。一般来说，令j为真实输入的数目，即，j=|{ik|1 ≤k≤n且ik=1}|.对j的直接归纳表明：⎧ ⎫如果j是偶数，f（i1，i2，.，in）=如果j是奇数，因此，f完全由a的选择所指定。因此，正好有两个这样的函数，奇偶校验函数和它的否定。Q检查这个结果的第二部分，我们看到t（0）= 2。这两个连接词是逻辑常数T和T，它们可以被看作是元数为0的连接词（它们可以被看作是元数为0的奇偶和非奇偶连接词）。 很容易看出t（1）= 2，这些是单位联结词（J. Raghunandan，A.J.Summers/Electronic Notes in Theoretical Computer Science 171（2007）8595SDS SA组B组D A BB−ADA→B无无无无无无无A↑BDA↓B B→ADA−BS SD DTASB A ParticipBN N⊥ ¬ASB AD注：↑=，↓= nor，= xor图二. 二元连接词返回它接收的任何输入不变）和否定（<$）。 此外，我们看到t（2）= 10，即有10个不同的逻辑联结词的真元为2。 这些连接词将在下一节中列出，尽管读者可能会觉得首先尝试命名它们很有趣！从今以后，我们将只对第2元（和- low）的联结词感兴趣。正如所评论的，这种选择在文献中很常见。实际上，由于读者可以验证t（3）= 218，因此对所有可能的更大数量的连接词进行详尽的分析将过于繁琐。5.2二元连接词在本节中，我们将给出可能的二元连接词的完整集合，并根据第5节开始时概述的三个问题对它们进行分析。我们感兴趣的是这些连接词之间可能存在的关系，以及这些连接词如何被它们的计算对应物所反映。例如，对偶性是一个与二元逻辑连接词相关的众所周知的概念，并且可以看到这种关系延续到它们的计算行为中（这与[2，14]的结果有关）。我们利用连接词之间的以下关系第五章. 2[重新计算成本]对于任意两种成本计算方法，·：对偶我们说·是iA·B（B）的对偶否定我们说·是iA·B<$（AB）的否定NSDNSSDS96J. Raghunandan，A.J.Summers/Electronic Notes in Theoretical Computer Science 171（2007）85Γ<$B，Δ Γ，A<$ΔΓ，A←B<$Δ（←L）Γ，B<$A，ΔΓ<$A←B，Δ（←R）图三. 反向蕴涵的顺序规则←我们说·是iA·BBA的相反。翻转输入我们说·是通过翻转一个输入得到的，如果A·BB。除了最后一种情况，这些概念都描述自反函数（例如，连接词的对偶的对偶是连接词本身）。二元连接词包括连接词（conjunction）、分离词（disjunction）、非（nor）和非（↑）。有蕴涵（→）和它的逆蕴涵（←），以及所谓的“微分”算子（−），其中A-B B。对于反向连接词−（没有标准符号），我们倾向于简单地使用−并交换参数，但很快就可以省去这种轻微的符号滥用。除此之外，还有“如果且仅如果”（Participate）、“异或”（exclusive or）和退化情况（T、和每个参数上的恒等式和否定式，我们将写为id A、<$A、id B和<$B）。虽然我们称这些退化的情况为二元连接词，但我们将把它们视为具有它们的真实特性（例如，当使用否定时，我们只提到它使用的输入）。所有这些连接词都在图2中显示，还有箭头表示连接词的对偶（D），否定（N）和反转（R）首先，我们希望考察联结词的“颠倒”对我们的利息问题的影响。例如，考虑连接词←。图3显示了这个连接词的一对合理的规则。推导出表示这些规则所需的语法，我们发现我们可以使用与蕴涵完全相同的语法。这是因为相同的输入和输出是绑定的，在规则中引入了类型;与蕴涵规则的唯一区别在于A和B的位置，一旦删除类型，这就无关紧要了。类似地，表示这个连接词所需的归约规则将与表示蕴涵的归约规则完全相同，因此所获得的计算内容也是如此。这些概念可以推广到任何连接词及其相反的情况。由于这一观察结果，我们选择检查问题模反转中的连接词由于图2中的大多数连接词都是对称的（颠倒时保持不变），这实际上只减少了四个连接词的数量。我们的符号变得不那么麻烦，因为我们需要不写公式来定义任何连接词（例如，B-A被用来写A−B的相反）;我们现在可以为每个写一个明确的符号。 这在图4中示出，其中指示对偶（D）、否定（N）和重复输入（F）的箭头将相关的连接词组合在一起。我们需要解释这三种关系的重要性。在考察否定连接词的效果之前，考察否定连接词本身是有用的。否定的基本规则如下：ΓA，ΔΓ，<$A Δ（€L）Γ，AΔΓA，ΔJ. Raghunandan，A.J.Summers/Electronic Notes in Theoretical Computer Science 171（2007）8597（€R）98J. Raghunandan，A.J.Summers/Electronic Notes in Theoretical Computer Science 171（2007）85FFNDFTIDDid∨ − ↔NN NN，DF↑DF↓ → ⊗F见图4。 二元连接模反转第一条规则将一个公式绑定在图的左边，并在右边产生一个新的公式，而第二条则相反。我们选择用于求反的语法以可能的最简单方式反映了这种输入与输出的交换;对于最小和最小的项，我们写x·Pα^和^Q·β。我们的产品否定的归约规则如下：（x^P·α）α^<$y^（y·Qβ^）→Qβ^<$x ^Pα/∈fp（P）， y/∈fs（Q）给定任何连接词的否定规则，导出连接词的否定的适当的否定规则是直截了当的。例如，蕴涵（→）的否定是“差异”连接词（−），通过在一个符号的左边和右边寻找公式<$（A → B）的适当推导，人们可以推导出“差异”的适当规则，如图5所示。请注意，表示“差异”的适当语法为了暗示，除了引入的自由连接符出现在符号的相反侧（由于否定）。例如，对于t-输入还原规则，Pβ^[α]x^Q是离散的连续性度量的情况和x·y^Pβ^。这种传统的做法是相互联系和相互制约的;项表示对于每一个都是相同的，但是左项和右项交换。此外，在定义割消规则时，我们可以看到，关键逻辑规则的归约在→和−的情况下是相同的，一般来说，对于连接词及其否定词也是相同的。连接词和它的对偶词之间的关系，就其计算表示而言，也可以被看作是它们的术语表示之间的关系。在这种情况下，以及引入的公式“交换边”，在证明规则中绑定的公式也这样做。例如，比较规则为：Γ，A，B<$ ΔΓ，A<$B<$ Δ（比利时法郎）ΓA，ΔΓB，ΔA（孟加拉国）<$A，B，Δ<$A<$B，Δ（孟加拉国）Γ，A<$Δ Γ，B<$ΔΓ，A<$B <$Δ（比利时法郎）在这里可以看到惊人的相似之处。 在这个微积分的背景下，这是原因-FDNDFD注：↑=，↓= nor，= xorJ. Raghunandan，A.J.Summers/Electronic Notes in Theoretical Computer Science 171（2007）8599\/\/\/\/--ΓA，Δ- -Γ，B Δ（→L）Γ<$A，Δ Γ，B<$Δ（−R）ΓA−B，ΔΓA→B，ΔΓ（A→B），Δ（€R）- -- -- -Γ，A<$B， ΔΓA→B，Δ（→R）（€L）Γ，A<$B，Δ（−L）Γ，A−B<$ ΔΓ，<$（A→B）<$ Δ图五.推导出不同连接词的规则-能够将析取视为另一种对输入求反的结果是仅对连接词的一个输入求反，连接词又对应于规则中交换侧的公式之一的绑定出现例如，蕴涵可以通过对第一个输入（A→B<$$>A<$B）进行迭代来从析取中获得。 这一点也可以通过比较两种规则来看出。在这个意义上，在微积分中，偶蕴涵可以看作是一种配对。检查X的语法（为简洁起见，与在规则中进行比较），例如，对Q[x]y[x]R进行的语法定义是两个项Q和R的对，绑定一个项的输出和另一个项的输入。 出口z^Pβ^·γ是一种可以将该粒子消除的方法;它提供了一种连续性或连续性这两个元素对，类似于（例如）的术语对应于EML。从上面的讨论中可以看出，一旦知道了特定连接词的否定规则（以及因此的适当的术语表示），就可以容易地导出连接词的否定和对偶以及通过对输入进行否定而获得的特别是这六个连接词它们通过图4中的各种箭头（包括箭头A、箭头B和箭头C）彼此连接）都有相关的规则。事实上，每一个都可以被看作是一种配对连接词;区别在于输入或输出是否被约束在组成配对的两个子项中，以及配对是否在引入的输入或输出上可用。我们有时会把这六个连接词称为配对连接词。从图4中可以看出，剩下的连接词是两个一我们已经讨论了否定连接词的语法和主要规则，而同一连接词可以被看作具有非常琐碎的计算内容（充其量它提供了一种别名，连接词是绑定的100J. Raghunandan，A.J.Summers/Electronic Notes in Theoretical Computer Science 171（2007）85在子项内，然后立即以新名称再次导出T和T连接词是相当不寻常的，因为事实证明，它们都没有合理的证明规则来将连接词引入到T的一侧（事实上，可以添加一条规则，但这相当于弱化的特殊情况在T的情况下，只有一个合理的规则，在右边，对称地介绍仅在左侧有一个介绍规则。 这些规则如下：（TR）Γ，ΔT， Δ（比利时法郎）Γ，πΔ由于这些规则引入了一个新的公式，而没有约束任何现有的公式，因此可以看出它们被一些项所占据，这些项使得可以使用不与任何东西连接的输出（相应地输入）就归约规则而言，不可能添加通常的主逻辑规则，因为不存在左和右对。正确的连接方式当人们考虑（例如）TR规则之间的切割时在左边和一些其他的术语在右边，很明显，连接器绑定在另一侧的削减必须引入削弱（如果削减是可打字）。以这种方式，表示T和T的术语可以用于提供“死端”切割，当评估时，其简单地消失（参见图10）。引理3.5）。作为可表达的计算内容类型的一个例子，如果一个人向现有的X-演算添加了用于RNL规则的语法，那么一个人可以表达对连续的直接操作。（因为用→和可以表示否定）。作为一个单独的点，应该注意的是，如果在一个术语演算中使用一个以上的逻辑连接符，那么将有可能在它们各自的语法表示之间创建（不可键入的）切割例如，如果一个人要用中介来切割TR没有合理的方法来评估削减。因此，当使用一个以上的逻辑连接词时，范式的概念就被扩展了;特别是，它将有可能有（不可键入的）包含切割的范式这里只剩下两个二元连接词需要讨论：参与式if’) and 这两个词在图中是相关的;事实上，这两个连接词是通过否定、二元性而相关的，并且可以通过对其中一个输入进行重复而从另一个获得。在某种意义上，它们所描述的（类似的）操作很难与任何其他联结词直接联系起来;没有“简单的”等价公式可以用其他联结词来表达这些联结词。当然，我们也可以用其他的连接词来编码这些连接词，但正如下面的结果所示，它们必须以一种更复杂的方式表达定理5.3（表示Participant，n）设S是不含Participand n的二元布尔联结词的集合. 不存在仅使用S中的连接词可表达的公式F，使得：(a) F在逻辑上等价于A Participate B或A B。(b) A和B在F中只出现一次。注5.4相反，S中的所有连接词都可以用S中的其他连接词来表达，只使用A和B一次;在某种意义上，它们可以比所讨论的两个连接词更直接地表达。J. Raghunandan，A.J.Summers/Electronic Notes in Theoretical Computer Science 171（2007）85101下面的技术引理允许我们展示定理：引理5.5（移除T、Id和Id）如果F是使用二元连接词以及命题变量A和B构造的公式，则存在公式G使得：(a) GF.(b) A和B在G中出现的次数并不比在F中出现的次数多。(c) 没有其他命题变量出现在G中。(d) G不使用ID连接词。(e) 要么G不提及T和，要么G = T或G =。证据这里只给出证明的概念。首先，很明显，ID连接词的任何用法都可以简单地删除，同时保持一个等价的公式。然后可以定义一个重写系统（使用等价）来消除所有出现在另一个连接词下面的T和T。例如，将A→ T改写为A，并且A →A → A改写为<$A。很容易证明重写系统是强规范化的，并且它的规范形式满足列出的标准Q证据 [定理5.3]设存在这样一个公式F，求一个矛盾.显然，F不可能等价于T或。 因此，根据引理5.5，存在一个公式G<$F，它没有提到T，k或id，而只提到A和B一次。注意，Participate和Patient分别是两个参数的奇偶校验函数，以及它的否定。由于AParticipateB的真值取决于两个参数的真值，G必须只提到A和B一次。现在去掉可能出现的任何双重否定，得到公式 GJ.在不失一般性的情况下，GJ 是 公 式 1（（2A）·（3B））的一部分，其中是一个或多个，其中1、2、3是可能出现或可能不出现的位置。再次不失一般性，通过假设GJ=AParticipateB（对于A的情况是相同的）。AParticipateB总是依赖于A和B的值来评估其结果，而根据定理5.1（3），·并不总是依赖于其参数的值，因此GJ并不总是依赖于A和B的值。矛盾Q这一定理表明，两个连接词Participate和Please可能有一些其他二元连接词没有的内部复杂性。研究这两个连接词的计算内容似乎是很自然的，这似乎是迄今为止文献中没有尝试过的。特别是，似乎没有为这些连接词定义切割消除规则（或类似地，自然演绎设置中的证明还原规则）。正是这些问题激发了下一节的讨论。6解释if-and-only-if在本节中，我们研究逻辑连接词“if-and-only-if”（简称“i "）的计算行为我们同样可以选择研究否定102J. Raghunandan，A.J.Summers/Electronic Notes in Theoretical Computer Science 171（2007）85这个连接词例如，我们可以通过等价AParticipate B<$$>（A<$B）<$（A<$B）来确定i连词的左右引入规则的形式由此，我们可以构造导子，其结论在一个子的左边和右边（详细证明见附录A）。压缩这些派生给我们图6所示的（ParticleL）和（ParticleR）引入规则，我们可以用通常的方式使用X风格的术语。我们将计算公式[M μ ^σ ^[y]^i^j N]和[x ^P α ^，z ^ Q δ ^]分别表示为[ M μ ^ σ ^ [ y ] ^ i ^ j N ]和[ x ^ P α ^，z ^ Q δ ^ ]。很好。Γ<$A，B， Δ Γ，A，B<$ Δ Γ，（AParticipB）<$Δ（参加）Γ，A<$B，Δ Γ，B<$A，ΔΓ<$（AParticipB），Δ（参加）见图6。ParticipL和ParticipR引入规则i 的 主 要 逻 辑 规 则 应 该 转 换 一 个 证 明 ， 将 一 个 （ ParticipR ） 公 式 与 一 个（ParticipL）公式切割在一起，或者用X表示法，（[x^Pα^，z^Qδ^]。γ）γ，（[Mμ，σ，[y]，γ，γ，N ]），γ，（[M μ，σ，[y]，[N]），γ，γ减少不是直接确定的。每个连接词的规则都绑定两个输入和两个输出，每个规则都有两个子项。我们观察到，这些术语与那些用来表示蕴涵连接词的术语（即X的句法，定义3.1）有着惊人的相似之处。i-right术语让人想起导出术语，除了在同一个接 口 上 可 以 使 用 两 个 “ 函 数 ” 而 不 是 一 个 （ 注 意 ： AParticipateB<$ （ A→B ）<$（B→A））.左项是中介的remi- niscent，每个子项上有两个binder，而不是一个。在这种情况下，内存驱动器R[l]kS，我们可以通过提供的连接器将内存R和S连接一般来说，直接将k与k联系起来会导致我们的“蕴涵”必须是A → A的形式的限制允许插入导出的主体以如果我们把i-左项看作是一种中介，那么我们必须解决的问题又是连接项M和N之间的输出和输入。然而，即使在一般情况下，M和N也有具有共同类型的绑定连接符;看起来我们已经拥有了将这些术语连接在一起所需的一切直接地。Mμp与h^iN和Mσp相互连接w ith^jN.一般来说，这是不能做到的，因为底层的证明序列将两个输入的类型解释为合取地读取的公式，并且将两个输出的类型解释为析取地读取的公式。在此上下文中，M表示类型A的值或类型B的值（不严格地说，类型A的值为B），而N需要类型A的值和类型B的值（不严格地说，需要类型A的值为B）。因此，我们在尝试连接这两个证明本质上是确定我们如何从A<$B类型的值转换为A<$B类型的值，即我们直观地需要（A<$B）→（A<$B）类型的值J. Raghunandan，A.J.Summers/Electronic Notes in Theoretical Computer Science 171（2007）85103一Mμ：AAμ^†x^APBα^†^jσ：B B