可定义性和完全抽象的关系

理论计算机科学电子笔记172（2007）301-310www.elsevier.com/locate/entcs可定义性和完全抽象皮埃尔-路易·居里PPS、CNRS和巴黎第七大学摘要游戏语义学更新了指称语义学。除其他外，它还提供了一个有吸引力的编程特性分类，并带来了一系列新的可定义性结果。与此同时，在证明理论的指称语义中，自90年代初以来已经出现了几个完全完备性结果。 在这篇笔记中，我们回顾了可定义性和完全抽象之间的关系，我们把一些旧的和最近的结果放在透视图中。保留字： 操作语义，指称语义，顺序性。1介绍在编程语言的语义学中，完全抽象的研究始于Robin Milner [44]和Gordon Plotkin[49]的两篇关于PCF的论文（另见[50]）。Milner证明了PCF的完全抽象（cpo）模型的唯一性（直到同构）Plotkin表明PCF的连续模型（当时唯一可用的模型）不是完全抽象的，但他表明，对于PCF的扩展“parallel or”（实际上，最初是“parallelif”，参见[ 18 ]更自然的parallel or变体），它变得完全抽象从那时起，有两种选择可供研究完全抽象：• 改变语言以适应预期的模型，• 改变模型以适应预期的语言。Plotkin的结果是第一种结果。随后是Berry和Curien [10]的结果，他们表明他们的顺序算法模型[9]（出于解决原始语言PCF的完全抽象问题的动机而开发）对于语言CDS- a（的内核CDS 01）是完全抽象的1电子邮件：curien@pps.jussieu.fr1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.02.011302P. - L. Curien/Electronic Notes in Theoretical Computer Science 172（2007）301基于Kahn和Plotkin的具体数据结构（最初称为“信息矩阵”）的函数语言后来，在[13]中（也见[12，19]），相同的模型被证明是完全抽象的，用于一种更在我的“THE ` E SEND ' E TAT“的结尾随着游戏语义学的出现，整个主题重新开始，并根据线性逻辑，它同时教会了我们分解A→B=！AB：这样一个分解的顺序算法（和相关的阅读的模型在游戏方面）被发现[37，20]。不久之后，现在被称为HO的两个团队（Martin Hyland和Luke Ong，应该加上Hanno Nickau的名字[45]，他们独立地制定了相同的模型）和AJM（Samson Abramsky，Radha Jagadeesan和PasqualeMalacaria）提出了PCF术语模型的语法独立描述（基于适当的B？ohmtrees，其中IhicIh havepo osedtocalllPCFB？ohmtrees[7]）。游戏和策略的两个模型，在精神上类似于顺序算法的模型（但具有不同的“操作），因为PCFBo？hmt r e s i n t eret i n p r e n ti v en和suri t i v en t ive n。到目前为止，满射性是最有趣的性质，它最好被理解为表征解释的形象的问题。因此，两支球队都表现出了重要的可定义性结果。这两个结果都是在相同的团队在（乘法线性逻辑）证明的语义领域中以完全完备性的名义获得了类似的满射性属性之后[3，31]。从那时起，出现了许多完全完备性或指称完备性（Girard [27]引入的术语）结果，用于各种模型中线性逻辑的各种片段的语义。但是让我们回到PCF和相关语言的语义。HO的特征，这被证明是更灵活的，是如下：everyinocenet和dwell-braketedstrategy是（unique）imageofaPCFBom树的解释。于是，人们自然会问，如果去掉这两个条件中的任何一个，会发生什么。事实证明，无辜的（不一定是好括号的）策略表征了PCF扩展中程序解释的图像，而好括号的（不一定是无辜的）策略表征了理想化Algol版本的解释图像[5]。（粗略地说，这个版本的理想Algol是“PCF +一阶引用”。此外，后者的结果产生了一个完全的抽象结果（几乎）没有商。在这篇短文中，我们重新描述了可定义性和完全抽象之间的关系，并考察了关于这两个相关概念的较早和较新结果的状况。从道德上讲，一旦可定义性成立，一个完全抽象的模型就可以通过一个商来构建，这个商在语义层面上模仿操作等价。当然，这样的完全抽象结果有点P. - L. Curien/Electronic Notes in Theoretical Computer Science 172（2007）301303具有足够的分离能力。这种情况发生在以下三种情况下：• 当模型是伸展的时（Plotkin• 对于顺序算法模型，关于CDS 01（Berry-Curien）和PCF+catch（Cartwright-Curien-Felleisen）;• 关于理想化大陵五（Abramsky-McCusker）（的一个变体）的好括号策略模型。我们将在续集中更详细地解释这一点。2从可定义的分离可定义性和完全抽象之间的差距由一个非常简单的充分条件决定，我们在下面给出。 这正是本文的目的所在 以强调这些性质不相同的基本事实。不知何故，各种各样的术语，如完全完备性或指称完备性（参见。[14]或[15]，或[16]，或[17]，或[18]，或[19]。我不需要输入PCF或其各种扩展的具体内容。这将足以修复一些类型（顺序）应用（即承认函数类型和函数应用）语言L，连同可观察类型和值的集合，以及可观察类型. 我们写M→M_v来表示M的求值终止的事实具有可观察值V。模型将类型和术语解释为类别的对象和态射。模型的A型元素d（即从1到[A]]的态射）是可定义的，如果存在A型闭项M使得[M]]=d。大多数模型都满足所谓的计算充分性，即对于所有可观测类型的闭项M，M→Mv当且仅当[M]] =v。 特别地，可观察值接收它们的这种表示法也意味着模型中可观察类型的每个元素都是可定义的。因此，在可观察类型，语法和语义之间存在完美的匹配。计算充分性通常通过可计算性/可实现性方法的变体来证明。完全抽象的属性允许我们为任意术语制定语法和语义之间的对应关系其表述依据的是上下文（操作）对等概念，即：M=opN惠（pC C[M]→pv惠C[N]→pv），其中C在上下文（有洞的项）上变化，使得C[M]（C中整体被M填充）和C[N]都是封闭的，并且是可观察类型的。则304P. - L. Curien/Electronic Notes in Theoretical Computer Science 172（2007）301模型被称为关于L的完全抽象，如果对于所有M，N（相同类型）：[[M]]=[[N]]惠M = opN。从左到右的方向被称为充分性（或另一个方向是硬的，并将其与“compl`et e a d'equation“（用于完全抽象的法语术语）的compl`ete联系起来为什么这是等价的困难的一面，一个很好的解释来自交集类型理论[15]和“逻辑形式的域”理论[ 2 ]，它改写了对应的证据是“证据”的一面然后，在这些眼镜下，丰满/完整性朝着正确的方向发展：如果|= M = N（即，如果M=opN），则M=N（即，[M]] = [[N]]）。现在，我们可以陈述这份说明所围绕的标准为了简单起见，我们假设只有一个可观察的基本类型o，但当然，在存在多个可观察类型的情况下也是如此（例如，PCF有两个可观察类型：nat和bool）。准则2.1如果模型是这样的，对于同一类型A的每个不同的（可定义的）f，g，存在A→o类型的可定义h，使得hf/= hg，那么它是完全抽象的。证 据 如 果 [M]] = [[N]] ， 则 h 由 我 们 的 假 设 给 出 ， 且 P 使 得 [[P]] =h ， v1=h（ [[M]] ） ， v2=h （ [[N]] ） ， 且 C=P[ ] 。 则 C[M] →αv1 和 C[M] →αv2 ， 因 此Mi=opN。Q我建议把这种充分抽象的充分属性称为可定义的可分离属性。据我所知，基于可定义可分性的完全抽象的第一个证明是：• (in一个无类型的设置）一个与无类型lambda演算的模型D∞和头部范式的概念相关的设置[30，53]（见[21]的简洁和• 在目前的类型化设置中，证明了PCF+catch的顺序算法模型的完全抽象[13]。准则2.2在类型层次是简单类型层次并且模型在代数完全偏序上丰富的假设下，可定义可分性（因此是完全抽象）的一个充分条件是模型的以下两个性质的结合(i) 紧致可定义性：所有类型的所有紧致元素都是可定义的，(ii) 外延性：函数类型的模型元素是函数（在范畴理论术语中，模型有足够的点）。证据 我们可以把任意类型A写成A1→.. →An→o。 设fG. 通过EXTENSIONALGEBAICITY，THEREXISTCOMPACTDI， . . . ，dnsuc hth atfd1. . .dn=/P. - L. Curien/Electronic Notes in Theoretical Computer Science 172（2007）301305gd1. dn. 设Pi满足di=[[Pi]]（1≤i≤n）. 设h =[[λx.xP1. Pn]]。然后hf/=hg。Q当然，可以直接证明（即）。 没有经过可定义的分离性），一个具有可定义性属性的可拓模型是完全抽象的（在上面的证明中，不是定义h，而是直接定义上下文[ ] P1...... Pn）。这就是Plotkin如何证明连续模型对于PCF+por是完全抽象的。符合第一个标准而不是第二个标准的模型的例子是，再次，D∞（不满足紧可定义性）和序列算法模型，Rithms（不是扩展的）。让我们在这里做一个简短的题外话。在[49]中，还提出了PCF的进一步扩展，使得模型的所有类型的每个可计算回到紧致可定义性，米尔纳证明了与上述第二个标准相反的一个条件：PCF的完全抽象cpo模型必须是（因此以存在的性质为特征）序延拓的，并享有紧致可定义性。（当函数类型的元素不仅是函数，而且它们的排序是逐点排序时，模型被称为序扩展的。对完全抽象模型的长期探索就是从那里开始的。首先，Berry定义了稳定模型[8]，它是外延的，但不是有序外延的。然后Berry和我自己构建了序列算法的模型，它不是可拓的（尽管它可以通过扩大一个误差元素的可观测值集来扩展更重要的是，在这些模型中，PCF的紧凑定义失败了：• 一个著名的反例证明了紧致稳定函数的失败是所有可定义的是古斯塔夫，或Berry-Kleene函数（见，例如。[7]）。• [18]中序列算法模型的紧凑可定义性的反例在AJM博弈模型的起源游戏语义学的著作从根本上背离了这条路线，更果断地放弃了外延性。PCF的HO和AJM博弈语义（限于PCF的类型层次结构）相当于PCF的无语法描述。该游戏模式使用了一种用于compac tdefine的bilityprop rty（因为将bilitectionbettweenstrategiesanddPCFB ？ohmtre s reestri ct sts 转 换 为 bilitectionbet tween finite（=compact）strategiesanddfini t ePCFB？ohmtres，并且因为后者本质上是某种规范形式的PCF项）。然而，HO和AJM模型不能是外延的，它们也不能满足可定义的可分性。但是，有一种“抽象无意义”的机制，迫使可定义的可分离性属性。一个等价于任何不能被h分开的A类型的f和g（对于所有解释语法类型的A），即我们设置f=opg，只要hf=hg对于所有A→o类型的h。唯一微妙的一点是验证商仍然是一个模型（特别是可以解释PCF的定点构造）。306P. - L. Curien/Electronic Notes in Theoretical Computer Science 172（2007）301我们在这里强调，这种抽象的构造并没有利用博弈模型的任何特征，事实上也可 以 应 用 于 PCFBéohm 模 型 （ 其 中 HichisomorphicictoheHOandAJMmodelsonthefine itetype hierarchy），产生了Milner最初构造的PCF完全抽象模型的一个版本（这也是一个语法商，以稍微不同的换句话说，尽管它们的标题，每一个开创性的HO和AJM论文的关键贡献是一个可定义的结果。从某种意义上说，这是人们所能期望的最好结果，因为Loader [39]表明PCF的运算等价性是无效的（并且对于有限值PCF是不可判定的，PCF的版本中唯一的基本类型是有限类型的布尔值）。这个否定的结果在某种程度上结束了对PCF的完全抽象模型的“直接”构造的探索莱尔德因此，他的模型需要验证，事实上Laird已经展示了如何获得序列算法的模型作为他的模型的商[36]。一旦清白被去除，那么（一种变体）可定义的可分性就成立了。需要一个变体，因为候选h通常也不是好括号的，但是当f和g至少在它们的一个好括号的策略中不同时，则可以找到好括号的h。在理想化的Algol的好括号模型中，它认为M=opN当且仅当[M]]和[[N]具有相同的好括号的（完全的，在[5]的术语中）策略。下表总结了本节讨论的可定义性和完整抽象结果语言模型可定义性全抽象PCF +porCont是的是的PCF +catchSA（Ginn/=op）是的是的PCFPCFBT/=操作是的是的PCFGAJM、 GHO、PCFBT是的没有PCF +对照G驿站是的没有理想大陵五G是的是的P. - L. Curien/Electronic Notes in Theoretical Computer Science 172（2007）301307其中Cont、SA、PCFBT、GAJM、GHO、Ginn和G分别代表连续模型、等式算法模型、PCFBüohm模型、AJM模型、HO模型、无辜策略模型和良好括号策略模型。（回想一下，当限制到有限类型层次时，三个模型PCFBT，GAJM，GHO3关于可观察在最后一节结束的表格中，所有考虑的语言都具有相同的observable概念。我们还可以（不完全）将另外两个完全抽象结果添加到列表中：• Longley• Paolini已经证明，对于具有两个算子的PCF的扩展，稳定模型是完全抽象的，其中一个是Gustave类算子[48]。更一般地说，当改变语言时，也可以考虑改变可观察的类型和值。我们这里只提到一个例子，它与PCF非常接近，但其性质却截然不同。一元PCF是PCF的变体，其中唯一的基本类型只有一个（非底部）元素，并且其中PCF的条件构造Loader已经证明了这种语言的操作等价性是可判定的[38]，这与PCF的情况（甚至是无限的）非常相似。事实上，Laird4总结发言PCF的完全抽象问题已经引发了大量的工作，并以其“副作用”而闻名• 稳定模型（由Girard重新发明）产生了线性逻辑[26]，其在我们社区的巨大影响应该在其他地方重新叙述。• 顺序算法的模型使我认真地把范畴闭范畴作为一种语法，并从那里到范畴抽象机[16]，然后到显式替换[1]。• 完全抽象问题也推动了逻辑关系的研究[51，52，46]，并激发了序列性的扩展解释（参见：第3条）。• 游戏语义学被证明是非常灵活的。除了控制和一阶引用（上面讨论过）之外，游戏还给出了各种编程特性的语义描述，包括子类型[14]，非确定性[28]，概率选择[22]，高阶引用[6]，按值调用[29]或并发性[25]。308P. - L. Curien/Electronic Notes in Theoretical Computer Science 172（2007）301• Malacaria和Hankin将游戏语义应用于程序分析[41，42，43]。类似地，游戏语义在程序等价和不等价的有效证明中的应用，以及更一般地在抽象解释和模型检查中的应用，正在以算法游戏语义的名义开发[24，47，23]。最后，让我们提到，完全抽象在进程演算理论中也具有普遍的重要性。在那里，操作等价的概念在许多变体下是双模拟的，模型的概念由目标演算给出：因此，人们研究一种语言到另一种语言的完全抽象翻译，在某种意义上忠实于完全抽象的原始定义。引用[1] 我 很 好 M ， L.Card elli ， P.- L.Currien ， anddJ.- J.L'evy ， Expli tt ub st ut i ons ，JournalofFunctionalProgramming 1（4）（1992），375-416.[2] Abramsky，S.，Domain theory in logical form，Annals of Pure and Applied Logic51（1991），1-77.[3] Abramsky，S.，和R. Jagadeesan，乘法线性逻辑的游戏和完全完备性，符号逻辑杂志，59（2）（1994），543-574（会议版，Proc. FOSSACS'92）。[4] Abramsky，S.，R. Jagadeesan和P. Malacaria，Games and full abstraction for PCF，Information andComputation163（2）（2000），409-470（preliminary conference version in Proc. Theoretical Aspectsof Computer Science 1994，Springer LNCS 789，1-16）.[5] Abramsky，S.，和G. McCusker，Linearity，sharing and state：a fully abstract game semantics forIdealized Algol with active expressions ， in O'Hearn and Tennent （ eds. ） ， Algol-like languages ，Birkhauser（1997）.[6] Abramsky，S.，K. Honda和G. McCusker，A fully abstract game semantics for general reference，inProc. Thirteenth Annual IEEE Symposium on Logic in Computer Science ， IEEE Computer SocietyPress，334-344（1998）。[7] 阿马迪奥河P. - L. Curien，“Domains and Lambda-Calculi”，Cambridge University Press（1998）.[8]Berry，G.，典型肾结石的稳定模型，Proc. ICALP，Springer Lect. Comp. Sci. 62（1978年）。[9] Berry ， G. ， P. -L. Curien ， Sequential Algorithms on Concrete Data Structures ， TheoreticalComputer Science20（1982），265-321.[10] Berry，G.，P. - L. Curien，The kernel of the applicative language CDS：theory and practice，Proc.French-US Seminar on the Applications of Algebra to Language Definition and Compilation ，Cambridge University Press（1985），35-87.[11]Bucciarelli ， A. ， 和 T. Ehrhard ， Sequentiality in an extensional framework ， Information andComputation110（2）（1994），265-296.[12] 卡特赖特河，和M.张文，可观测序列性与完全抽象，《计算机程序设计原理》，1992年。[13] 卡 特 赖 特 河 、 P. - L. Curien 和 M. Felleisen ， Fully abstract semantics for observably sequentiallanguages，Information and Computation111（2）（1994），297-401.[14] 赫罗博切克，游戏语义和子类型，在Proc.第15届IEEE计算机科学逻辑研讨会（LICS[15] Coppo ， M. ， 和 M. Dezani ， A new type assignment for a new terms ， Archiv. Math. Logik19（1978），139-156.[16] 阿 基 诺 湾 、 P. - L. Curien 和 M. Mauny ， The categorical abstract machine ， Science of ComputerProgramming8（1987），173-202.P. - L. Curien/Electronic Notes in Theoretical Computer Science 172（2007）301309[17] Cur ien，P. -L。，“C om b i n ateur s ca t 'ego r i que s，a l go r i t h m es s s' equent i e l s et t p r am at i o n fonct i onne l l e“，T h ` e se d ' E tat，U ni v. 第7页（1983）。[18] Curien，P.L.，“Categorical Combinators，Sequential Algorithms and Functional Programming”，Pitman（1986），rev i s ed it i on，B ir k hüau s er r（1993）.[19] P. - L.陈文龙，“数据结构中的可观测序列算法”，第七届计算机科学逻辑研讨会论文集（LICS[20] Curien，P. L.，关于顺序性的对称性，Proc. Mathematical Foundations of Programming Semantics'93，Springer Lect. Notes in Comp. Sci. 802，29-71（1994）。[21] Currien，P. -L。，Sur l'n- e x pansio n in fini e，C o m pte s - R endu s d e l ' A ca d'e mie de s science s33 4 Sec. I（2002），77-82.[22] 达诺斯河谷，和R.Harmer，概率博弈语义学，ACM计算逻辑学报3（3）（2002）。[23] Dimovski，A.，D. R. Ghica和R.懒惰。Data-abstraction refinement：a game semantic approach，inProceedings of the 12th International Static Analysis Symposium（SAS[24] Ghica ， D.R. ， Guy McCusker ， The regular-language semantics of second-order idealized ALGOL ，Theoretical Computer Science309（1-3）（2003），469-502.[25] Ghica，D.R.，和A.Murawski，Angelic Semantics of Fine-Grained Concurrency，Proc.软件科学和计算结构的基础[26] Girard，J.-是的，Linear logic，Theoretical Computer Science50，1-102（1987）.[27] Girard，J.-是的， 关于指称完备性，Theoretical Computer Science227（1999），249-273.[28] 哈默河，和G. McCusker，A fully abstract game semantics for finite nondeterminism，in Proc. of the14th annual IEEE symposium on Logic in Computer Science（LICS[29] 本田，K.，和N.Yoshida，按值调用计算的博弈论分析，理论计算机科学221（1-2）（1999），393-456。[30] Hyland ， J.M.E. ， A syntax characterization of the equality in some models of lambda calculus ， J.London Math. Soc.2（1976），361-370.[31] Hyland，J.M.E.，和C. H. L.无混合规则乘法线性逻辑的公平博弈与完全完备性。预印本（1993年）。[32] Hyland，J.M.E.，和L. Ong，关于PCF I，II和III的完全抽象，信息和计算163（1）（2000），285-408（自1994年以来分发的初步草案）。[33] Kahn，G.，和G. Plotkin，Concrete domains，Theoretical Computer Science121（1993），187-277（1978年以TR IRIA-Laboria 336的法文[34] Laird， J.， Full abstraction for functional languages with control，Proc.12th Annual Symposium onLogic in Computer Science（LICS[35] Laird，J.，一元FPC的完全抽象双主模型类型化λ演算及其应用国际会议论文集（TLCA[36] Laird，J.，游戏和顺序算法。 地出现。[37] Lamarche，F.，Sequentiality，games and linear logic（1992）.[38] 莱德尔河，Unary PCF is decidable，Theoretical Computer Science206（1-2）（1998），317-329.[39] 莱德尔河，Finitary PCF is undecidable，Theoretical Computer Science266（1-2）（2001），341-364.[40] Longley，J.，序贯可实现泛函，纯逻辑与应用逻辑年鉴117（1-3）（2002），1-93。[41] Malacaria，P.，和C.陈文，一种新的控制流分析方法，载于《建筑工程学报》1998年，计算机科学讲义1383（1998）。310P. - L. Curien/Electronic Notes in Theoretical Computer Science 172（2007）301[42] Malacaria，P.，和C. Hankin，Generalised Auxiliary Charts and Games，in Proc. ICALP[43] Malacaria ， P. ， 和 C. Hankin ， Non-deterministic games and program analysis ： an application tosecurity，in Proc. of the 14th annual IEEE symposium on Logic in Computer Science（LICS[44] 米尔纳河，完全抽象模型的类型化演算，理论计算机科学4（1977），1-23。[45] Nickau，H.，遗传序贯泛函，Proc。计算机科学的逻辑基础：圣彼得堡的逻辑。A.尼罗德和尤。V.Matiyasevich，Lecture Notes in Computer Science 813，253-264（1994）.[46] O'Hearn，P.，和J. Riecke，Kripke逻辑关系和PCF，信息和计算120（1）（1995），107-116。[47] Ong，C. H. L.，三阶理想大陵五的观测等价性是可判定的，在Proceedings of IEEE Symposium on Logic inComputer Science 2002，Copenhagen Denmark，pages 245-256，Computer Society Press（2002）中。[48] 帕奥利尼，L.，“Lambda-theries：somemeivestigations“，PhDthesis，Universit`adiGenovaanddUniversit′eddelaM′editeran′ee（2003年）。[49] Plotkin，G.，LCF作为一种编程语言，理论计算机科学5（1977），223-257。[50] 斯科特，D.，类型理论替代ISWIM、CUCH、OWHY、理论计算机科学121，411-440（1993）（手稿自1969年以来分发）。[51] Sieber，K.，通过逻辑关系推理顺序函数，Proc。计算机科学中的范畴应用，剑桥大学出版社（1992）。[52] Stoughton，A.，机械化逻辑关系，Proc. Mathematical Foundations of Programming Semantics，Springer Lect。对比中的注释Sci. 802（1994）。[53] Wadsworth，C.，The relationship between computational and denotational properties for Scott