理论计算机科学电子笔记172（2007）33-67www.elsevier.com/locate/entcs事件域、稳定函数与证明网Samson Abramsky萨姆森·阿布拉姆斯基1，2牛津大学计算实验室Wolfson Building，ParksRoad，Oxford OX1 3QD，英国摘要我们追求揭示逻辑系统的“证明空间”的内在数学结构的程序我们研究乘加线性逻辑（MALL）的情况。我们使用域理论的工具来开发MALL的证明网的语义概念，并证明了序列化定理。这篇文章是一个关于与RadhaJagadees an[5]和Paul-Andr'eM ell i`es一起工作的一个新的尝试[6]。关键词：线性逻辑，证明网，域理论，事件结构，稳定函数。奉献：Gordon Plotkin是我作为一个re-trouble的主要塑造者，因为他一直在计算语义的整个领域。他也是一个真正的朋友，这么多年来。在他六十岁生日之际，我非常高兴地把这份文件献给他。 我希望他会对它为语义研究的一些基本工具所发现的新用途感到高兴，他已经做了很多工作来创建和开发。1引言关于逻辑与结构的关系，我们可以区分出两种观点：(i) 描述性的观点。逻辑是用来谈论结构的。这是模型论中的观点，也是逻辑的大多数应用（时态逻辑，MSO等）中的观点。在验证中。这是迄今为止更普遍和更广泛理解的观点。(ii) 内在的观点。逻辑是结构的体现。 这是隐含地或明确地，在Curry-Howard同构中所采取的观点，以及更多1本研究得到EPSRC Grant EP/D 038987/1的部分支持2电子邮件：samson@comlab.ox.ac.uk1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.02.00334S. Abramsky/Electronic Notes in Theoretical Computer Science 172（2007）33一般在结构证明理论，并在（大部分）范畴逻辑。例如，在Curry-Howard同构中，人们不使用逻辑来谈论函数式编程;相反，逻辑（在这方面）是函数式编程。如果我们要在逻辑的证明理论中找到结构，我们面临着一个挑战。证明系统受制于许多次要的“设计决策”，这并不能保证所描述的对象（形式证明）具有健壮的内在结构。用几何学作类比也许是有用的现代几何学的一个主要关注点是寻找内在的，通常是无坐标的，描述性的，地球物理学中的天体是地球物理学中的天体。我们来看看Prof中syntax的基本原理理论类似于几何学中的坐标;对计算来说是无价的，但对发现潜在的不变结构来说是一个障碍。在寻找证明的更内在的描述，它们的几何结构，以及它们在割消下的动力学方面，一些特别有前途的进展发生在线性逻辑中的证明网的研究中[16]，以及相关的相互作用几何的研究[18]。在语义方面，博弈语义学和完全完备性结果的发展[5]（以及随后的[24，9，6，14，10]）极大地丰富和深化了结构视角。在本文中，我们建立在以前的联合工作与拉达Jagadeesan[4]和Paul-AndreMelli`es[6]。 本文研究了多址线性逻辑（MALL）。我们使用域理论的工具来开发MALL的证明网的语义概念，并证明了这个概念的序列化定理1.1相关工作我们建立在以前的工作证明网和语义的MALL。特别是Faggian和Curien最近关于Ludics网的工作[15，12]也明显相关-尽管应该强调的是，Ludics处理的是极化的（因此是“序列化的”）线性逻辑，而我们处理的关于这个问题的进一步讨论见[2最近对MALL证明理论的一个重要贡献是Hughes和van Glabeek的工作 [21]。他们给出了可以被认为是MALL的证明网的最佳概念，在这个意义上，它包含了重建一个证明所需的最小信息我们希望最终扩展我们的方法来分析他们的证明网概念，并将其与我们的语义思想联系起来。然而，这是留给未来的工作。最 后 ， 如 前 所 述 ， 本 文 建 立 在 我 们 自 己 以 前 的 工 作 基 础 上 ， 其 中 有RadhaJagadeesan[4]和Paul-Andr′eMelli`es[6]。实际上，产生我们的证明网的“语义”概念的基础模型本质上是从[ 4 ]中给出的构造中导出的Int或G结构的前身[22，1]）;甚至是域理论用于加法部分的过程，其为每个加法分辨率构建树，以S. Abramsky/Electronic Notes in Theoretical Computer Science 172（2007）3335它是粘在叶子上的一个排列，给出乘法结构，可以在那篇论文的第7节中找到雏形。本论文的主要新颖之处在于证明网的语义发展我们给出了我们的概念的序列化定理的详细证明这与[20]中的证明非常接近，但是考虑到我们的证明网的非常不同的形式-没有明确的链接或权重，[20] - 这似乎是值得的。此外，我们还得到了一个比[20]更强的结果.证明网和可证明之间存在多-多关系;而我们定义了从可证明到证明网的一个规范映射，使得从一个证明得到的序列化的证明网总是表示一个近似于我们开始时的证明网。事实上，这个结果只能在我们的领域里有意义地陈述-理论设置，其中有一个自然秩序的证明网。这反过来又打开了一个有趣的结构的“并行度”在每个等价类的证明网下的本文实际上是一个更大的工作[3]的一部分，在这个工作中，我们回顾了[6]中的工作，并证明了MALL的并发游戏语义的完全完备性。[6]中的大量工作都是在[20]意义上的证明结构的映射策略上进行的目前的处理，其中我们使用了一个证明网的概念，它接近于[6]中使用的策略的语义概念，并直接证明了该概念的序列化，似乎更独立和有启发性。1.2纲要我们简要概述了论文的内容。在第2节中，我们回顾了MLL的证明网和序列化，作为后续处理MALL的热身和模板在第3节中，我们回顾了MALL的基本语法我们将在第4节中回顾我们将使用的领域理论的一些概念第五节介绍了证明结构的语义概念。与其他概念的比较，以及语义证明结构的域理论精细结构证明网的相应概念在第7节中定义，序列化在第8节中证明。第9节结束确认如前所述，本文中的工作建立在以前与R和Jagadees和Paul-Andr'eMelli`es的联合工作的基础上。我与他们以及Dominic Hughes进行了非常有启发性的讨论，并澄清了他与Rob van Glabbeek在MALL proof-nets上的工作36S. Abramsky/Electronic Notes in Theoretical Computer Science 172（2007）332MLL线性逻辑的乘法片段，减去单位--此后的MLL --是一种逻辑天堂。一切都工作得很好，很顺利，很自然。这些想法简单而令人信服，但并非微不足道。 因此，我们将使用它作为我们随后讨论乘加线性逻辑（MALL）的模板。2.1MLL的扩展该系统的公式是从文字，即命题原子α，β，. ..，（正字面值），以及它们的否定项α，β，.，（否定字面值），由语法A：：= α |α⊥|AA|AA。这里的“Times”和“Par”是乘法连接词。否定被定义性地扩展到一般公式，（A<$B）=A<$B<$（AB）= ABA= A.我们还定义了线性蕴涵AB通过：AB= 一个大的。MLL中的一个表达式是一个表达式r，其中r是一个有限的公式序列。2.2MLL的序列演算公理/切割结构规则ID► A，A，► Γ，A Δ，A► Γ、 Δ切割► 交易所乘法► σΓ► Γ，A < $Δ，B► Γ， Δ，AB时间A，B► Γ，AB标准杆2.3证明结构我们现在转向句法的“几何化”。我们将以一种流线型的形式引入（免裁剪）证明结构[17，5]。我们首先考虑公理被限制在原子实例中的微积分版本► α，αId请注意，对一个Γ的任何无割证明都必然会按照规则的某种应用顺序再现Γ中公式的结构，而这并不意味着S. Abramsky/Electronic Notes in Theoretical Computer Science 172（2007）3337我内在意义，除非它表明文字的出现是如何由公理成对引入的。因此，我们大胆地说，证明的基本内容就是这个信息，它可以表示为：匹配的文字出现对的列表{li，lj}，其中lj=lj。 更方便的是，我们可以把一个证明结构看作是在Γ中文字出现的集合L（Γ）上的一个尊重文字的对合：即一个置换σ：L（Γ）−→L（Γ）使得σ=σ−1，并且如果σ（a）=b，则λ（a）=λ（b），其中λ（a）是a是出现的文字。请注意，这样的函数必须是无定点的，即对所有a∈ L（Γ），σ（a）/=a例如考虑一下这个符号。事实上，只有两个无割证明这个定理（对应于恒等式和扭曲映射）。它们对应于以下证明结构：α⊥αα⊥αα⊥αα⊥⊗αα⊥αα⊥αα⊥αα⊥⊗α2.4将顺序证明解释为证明结构我们现在展示如何将每个证明都解释为一个证明结构。公理► α，αId我们指定换位αParticipateα。张量► Γ，A <$B， Δ► Γ，A<$B， ΔTimes假设我们把置换σ分配给了πΓ，A的证明，把τ分配给了πB，Δ的证明。然后我们将不交并σ+τ分配给Γ，A<$B， Δ的证明这是有意义的，因为L（r，A<$B， Δ）是L（r，A）和L（B，Δ）的不交并。因此σ + τ（a）= σ（a），a∈ L（Γ，A）， σ + τ（b）= τ（b），b∈ L（B，Δ）.ParΓ，A，B► Γ，AB标准杆由于（本质上）L（Γ，AB）=L（Γ，A，B），我们可以将相同的置换分配给结论作为前提！38S. Abramsky/Electronic Notes in Theoretical Computer Science 172（2007）332.5证明网这就提出了一个问题：我们如何描述哪些排列作为对证明的解释而出现？如果我们能做到这一点，我们就有权把这种排列看作是证明的内在表现，揭示它们的本质结构和内容。第一种方法是通过几何标准：这是证明网的概念。切换图的转换S将L或R分配给的每一次出现。给定一个矩阵T、一个证明结构σ和一个切换S，切换图GT（σ，S）具有：• 子公式在Γ中的出现作为顶点;• 对于每次出现A<$B，连接A到A<$B的边和连接B到A<$B的边;• 如果S将L分配给AB，则连接A到AB的边，以及连接如果S将R赋值给AB，则B赋值给AB;• 如果σ（a）=b，则连接文字出现a和b的边。Danos-Regnier准则证明结构σ是MLL证明网，如果对每个开关S，GΓ（σ，S）是非循环连通的.命题2.1（合理性）作为对非线性证明的解释而产生的证明结构是证明网。MLL证明网的主要结果如下[16，13，19，26]：定理2.2（序列化定理）每个证明网都是由一个序列证明产生的.证明中的关键情况是当所有非字面结论都是张量时;我们需要找到一个分裂张量A<$B，这样我们就可以将Γ，A<$B分裂为Γ1，A和Γ2，B，这样我们的证明网就可以分解为两个子证明网。这是通过帝国的概念来实现的。我们将看到所有这些想法在更复杂的MALL环境中详细发展讨论通过文字出现的排列来表示证明结构的步骤--这不是证明网的标准公式[16，19，26] --已经是朝着证明的语义视图迈出的重要一步。它直接导致相互作用几何[17，18]和完全完备性结果[5]。这些反过来又提供了一个优雅的组成帐户的动态削减消除。我们的方法可以被看作是这些想法在MALL更丰富的环境中的延续，在那里需要新的想法。S. Abramsky/Electronic Notes in Theoretical Computer Science 172（2007）3339我3关于MALL该系统的公式是从文字，即命题原子α，β，. . .，以及它们的否定式α<$，β<$，.根据语法A：：= α |α⊥|AA|一一|AA|A&A。在这里，“”和“”是乘法连接词，而“”是加法连接词。否定被定义性地扩展到一般公式，（AB）=AB（AB）=AB（AB）=AB（AB）=ABA= A.MALL中的一个表达式是一个表达式r，其中r是一个有限的公式序列。3.1MALL的顺序演算公理/切割结构规则ID► A，A，► Γ，A Δ，A► Γ、 Δ切割► 交易所► σΓ乘法添加剂► Γ，A► Γ，A < $Δ，B► Γ， Δ，AB时间► Γ，B► Γ，A，B► Γ，AB标准杆► Γ，A Γ，B► Γ，AB+ L► Γ，A+B+ R► Γ，AB，带3.2广义公理为了进行序列化定理的证明，引入广义公理是有用的，如下[19，20]。在我们的设置中，以下面的方式进行是最我们引入了一组参数，. ，不同于命题原子α，β，. . .每个参数k具有元数k，并且参数实例k1，. ，pk10。公式可以从参数实例以及命题原子构建我们通过以下方式扩展否定的定义：ξ⊥= ξi.40S. Abramsky/Electronic Notes in Theoretical Computer Science 172（2007）33对于arityk的每个参数k，都有一个公理规则（► 2001年，...，阿斯克·阿克斯这个想法是，2011年，...，k表示“框”的结论。给定Γ[1，.]的一个无割证明，，k]，以及Δ = B1，…，Bk，我们可以形成Γ[Δ/λ1，.，.，以102为单位。3.3事件和线性上下文在一个给定的公式或命题中，有必要谈到公式的出现。这通常会导致尴尬，不精确，或两者兼而有之。处理事件的一种方便方法是通过线性上下文。这些都是用与公式或序列相同的语法构建的，但只使用了一个“洞”[·]。举例说明，公式A_（[·] C）可用来证明公式A_（[·]C）中B的线性语境与事件有明显的双唯一对应关系，并允许方便的归纳定义。 我们将在公式A在公式B（或一个Γ）中的出现O和相应的上下文C[·]之间自由地传递，因此C[A]=B（或C[A]=Γ）。我们使用字母O、P、Q、R表示出现次数，V和W表示With出现次数，L和M表示文字出现次数。我们写O（Γ）为在一个集合中出现的集合;和L（Γ）为在一个集合中出现的集合。文字的出现4域名背景为了使本文合理地自成一体，我们将简要地回顾一下域理论的一些背景材料一个有用的参考文献是[27]。尽管我们会在一个更受限制的环境中工作。这些想法的开创性参考文献是[23，25]。我们做了一个全局假设，即本文中考虑的所有域都是有限的。这意味着我们可以忽略完整性和连续性的所有考虑。本节中的所有定义都是在假设基础偏序集是有限的情况下做出的。我们将专门研究有界完备偏序集;也就是说，部分有序集，其中每个有界子集（即，在偏序集中具有上界的子集）具有最小上界。这样的偏序集也有非空的相遇。特别要注意的是，有界完备偏序集有最少的元素，记为n。偏序集中的素数是一个元素p，使得p±xHy蕴涵p±x或p±y。我们把P的素元素的集合写成Pr（P）。 事件域是有界的完全偏序集D，其中每个元素都是素数的最小上界在它下面，我们写.x= ↓Pr（x），S. Abramsky/Electronic Notes in Theoretical Computer Science 172（2007）3341其中↓Pr（x）={p∈Pr（D）|p± x}。命题4.1事件域是分配的：即xH（yHz）=（xHy）H（xHz）当y和z有界时。换句话说，每个主下集↓（x）都是分配格。偏序集中的覆盖关系定义为：x<$y<$xиy<$（x±z±y<$（x = z）<$（y = z））.事件域中的原子是一个元素a，使得 事件域是原子的，如果除了素数之外的所有素数都是原子。另一类事件域是（分配的）具体域，它满足一个附加公理。我们忽略了定义，可以在[23，27]中找到。Domain上的构式我们将在域上使用一些结构• 一点域，写1。• 笛卡尔积D×E，逐点排序。• 通过在D上附加一个新的底元得到升力D。• 通过形成D和E的不交并而得到的分离和（D+E）是E，并且邻接底部元件。• 平坦域X通过将一个底元素邻接到一个集合X上而得到，其序关系为：x±yi<$x=<$x或x=y。• 集合X上的部分双射的集合，按包含排序• 对于Sierpinski域，我们使用符号O = 1π，即， 二元晶格T.命题4.2事件域和具体域在所有上述构造下都是封闭的。除了提升和分离和之外，原子域都是封闭的。记法我们写Max（D）为事件域D的最大元素的集合，MaxPr（D）为D中的最大素数的集合，即MaxPr（D）=Max（Pr（D））。因此，一个4.1Domain上的函数域之间的所有函数将被假定为单调的：x± y<$f（x）±f（y）.42S. Abramsky/Electronic Notes in Theoretical Computer Science 172（2007）33我们将关注一个额外的性质，即稳定性[8]。 一个函数f：D−→E是稳定的（第一个版本），如果当x和y有界时，f（xHy）=f（x）Hf（y）。有一个等价的定义，它更有启发性，对我们更有用。 假设我们有一个输入x∈D，y∈E，使得y±f（x）。 我们定义稳定模为最小xJ±x，使得y±f（xJ）。这样的元素一般不存在。如果它总是这样，我们说f是稳定的（第二个版本），并用M（f，x，y）表示这个模。如果f稳定（第一个版本）我们可以通过以下方式定义这个模数：M（f，x，y）=.{xJ±x|y±f（x，J）}。相反，我们可以证明，如果D和E是事件域（实际上更一般），则稳定性的第二个版本意味着第一个版本。我们将提到的另一个性质是顺序性。我们不看这个，看这个，看这个。命题4.3稳定函数和序列函数在与前面小节中描述的整环上的构造相关的所有下列运算下都是封闭的：常数函数、合成、恒等式、投影、配对、注入和通常的条件。我们还将使用嵌入投影，它表达了一个域如何作为另一个域中的子域。一个嵌入投影被写入e：D E：p其中D和E是事件域，e：D−→E和p：E−→D是单调映射，满足：p∈ e = 1 D，e ∈ p ± 1 E。我们在这里使用的函数的顺序是逐点顺序：f± g惠益x. f（x）± g（x）。这是我们将使用的函数的唯一顺序，即使是稳定函数;我们永远不需要考虑函数空间和高阶函数。4.2Domain的分解我们提出了一些技术概念，这些概念将被证明是有用的。我们在事件域D上引入了限制的概念。 如果d是一个元素，D，P是D中的一组素数，我们定义：.dTP ={p ∈ ↓Pr（d）|p ∈ P}。我们可以用以下两种等价的方式之一来定义D的子域DP•DP是由P生成的，作为P的有界子集的连接的集合。S. Abramsky/Electronic Notes in Theoretical Computer Science 172（2007）3343我我• DP是微分rP：d<$→dTP的像。我们可以定义一个嵌入投影e：DPD：p其中e：DP<$）D是包含，p（d）= dTP。现在假设我们有一个单调函数f：V1× V2−→ D。我们假设给定的素数集P1，P2≠D，以及相应的嵌入投影ei：DiD：pi， i = 1，2。我们假设子域Di本身是事件域。注意，存在稳定的嵌入投影φi：ViV：πi，i = 1，2φ1（v1）=（v1，v 1），φ2（v2）=（v 1，v2），其中V=V1×V2。 因此，我们可以定义函数fi= pi<$f <$φi：Vi−→ Di i = 1，2.注意，如果f是稳定的，那么fi也是稳定的，因为φi是稳定的，而pi保持所有的满足，因为它是一个投影。我们如何从f1和f2（近似）重建f？我们假设f <$φi通过包含Di<$）D，i = 1，2因式分解。因此，我们可以定义稳定函数。fJ= ei<$fi <$πi：V −→ Di = 1，2.注意，f J± f，i = 1，2。因此，我们可以定义f1[f2]：V−→E，f1[f2]：v <$→ FJ（v）Hfj（v）.1 2命题4.4（i）f1 [f2] ±f.(ii) 若fi±gi，i = 1，2，则有f1 [f2] ±g1 [g2].5语义证明结构我们首先回顾Hughes-van Glabeek（HvG）对证明结构和证明网的定义[21]。44S. Abramsky/Electronic Notes in Theoretical Computer Science 172（2007）33HvG证明网他们将MALL的加法归结定义为每次出现加法连接词的一个变元被删除的结果&。公理链接是某个文字的一对互补出现之间的边。在Γ的加法归结上的链接λ是公理链接的集合，其中的每一个涉及保留在加法归结中的出现，并且使得每一个加法解析中剩余的文字出现恰好在λ中的一个链接中。Γ的A-归结是在Γ中的每一次出现中删除一个变元的结果。如果链接中出现的每个文字都在-解析中，则链接在-解析上。T的加法归结的A-转换是删除加法归结中的每次出现的一个自变量的结果。定义5.1用于Γ的HvG证明网是Γ的加法分解上的链接的集合Θ，使得：(i) 对于Γ的每一个-分解，在该-分解上恰好有一个连接λ∈Θ。(ii) 每每个λ∈Θ的-交换是连通的和非循环的。(iii) 更进一步，相当微妙的技术条件称为切换。我们将不在这里进一步讨论切换。它仍然是一个远离直觉的概念，未来研究的目标是更好地理解它。我们希望本文件中开发的工具将有助于实现这一目标。我们将取一个带有术语的小库，并将满足上述第一个条件的连接集称为HvG证明结构。5.1HvG的论域形式化Hughes和van Glabeek使用的各种概念，如加法分辨率，-分辨率等，是非常直观的。他们还提供了这些概念的正式定义，在标记图。我们将寻求一种替代的，更这揭示了这些定义中固有的一些数学结构，但在[21]中没有明确说明，这将证明是有用的和有启发性的。我们的方法将建立在[4，6]的语义见解上。给定一个MALL环Γ，我们将引入若干个与Γ相关联的事件域.我们将在MALL证明网的演示中使用这些S. Abramsky/Electronic Notes in Theoretical Computer Science 172（2007）33455.1.1形式化加法决议首先，我们为每个MALL公式A定义一个偏序集D（A），归纳如下：D（α）=D（α）=OD（AB）=D（AB）=D（A）×D（B）D（AB）=D（A<$B）=（D（A）+D（B））<$D（λ）=O.我们把这个赋值推广到序列Γ = A1，.，Ak由D（r）= D（A1）×···× D（Ak）。注意，这与将λ视为其公式的Par一致。回想一下，O=1<$是二元晶格<$T。这些定义背后的直觉遵循[4，6]中的定义，并在[2]中进行了广泛的讨论简单地说，把多重连接词解释为产品反映了它们与并发性和因果性的联系，而把加法解释为分离和反映了它们与选择、冲突和因果性的联系。同步的时刻（cf. [16、17]）。谢尔宾斯基域O对原子的解释应该被看作是一个方便的例子，在这个例子中，命题原子实际上是一个参数（实际上是函子）定义。作为参数。为了方便起见，我们通常将DΓ写成D例如考虑<$r =（α<$α<$）（α<$α <$），α<$α。 定义域DΓ为：（O2 + O2）<$× O2.我们将该域的底部元素和原子说明如下：（inl（（，）），（，））（inr（（，）），（，））（，（T，））（，（，T））（，（，））增加第一个分量的排序以决定分离的和对应于解决加法选择。我们现在将这个形式结构与HvG概念联系起来，并有以下简单的观察。命题5.2D Γ的极大元与Γ的加法分解一一对应;而D Γ的极大素数与Γ中的文字和参数实例的出现一一对应。46S. Abramsky/Electronic Notes in Theoretical Computer Science 172（2007）33这个命题的后半部分显示了使用O作为文字解释注意，例如，任何纯乘法的解释都是在以下中的文字出现上索引的乘积OL（r）：I. 有一个唯一的最大元素，即元组，其中所有组件是T。 最大素数是那些元组，其中正好有一个组件是T，产生双射对应。如果我们使用一点域1而不是O，那么相应的乘积仍然只有一个元素！在上面的例子中，注意，这个公式有两个加法分解，对应于选择的左或右自变量;对应的最大元素是（inl（（T，T）），（T，T））和（inr（（T，T）），（T，T））。最左边的α（正文字）的出现对应于最大素数（，（T，））。符号对于Γ中的每个文字出现L，我们为DΓ中对应的最大素数写一个L。给定d∈ DΓ，我们定义：|D|={aL|L ∈ L（Γ），aL± d}.事实5.3如果d±dJ，则|D|Γ⊆|DJ|I.5.1.2形式化链接为了明确地指定Γ的加法分解上的链接，我们必须给出两件事：• 根据命题5.2，它对应于DΓ的一个极大元d。• 将加法分解中的文字出现划分为互补对{L，L<$}的一组公理链。这相当于指定一个关于文字的部分对合（就像MLL一样），|D|.这自然被形式化为一个相关和。我们将集合X上的部分双射的集合记为S（X），按包含排序。用图表示部分双射，我们有：X<$Y =<$S<$（X）<$S<$（Y）。我们现在定义预链接的域：（1）A = A（|D|）={（d，π）|10- 12 - 13 - 2000张世荣（|D|）}，并进行逐点排序：（d，π）±（dJ，πJ） d±djS. Abramsky/Electronic Notes in Theoretical Computer Science 172（2007）3347⊥我们定义一个环为E Γ的极大元（d，π），使得π是上的尊重文字的对合。|D|.继续示例继续来自先前子部分的示例，Dr的最大元素是d=（inl（（T，T）），（T，T））。对应的文字出现集合是|D|={ai|i= 1，.，4}，其中a1=（inl（（T，）），（，）），a2=（inl（（，T）），（，）），a3=（，（T，）），a4=（，（，T））.加法分辨率d上的链接是（d，{a1Participa3，a2Participa4}）， （d，{a1Participa4，a2Participa3}）.我们将这些联系的第一个说明如下：α⊥α⊥α α⊗&5.1.3正式化-决议设W（Γ）是Withs（即形式AB的子公式）在Γ中出现的集合。设VΓ是从W（Γ）到B={ 0， 1}的偏序函数集，序W（Γ）通过包容。 等价地，VΓ=B，是一个双域的乘积。 我们称VΓ的元素是（部分）赋值;最大元素是全赋值。 这些对应于-决议在一个明显的方式。如果v是一个赋值，且W∈ W（Γ），我们定义一个新的赋值v<$W，其中v<$W（WJ）=v（WJ），WJ/=Wv<$W（W）=<$v（W）其中：<$0= 1， <$1= 0， <$1 = 0。我们称之为我们还定义了估值v\W，使得v\W：W→ n，并且v\W：WJ→v（WJ），对于WJ48S. Abramsky/Electronic Notes in Theoretical Computer Science 172（2007）33W. 这扩展到一组With出现，v\{W1，. ，Wk}，以明显的方式。S. Abramsky/Electronic Notes in Theoretical Computer Science 172（2007）33495.1.4HvG证明结构的形式化我们现在可以用我们的术语形式化HvG证明结构。HvG证明结构的定义：第一次尝试MALL矩阵上的HvG证明结构是函数f：Max（VΓ）−→Max（EΓ）它赋予每个&-分解（全赋值）一个在Γ的加法分解（E Γ的极大元（d，π））上的连接，使得π是在|D|）.这个定义没有抓住HvG的定义，因为我们没有表达对应于一个-归结的连接必须在那个-归结上的条件。直觉上，这表达了这样一种想法，即With归结是我们通过下面的（非）例子来说明这个条件的必要性非示例考虑<$r =α<$（αα），α<$，和连接集{λ1，λ2}：λ1λ2α α α α α⊥⊕&⊕如果我们把第一个连接λ1赋给使唯一的伴随出现W为0的赋值，把第二个赋给设为W= 1的赋值，那么我们得到一个满足上述定义的函数;然而，这组连接显然不对应于任何证明。然而，这两个链接都在-赋值[W= 1]上，因此这不是HvG证明结构。为了公式化连接是在-&分辨率上的条件，我们需要捕捉这样的想法，即在加法分辨率d中剩余的每个文字出现L，即 使得一个L± d，诱导出一个关于出现的部分赋值，与决议一致。要做到这一点，我们需要把在D Γ中的出现与DΓ的元素联系起来。50S. Abramsky/Electronic Notes in Theoretical Computer Science 172（2007）33Q⎨语义发生对于A中的一个多变量B的计算，我们定义QC[·]、A ∈Pr（D（A））：Q[·]<$A=ΔD（A）QC[·]mB<$AmB=（QC[·]<$A，n），m∈{n，}QAmC[·]<$AmB=（λ，QC[·]<$B），m∈{λ，}QC[·]aB<$AaB=inl（QC[·]<$A），a∈{，n}QAaC[·]<$AaB=在r（QC[·]<$B）中， a∈{，<$}我们将其推广到序列Γ = Γ1，A， Γ2中的出现，Qr 1，C[·]，r 2，r=（C， . . ，，QC[·]<$A，，. . . ，J.）。继续示例在我们的运行示例中，唯一的With出现W具有对应的素数W=（，（，））。注意，一般来说，许多不同的句法出现可以映射到D Γ中的同一个素数。我们定义一个函数输出：DΓ−→VΓ这使得明确的加法决议如何诱导的价值（一般是pal）上的智慧。对于chW∈W（Γ），其中h∈C[·]，其中C[AB] = Γ，我们定义：⎧QC[[·] B]<$r±d输出（d）（W）=⎪1，QC[A[·]]<$r±d但是，他没有定义的直接后果如下：命题5.4如果d∈ DΓ且W∈ W（Γ），则：QW <$/± d输出（d）（W）= ω。继续示例在我们的运行示例中，加法分辨率（inl（（T，T）），（T，T））通过out映射到赋值[W = 0]，而（inr（（T，T）），（T，T））映射到[W= 1]。注意，（T，T）映射到[W = W]。为了方便起见，我们将此函数提升为链接：p：EΓ−→ VΓ：：（d，π）›→ out（d）。S. Abramsky/Electronic Notes in Theoretical Computer Science 172（2007）3351Q1KQQ现在给定一个总赋值v和一个连接（d，π），我们可以定义（d，π）为v如果对于所有文字出现L：aL±d=输出（aL）±v.注意，我们使用函数的逐点顺序来比较（一般是部分的）赋值out（aL）与v。有一个最终的微妙。证明结构的HvG定义只是一组链接。当我们将它们的定义“统一”为一个从赋值到连接的函数时 因此，对于每个-分辨率，在该-分辨率上的集合中存在唯一链接的条件转化为函数图像的唯一性-全局而不是逐点属性。最后，我们可以给出HvG证明结构的形式定义：定义5.5MALL矩阵上的HvG证明结构是一个函数f：Max（VΓ）−→Max（EΓ）它为每个-分辨率（总估值）v分配一个连接（d，π），v. 此外，它必须满足以下图像唯一性条件：对于所有值vJ，如果（d，π）在vJ上，则f（vJ）=（d，π）=f（v）。命题5.6图像唯一性条件等价于以下更“局部”的条件：（Tog）对于所有出现W，如果QW <$/± d，则f（v）= f（v<$W）。证据假设图像唯一性。 如果 W/±d，则对于所有aL±d，out（aL）（W）=- 是的因此d在v<$W上，且f（v）=f（v<$W）。为了提高竞争力，请将其放在VJ上。 我们可以计算vJ=v<$W··<$W。假设对于某个Wi，我们有Wi±d。 那么对于Wi上面的某个字面出现L，我们将有一个L±d，并且out（aL）（Wi）=v（Wi）。这将与vJ上的d相矛盾，因为显然out（aL）/±vJ。所以我们必须有Wi/±d，i = 1，.，k.因此，通过k次应用（Tog），f（v）=f（vJ）。Q非示例续我们重新审视我们的反例，我们第一次尝试定义HvG。这转化为函数[W= 0]›→（（inl（inl（T）），T），{a1参与者5}）， [W= 1]›→（（inr（inr（T）），T），{a4参与者5}）哪里a1 =（inl（inl（T）），n），a4 =（inr（inr（T）），n），a5=（n，T）。请注意，此函数确实为每个赋值分配了一个链接，该链接位于该赋值上;然而，由于对[W= 0]的分配也位于[W= 1]上（因为out（a1）= 0），因此它不符合图像唯一性属性。52S. Abramsky/Electronic Notes in Theoretical Computer Science 172（2007）33ΓΓ5.2单调证明结构HvG定义是用完全加法和-分解来表达的，它们对应于我们域的最大元素。尽管如此，我们已经发现域结构在将出现定义为素数以及在形式化连接存在于-归结上的条件时是有用的。此外，HvG切换条件和相关概念隐含地涉及部分赋值（通过饱和连接集）[21]。现在我们将进一步和更重要地使用域结构，以制定更广泛的证明结构概念，我们随后将使用它作为我们的证明网概念的基础。单调证明结构就是简单的单调函数f：VΓ−→ EΓ。请注意，这样的函数将任意赋值（而不仅仅是总赋值）映射到任意预链接。这样的证明结构应该满足什么条件？一个明显的例子是，它对总估值的限制应该产生一个HvG证明结构： （PS1）单调函数f切到一个映射fm：Max（V）−→Max（E），这是HvG证明结构。其次，我们将推广每个分解的唯一连接条件，以涵盖部分赋值。HvG的定义在链接方面以“自上而下”的风格进行措辞在我们的环境中，最好是以一种更具建设性的方式在秩序中向上工作于是，用“与”的发生本身来表述条件就变得更加自然了事实上，我们已经在命题5.6中看到了这样一个重新表述的例子。第一个条件是形式上：（PS2）对于W∈W（Γ），且f（v）=（d，π）：QW ± d = ω out（d）（W）= v（W）.命题5.7条件（PS2）意味着p<$f±id，并且（d，π）在v上。证据 对于a，当W∈ W（Γ）出现时，如果out（d）（W）≠ 0，则QW<$±d，且因此由（PS2），out（d）（W）±v（W）。 因此pf±id。 类似地，如果L±d，则out（aL）±out（d）±v.Q举一个简单的例子，考虑公式αα。任何将[W= 0]映射到π或inr（T）的单调函数f都违反（PS2）;事实上，唯一允许的选择是inl（d）的形式。
我的内容管理
展开
