命令式语言局部变量的指称语义模型：可能世界和对象空间中的范畴论研究

理论计算机科学电子笔记265（2010）389-402www.elsevier.com/locate/entcs局部变量建模：可能的世界和对象空间Guy McCusker1，2 约翰·鲍尔3巴斯大学计算机科学系英国巴斯BA2 7AY摘要命令式语言中的局部变量至少以两种根本不同的方式被赋予指称语义。 一种是通过使用函子范畴，关注可能世界的概念。 另可以被称为基于事件的，以Reddy的基于游戏语义的对象空间和模型为例。O'Hearn和Reddy通过给出世界是对象空间的函子范畴模型，将这两种方法联系起来，然后证明他们的模型对于二阶以下的理想Algol程序是完全抽象的。但是对象空间的范畴并不小，因此为了构造一个局部小的函子范畴，从而笛卡尔闭的，他们需要处理对象空间的有限集合。这削弱了对象空间模型和函子范畴模型之间的联系：米田嵌入不再提供对象空间的原始范畴到函子范畴的完全嵌入。此外，对象空间的受限集合的选择是特别的。在本文中，我们通过证明有限对象形成简化对象空间模型的一个小的稠密子范畴来改进这种方法。因此，这些有限对象上的函子范畴是局部小的和笛卡尔闭的，并且包含对象空间范畴作为一个全子范畴。所有这些工作都必须在CPO中得到丰富。我们通过证明完全抽象在三阶失败来进一步完善他们的完全抽象结果关键词：指称语义，编程语言，命令式编程，类算法语言，局部状态，可能世界，范畴论。1介绍近几十年来，命令式语言中的局部变量至少有两种主要的方式被赋予指称语义。一种方法，特别是由奥赫恩和特南特，在很大程度上建立在工作，Oles等其他人的研究都是基于函子范畴的：人们构造了一个小的世界范畴W，并在函子范畴SetW或CpoW中对语言进行建模，以包括递归。世界的各种小类别W1本文件是由英国创新、大学和技能部（DIUS）资助的PMI2项目的成果，旨在为日本高等教育部门和英国高等教育部门提供帮助。所表达的观点不一定是DIUS或英国文化协会的观点2电子邮件：G.A. bath.ac.uk3电子邮件：A. J. bath.ac.uk1571-0661 © 2010 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2010.08.023390G. McCusker，J.Power/Electronic Notes in Theoretical Computer Science 265（2010）389已经逐渐变得越来越复杂，以模拟日益复杂的本地变量的功能，如文章[13]的集合中所概述的。我们在这里想到的另一种方法是与Reddy最相关的方法[14]。他开发了对象空间来模拟干扰控制的Algol，使用跟踪记录有状态对象的行为。 Reddy的模型命令式程序的游戏语义的重要先驱[1，2]，它提供了理想化Algol的第一个完全抽象的模型。这些模型不是由函子范畴给出的，而是直接根据自然但复杂的结构上的设置这就留下了两种方法是否可以统一的问题。 O’Hearn and Reddy made a start onthat question in [ 虽然这是一个实质性的进步，这仍然留下了一个实质性的步骤，实际上从范畴论的角度来看，一个根本性的步骤，没有解决。具体地说，这个问题是规模问题：Reddy的范畴在局部很小，但并不小。 如果像奥赫恩和雷迪那样，特别限制到一个小的子范畴，一个失去基本的范畴理论结构，如完整性和余完整性的性质。 但是如果一个人从一个不小的范畴W开始，那么函子范畴SetW通常 不 会 是 局 部 小 的 ， 这 又 会 导 致 重 大 的 破 坏 ， 例 如 不 允 许 一 个来 得 出Carbohydrate封闭性的结论。我们在本文中解决了这个难题。 具体来说，我们通过研究来解决这个问题，稠密性：范畴C的一个小的满子范畴D是稠密的，如果一个典范函子将C完全嵌入函子范畴集合D中，它必然是局部小的。密度是范畴论中的一个基本概念[7]，它的使用给我们带来了一个非常令人满意的情况：我们有一个理想化的Algol的函子范畴模型，一个没有不自然大小限制的干扰控制的Algol的对象空间模型，以及它们之间的完全嵌入。 这里有一个复杂的问题：我们不仅需要密度，而且需要密度的丰富版本，在Cpo类中富集。在第5节中，我们提供了一个反例来证明普通密度是不充分的，然后证明我们有我们所寻求的Cpo富集密度。密度的丰富概念是丰富范畴论的标准部分[6]。我们的工作并不是对奥赫恩和雷迪的工作的直接改进由此产生的世界范畴的优点是比雷迪的范畴更容易描述：它是有限集合上的自由量子范畴。然而，它产生了与Reddy的范畴相同的干涉控制Algol作为额外的贡献，我们改进了O'Hearn和Reddy的完全抽象结果。在他们的论文中，证明了函子范畴模型在二阶以下是完全抽象的，也就是说，对于二阶及以下的项，等式G. McCusker，J.Power/Electronic Notes in Theoretical Computer Science 265（2010）389391→→×在适当的操作语义中，该模型与上下文等价一致。他们关于完全抽象的论点几乎直接适用于我们的模型。我们给出了一个反例，充分抽象的顺序三，表明这一结果是尽可能的。2两种类Algol语言本节简要介绍了理想化的Algol的一个版本的语法，以及它的干扰控制变体。我们省略了操作语义学的细节，这些细节可以在文献中找到; O 'Hearn和Tennent编辑的文章集这是非常有用的[13]。这些语言是建立在三个基本类型之上的：命令的类型;自然数值表达式的类型;和可赋值变量的类型。理想化的Algol本身是在这些基本类型上应用的简单类型的Algol演算。因此，它的类型是通过乘积和函数操作从基类型生成的，它的语法是基于使用递归进行命令式编程的常量库，如下所示。• 0：nat• succ：nat → nat• pred：nat → nat• ifzeroB： nat×B×B→B• YA：（A→A）→A• skip：跳• assign： var× nat→var• deref：var → nat• seqB：×B→B• while： nat×→• new：（ var→ var）→ var• mkvar：（nat→ var）×nat→var其中，B的范围是基本类型，A的范围是所有类型。左列中的常量提供算术和递归，就像PCF中的例子一样。其余的提供了一种命令式程序语言：skip是不做任何事情的命令; assign（V，N）将表达式N的值存储在变量V中; deref（V）返回存储在V中的值; seq（C，M）执行命令C，然后计算M-注意，B是null的变体是命令的常见顺序组合，而其他的则允许nat或var类型的表达式在存储器上有副作用;而（M，C）重复执行C，直到M变为非零;ifzeroB提供条件分支; new（λx：var.C）在标识符x已绑定到新的存储单元的环境中执行命令C。最后，mkvar是一个“变量构造器”，它用nat类型的“写方法”和nat类型的“读方法”构建var类型的表达式。这种面向对象的变量观点是由雷诺兹在他的论文《大陵五的本质》中提出的，现在已经成为标准。事实上，包括O'Hearn和Reddy在内的一些演讲甚至将var与产品类型（nat）nat相识别。已经证明，mkvar的存在与该语言中程序等价的概念没有区别[9]。干扰控制的大陵五由一个带prod的Arkne演算组成，392G. McCusker，J.Power/Electronic Notes in Theoretical Computer Science 265（2010）389⇓⇓⇓−--→P在相同的基本类型上，使用相同的常量，除了Y被排除在外。a-函数演算限制了函数的应用，使得函数和参数不能共享任何标识符。这导致了一种情况，在这种情况下，不同的标识符永远不会被绑定到干扰程序短语，这使得程序分析更加直接，这也是Reynolds在SCI类型系统后来由O'Hearn等人[ 11 ]进行了改进，但我们在这里关注的请注意，在这个系统中，产品的两个组件仍然可以共享标识符，从而相互干扰，因此，诸如while之类的常量的类型意味着执行循环体可能会对将来执行保护程序产生影响。如果要保留任何有趣的命令式程序，这当然是必要的这两种语言可以配备一个操作语义，以存储的形式给出：从位置到自然数的函数。操作语义由判断s，M sJ，N组成，声明存储s中的项M评估为项N，将存储更改为sJ。项M和MJ是上下文等价的，如果对于每个上下文C[ ]，使得C[M]和C[MJ]是类型C的闭项，C[M]跳过当且仅当C[MJ]跳过;在这些判断中没有存储，因为闭项在空存储中操作3对象空间（简化）Reddy的因此，它是命令式程序的游戏语义的重要先驱[1，2]，这是理想化的Algol的第一个完全抽象的模型。也许更令人惊讶的是，Reddy在这一节中，我们提出一个简化的雷迪范畴，它以允许非决定论进入模型为代价，消除了相干关系。非决定论是理想化大陵五的保守扩展，在它的规则和干扰控制下，所以这与我们完全抽象的结果没有区别，同时大大简化了技术细节。设A、B、C为集合。 我们用PA表示A的幂集，A表示从A引出的有限序列的集合。 设f：A→ PB和g：B→ PC是任意函数.定义复合gf：A→ PC如下。 对于任何a∈A，（g<$f）（a）是集合{s1· · ·sn|1、 . . . ，bn. b1. . . bn∈f（a）i∈{1， . ，n}si∈g（bi）}其中s1···s n是序列s1，.， s n.这种复合的概念是结合的，而映射A一个发送每个a到[a]，包含单例序列的单例集，都是它的恒等式，因此我们有一个范畴FQ，之所以这样命名是因为它原来是集合上的自由量子范畴或者，我们可以将这个范畴表示为Kleisli范畴集PT，其中G. McCusker，J.Power/Electronic Notes in Theoretical Computer Science 265（2010）389393PP→×-PT是在集合上传递自由幺半群的单子。 复合函子 不由于分配律的作用，λ：TP −→ PT其动作如下。对于任意集合A，λ A取一个序列[S1，...，S n]到序列集{a1. a n|i∈ 1，.， n.ai ∈ S i. }第一作者已经证明，这一范畴的对立面产生了一个干扰控制的大陵五模型，它本质上与雷迪的对象空间模型相同这种表述也与[5]中lambda演算的恩格尔风格模型的发展以及[3]中提出的关系模型有很多共同之处;联系仍有待探索。事实上，当建模干扰控制大陵五，它原来是更方便的工作（相反）克莱斯利类别的T-代数，类别的代数单子T，即类别的monoids。这允许访问一些额外的对象，这使得模型的公式化更简单。然而，对于所有意图和目的，FQop是容纳前引文献中的干扰控制的Algol的完全抽象模型的类别。因此，我们将使用这个类别。3.1干扰控制的Algol现在我们回顾一下FQop中语言的类型和常量的语义。范畴的对象是集合，而映射AB可以看作是A和B之间的关系。集合的不交并给出了这个范畴中的积（因为它给出了集合中的余积，因此也给出了集合 PT中的余积）。大范畴（TAlg） op具有monoidal闭结构，其中张量积由Carnival积给出集合的内部homAB由集合A<$B给出。 在FQop中，monoidal结构不可用，但函数类型可用，这就足够了 让我们能够模拟语言。类型的解释如下所示，其中N表示自然数的集合：[[nat]]=N[[]]={}[[var]]={write（n），read（n）|n ∈ N}[[A×B]]=[[A]]+[[B]][[A → B]]=[[A]] × [[B]]。(In在后面的一些计算中，我们将用它们在这个模型中表示的集合来识别基本类型nat，nat和var现在我们把注意力转向常数。 对于每个常数c：A，我们定义 [C]作为[A]的元素。我们使用并置来表示序列的连接，并用它的单个元素来标识单例序列。当处理集合的不相交并集时，如在产品类型的语义中，我们使用上标来394G. McCusker，J.Power/Electronic Notes in Theoretical Computer Science 265（2010）389−−−∈∗∗ ∗∗表示给定元素属于不相交并集的哪个分量，例如在N + N + N中，n3是最右边分量中的值n。注意，序列svarn由元素write（n）和read（m）组成。如果每个read（）条目中的值都匹配，则我们称这样的序列为单元格跟踪最近的write（）条目：与存储单元相关联的行为类型。 如果没有写（）尚未发生，我们允许read（0）发生，建模默认初始值为零的单元格。 因此，通过以下方式生成细胞迹线：正则表达式read（0）<$·（<$n∈Nwrite（n）·（read（n）<$）<$。在此基础上，我们给出常量的语义如下。• [[0]]=零• [[succ]]={（n，n +1）|n ∈ N}• [[pred]]={（n +1，n）|n ∈ N}• [[ifzeroB]]={（01v2，v）|v ∈ B}<${（n1v3，v）|n ∈ N，n/= 0，v ∈ B}• [[skip]]=• [[assign]]={（n2write（n）1，n）|n ∈ N}• [[deref]]={（read（n），n）|n ∈ N}• [[se qB]]={（1v2，v）|v∈B}• [[while]]={01 <$2 01 <$2. 01 2 m1，）|m ∈ N，m/= 0}• [[new]]={（（s，），）|s是一个小区跟踪}。• [[mkvar]]={（n2，rea d（n））|n∈N} <${（n . . . n，n）1，write（n））|n∈N}在while的语义中，表达式0 1 2 0 1 2. 0 1 2表示正则语言（0 1 2）中的任何元素，包括空序列;类似地，n. mkvar语义中的n表示形式为nnnnn的任何序列。. . n.4O’Hearn在[12]中，O'Hearn和Reddy提出了一个完全理想化的Algol模型，该模型是通过（丰富的）Yoneda嵌入从Reddy的对象空间模型获得的。方法如下。要模拟理想大陵五，需要：• 一个笛卡尔闭范畴，来模拟类型化的代数演算• 一组对象来解释语言的基本类型，以及它们之间的映射来解释构成理想化Algol核心的• 一个解释递归的固定点组合子：对于每个类型A，一个映射[[A]][[A]]→[[A]具有适当的属性• [][[][[]][]][][[]][][]][][对象空间模型给了我们足够的解释基类型和简单常量，但不是笛卡尔封闭的：虽然它有乘积，但它没有指数;G. McCusker，J.Power/Electronic Notes in Theoretical Computer Science 265（2010）389395−关于我们- ×−→⇒在没有指数的情况下，问固定点和new是否可以解释是没有意义的。O'Hearn和Reddy提出的解决方案涉及使用Yoneda嵌入将对象空间的范畴嵌入到笛卡尔闭范畴中。 这个想法对象空间模型上的一个适当的预层范畴是Cartesian闭的，并且包含作为一个完全子范畴的对象空间。这立即满足了模型的前两个要求。不动点是通过处理Cpo丰富的范畴来获得的，事实证明，直接考虑var→var的解释允许构造new的语义。现在先把递归放在一边，让我们来说明函数类别SetFQ中new的语义。FQop通过米田嵌入完全嵌入到这个范畴中，对象A由协变的hom-functorFQ（A，）表示。产品是逐点给出的。除了我们稍后将讨论的大小问题外将有指数：给定函子F和G：FQ→Set，指数[F<$Q]是将对象X带到自然变换集的函子FQ（X，−）×F−→G。特别地，[[var]][[var]（X）是自然变换FQ（X，−）× FQ（[[var]]，−）−→ FQ（[[var]]，−）。由于FQ具有由集合的不相交并给出的余积，并且再次使用Yoneda引理，这与hom-set相同FQop（X+[[var]]，[[var]]）.因此，我们对new的解释必须给出，对于每个X，以一种自然的方式，从这个hom-set的元素出发的映射，即，（X+{read（n），write（n）}）|n∈N}）n和{n}到[X]的元素[X]=FQop（X，），即X与单例集之间的关系。我们定义[新]如下：[[new]][X]（f）={（s T X，n）|（s，n）∈ f，s T [[var] is a cell-trace}.注意与对象空间模型中new的解释的相似性，以及不同之处：在这个模型中，序列s不仅包含用于读取和写入的变量事件，而且还包含来自集合X的事件，以交错的方式。正是这一点使得大陵五的解释工作：来自X的事件中断了变量中事件的连续性，并允许我们记录干扰行为。然而，有一个重要的尺寸问题需要克服。当声称指数存在时，我们断言[F G]（X）由自然变换集FQ（X，）FG. 因为FQ不是一个小范畴，所以没有理由相信这个自然变换的集合是一个集合。在缺乏详细论证的情况下，我们不能声称集合FQ是笛卡尔闭的，所以我们不能用它来模拟理想化的大陵五。奥赫恩和雷迪意识到了尺寸问题：他们的论文明确指出，他们使用的函子-范畴构造只适用于小范畴。但396G. McCusker，J.Power/Electronic Notes in Theoretical Computer Science 265（2010）389−F∈⊆→→∈--◦ ⊆ ⊆◦F对象空间的范畴并不小，正如所写的那样，他们的工作直接将构造应用于这个范畴，因此他们的模型的笛卡尔闭包的本质属性还没有建立。对象空间的范畴是局部小的（hom-sets真的是集合），所以我们可以通过将注意力限制在某个对象集合上的完整子范畴来直接纠正这种情况。但是我们应该选择哪一套呢？在这一点上，一个紧张局势之间的愿望，使建设工作和愿望，有一个数学上自然和吸引人的模型。 可以提供一个快速修复 通过限制（例如）仅用于解释基本类型及其产品的那些对象，但人们立即失去了语法及其模型之间的区别：好的模型应该完全独立于语法考虑来构建。一个更令人满意的解决途径在于识别一个小的稠密子范畴并考虑函子范畴集C.这就是我们在本文其余部分所5一个小的稠密子范畴设C是一个范畴，它有一个小的满子范畴D，包含函子J：D<$C。回 想 一下，如果函子C设置D操作 把X带到C（J，X）是完全的和忠实的。等价地，C的每个对象都以规范的方式作为D对象的余限出现;参见Mac Lane [7]。我们的目标是找到有限乘积下闭的FQop的在此之上的预层范畴将是笛卡尔闭的，而FQop将以乘积保持的方式完全嵌入到这个范畴中。然后，我们将能够沿着上面指出的路线为理想化的Algol提供语义作为第一次尝试，考虑其对象是有限集的FQop我们称之为FQ操作。它可以等价地作为子范畴给出，对象是自然数，即形式为0，1，.的有限集合，n对于一些nN，这显然是一个小类别。 FQop的每个对象都是一个余限of a graph图表of theseobjects对象. 给定集合A和B，B、关系取元素aA到单例序列[a]提供了从A到B、背面：在A，B中：A → B ={（[a]，a）|a ∈ A}outB，A：B→A={（[a]，a）|a∈ A}请注意，B，A在A中，B=idA，如果ABC然后在A，C=在B，C在A，B中，并且对于外部地图也是如此。现在给定任何FQop的对象X，由X的所有有限子集和它们之间的所有A，B映射组成的图具有共极限X，A，X中的映射形成共极限锥。因此，人们可能期望有限集在FQop中是稠密的，但不幸的是，情况并非如此，如下面的反例所示。考虑实数的集合R。如果FQop在FQop中是密集的，则存在应该是FQop中的映射R→1和自然映射R → 1之间的双射对应G. McCusker，J.Power/Electronic Notes in Theoretical Computer Science 265（2010）389397F◦→→×→ ◦⊆→⊆⊆ ◦◦FF→∅◦⊆∅1Fn1n我 我变换FQop（J−，R）→FQop（J−，1）其中1是singleton set。给定这样一个自然变换α和集合XYR，自然性意味着α（inY，R）inX，Y=α（inY，R在X，Y中）=α（在X，R中）。因此，映射α（在X，R中）：X1形成在X，Y中的上的余锥，因此存在唯一的映射f：R1，使得f在X中，R=α（在X，R中），对每个有限元素XR。 FQ op的密度等于对所有映射g：XR，而不仅仅是对in映射，α（g）= fg的陈述。我们现在定义一个自然变换α，对于它这不成立。 给定有限集合X和映射f：XR在FQop中，α（f）是X上的关系式，1定义通过{（s，s）}|（s，x）∈f对于不可数多个x}。为了证明这是自然的，考虑任意的f：X→R和g：Y→X。若有（t，n）∈α（f）<$g，则必有（s，n）∈α（f）使得s=x1. x n，t=t1. t n且对每个i，（t i，s i）∈g.这意味着有不可数多个x使得（s，x）∈f，因此对于不可数多个x也有（t，x）∈ f <$g，使得（t，x）∈ α（f <$g）。因此，α（f）<$g<$α（f<$g）。对于另一个包含，设（t，f）∈α（f<$g），其中t是任意的.则有不可数多个x使得（t，x）∈ f ∈ g。 对于每个这样的x有一些s x使得（s x，x）∈f，并且s x=sx. s x，t=t x. t x，其中每个（t x，s x）∈g.但是sx是从可数集X中抽取的，所以一定有一些s使得 sx=s对于不可数的x。由此得出，对于不可数的多个x，（s，x）∈f，因此（s，n）∈α（f），然后（t，n）∈α（f）<$g。对于每一个X，R，α（在X，R中）= . 独特的调解地图F：R1也是空关系，但显然不是α（g）=G对于所有G。因此，FQop在FQop中不是密集的。我们不知道在非浓缩情况下纠正这种情况的直接方法。幸运的是，从上面的反例中可以清楚地看到，密度的失败是由自然变换α的分量的不连续性造成的，这可以通过处理Cpo富集范畴而不是普通范畴来消除。由于我们一直都打算转移到Cpo设置，以便恢复递归的语义，这是无害的，尽管画面可能比人们希望的更微妙我们让Cpo表示有向完全偏序范畴，可能没有底元，和连续函数。 回想一下，Cpo-范畴有hom-cpos而不是hom-set，复合是hom-cpos上的连续函数。 范畴FQ、FQop和FQop可以看作是Cpo-范畴：给定集合X和Y，FQ（X，Y）是X和Y之间关系的集合，按包含排序。验证组合是连续的很简单Cpo函子范畴CpoFQ具有来自FQ的所有Cpo函子作为它的对象到Cpo，也就是说，函子的作用在态射是连续的。Cpo函子之间的映射归结为底层普通函子之间的普通自然变换;但请注意，这种自然变换是Cpo中的映射，因此是连续函数。在此设置中，FQop是398G. McCusker，J.Power/Electronic Notes in Theoretical Computer Science 265（2010）389F--⊆- -∈×→◦◦FFQop的稠密子范畴定理5.1 FQop在FQ op中稠密。这里的稠密意味着从FQop到CpoFQf的函子 将对象X带到FQop（J，X）：FQfCpo是完全忠实的作为Cpo-函子，即它对hom-cpos的每一个作用都是序同构。证据我们必须证明函子在hom-cpos上的作用是内射的、满射的和反射序的。对于内射性，观察到如果f，g：X Y是FQop的不同映射，则必须存在某个对（s，y）X出现在f中但不出现在g中的Y（反之亦然）。我们必须证明自然变换FQop（J，f）和FQop（J，g）是不同的。设A X是包含s的所有元素的任何有限子集。实例化A上的自然变换并应用于A，X中的态射，给出了A，X中的两个映射f和A，X中的g，其中一个包含对（s，y），而另一个不包含，如所需的。一个类似的论证表明函子更有趣的是满射性的问题。设α：FQop（J-，X）→FQop（J-，Y）是任意自然变换。就像在非富集情形中一样，存在唯一的f：X→Y使得α（inA ，X）=f<$inA，X，对于所有有限A<$X：具体地说，这个f由所有那些对（s，y）组成，使得对于某个A，（s，y）∈α（inA，X）。还需要证明α=FQop（J−，f），即对于任何有限集合A和映射g：A→X，α（g）=f<$g。但对于任何有限BX，应用α的自然平方，FQop（JB，X）αBFQop（outX，B g，X）FQop（JA，X）一FQop（JB，Y）FQop（outX，Bblog，Y）FQop（JA，Y）到 的 元件 在B中，X的 FQop（JB，X） 意味 的 αA（inB，X<$outX，B<$g）=αB（inB，X）<$outX，B<$g=f<$inB，X<$outX，B<$g。述组地图{inB，XoutX，Bg：A→X|BX，B finite}是有向的，上确界为g。因此，根据αA的连续性，αA（g）=f<$g是必要的。Q我们所处的局势是令人满意的，但有些微妙。 函子范畴CpoFQf是局部小的和笛卡尔闭的，并且包含FQop作为一个完整的子范畴，所以我们能够给理想化的大陵五语义，正如奥赫恩和雷迪所解释的那样转向Cpo-范畴从一开始就在议程上，因为希望使用固定点来建模递归然而，Cpo富集起着双重作用，因为FQop不致密没有它，这使得构造不太灵活，而且我们在密度论证中使用了定向完备性而不是ω完备性这一事实增加了困难，因为Cpo不是局部可表示的，而ωCpo是。然而，我们已经确定了一个小的“世界”类别αG. McCusker，J.Power/Electronic Notes in Theoretical Computer Science 265（2010）389399→→提供了一个理想化的大陵五模型定理5.2CpoFQf中的理想大陵模型是二阶完全抽象的。证据这一证明遵循奥赫恩和雷迪的证明。由于FQop缺乏Reddy原始物空间模型的相干结构然而，在理想大陵五上增加非决定性是一种保守的推广（例如见[10]），因此这对结果没有影响。Q63级完全抽象失败我们现在给出一个完全抽象的反例，也就是说，在理想大陵五中，一对项在上下文上是等价的，但有不同的外延在函子范畴模型中。 这两项的类型是三阶的，所以我们有一个尖锐的结果：模型是完全抽象的二阶，但没有进一步。这些项的形式为λf：（λ f））其中M1和M2定义如下：M1= new（λx.f（λc.x：= 0; c; x：=！x+1; c; if！x≥ 2则Ω else x：=0）M2=f（λc.c;c）在这里，我们使用了一些语法糖，使用in fix操作符;和：=代替函数seq和assign！用于deref，以及易于定义的标准算术和布尔运算。引理6.1项λf.M1和λf.M2在上下文上是等价的。证据 这些术语的等价性是通过分析它们在完全抽象的博弈语义学中的外延来建立的[2]。 我们在这里不详细介绍游戏模型，但为熟悉该模型的读者给出了等价性证明术语的博弈含义f（λc.x：=0;c;x：=！x+1;c;if！x≥2则 Ωelsex：= 0）是博弈（（4→3）→2）×var→1。我们使用子脚本来标识这四个事件，并以类似的方式标记它们的运行和完成移动该策略的作用如下：• 当O播放运行1时，播放运行2• 当O播放完成2，播放完成1• 当O播放run3时，播放write（0），当O播放ok时，播放run4。我们将运行4的这种情况称为移动的第一次调用• 当O在响应第一次调用run4时播放done4，播放read;然后O播放某个值n，P播放write（n+1）;然后O播放ok，P播放run4- 这是第二次调用。400G. McCusker，J.Power/Electronic Notes in Theoretical Computer Science 265（2010）389联系我们→−→→→• 当O响应于run 4的第二次调用而播放done 4时，播放读取;当O播放值n时，播放写入（0），如果n为0，1，否则不作响应;当O播放ok时，播放done3。如果我们从这些策略中剔除所有的var移动，我们就得到了f（λc.c;c）项的策略。因此，为了建立等价性，我们只需要证明，如果O 这是通过归纳法来完成的，上述策略：我们表明，• 当运行4的第一次调用被播放时，最后一次写入携带值0• 当运行4的第二次调用被播放时，最后一次写入携带值1• 当响应于第一次调用而播放done4时，最后一次写入携带值0• 当完成时，响应于第二次调用播放4，最后写入携带值0或1• 当播放Done3时，最后写入进位值为0。有趣的案例涉及完成的4个动作。当使用done4时，前一步棋必须是run4，所以最后一次写入是0（第一次调用）或1（第二次调用）;或者done3，在这种情况下，最后一次写入是0。 谢谢 对于博弈模型中的问题和答案移动的括号规则，这是仅有的两种可能性，因此证明是完整的。Q引理6.2λf.M1和λf.M2的表示在模型中是不同的，CpoFQf.证据 这些术语将通过将它们应用于特定元素来区分（）的外延）。 这最容易被描述为自然转换α：[[1][[]]。它在X的分量是地图αX：FQop（X+，）−→FQop（X，）f f它把一个映射g映射到{（s1sJ1s2sJ2s3sJ3，）|（s1<$s2<$s3，n）∈ g，（SJ1<$sj2<$SJ3，n）∈ g}.很容易证明这是一个自然的转变。论元项的外延λc.x：=0;c;x：=！x+1;c;if！x≥2则Ωelsex：=0是自然变换[var]] → [[var→var]，其在X处的分量由映射FQop（X，var）→FQop（X+var，var）给出，该映射取映射h到对的集合（s1<$s2s3<$s4，n），其中h包含（s1，write（0）），（s2，read（m）），（s3，write（m+1））和（s4，n），对于某些m∈N和n∈ {0， 1}。把这两个词组合起来，f（λc.x：= 0;c;x：=！x+1;c;if！x≥2则 Ωelsex：= 0）当f与α结合时。这是一种自然的转变，G. McCusker，J.Power/Electronic Notes in Theoretical Computer Science 265（2010）389401关于我们在X上的分量是映射FQop（X，var）→ FQop（X，var），其中h到由所有对（s1sJ1s2s3sJ2sJ3s4sJ4，n）组成的关系，其中h包含对（s1，write（0）），（sJ1，write（0）），（s2，read（m）），（sJ2，read（mJ）），（s3，write（m+1）），（sJ3，write（mJ+1）），（s4，n）和（sJ4，nJ），对于某个m，mJ∈ N和n，nJ∈ {0，1}。根据我们的密度结果，这个自然变换必须对应于FQop（var，var）的一个元素，并且适当的元素是包含所有对的关系（write（0）write（0）read（m）write（m + 1）read（mJ）write（mJ+ 1）read（n）read（nJ），n）其中m，mJ∈N且n，nJ∈ {0，1}。这个关系是λx.f（λc.x：=0;c;x：= 0）x+1;c;if！x≥ 2则Ω else x：=0）。最后，将new应用于此会导致空集，因为在上述关系中没有一个变量作用序列是细胞迹。因此，我们得出结论，将[λf.M1]]应用于α会导致空关系。另一方面，一个类似的和简单得多的计算表明，将[[λf.M2]]应用于α给出了关系式（ε，）（跳跃的表示），它是非空的，完成了证明。Q推论6.3CpoFQf中理想化大陵五的模型对于3阶项不是完全抽象的。7今后工作在O'Hearn和Reddy的带领下，我们已经展示了一个小而简单的范畴如何在理想化的大陵五函子范畴模型中被用作世界的范畴。正如奥赫恩和雷迪所说，这些“世界”与文献中的其他世界具有相当不同的特征，这些世界通常与商店的可能形状相对应。我们建议，我们的模型中的世界被理解为描述一个人可以对程序进行的可能观察。也许还有其他的概念这个想法产生了有趣和有用的模型，以及与并发的预层模型的联系[4]。虽然我们声称，我们简化的对象空间概念产生了与O 'Hearn和Reddy的方法基本相同的模型，但它仍然是自然的是否可以找到Reddy原始范畴的一个小的稠密子范畴 对象空间。我们认为，类似的做法将是可行的，尽管我们还没有详细研究。也许更有趣的是问完全抽象的游戏模型是否可以与函子范畴方法相协调：是否有一种富有成效的方式将游戏模型视为函子范畴？引用[1] Abramsky，S.和G. McCusker，线性，共享和状态：一个完全抽象的游戏语义理想化的Algol与积极的表达式（扩展的抽象），在：1996年研讨会线性逻辑，电子笔记理论计算机科学3（1996年），页。2比14[2] Abramsky，S.和G. McCusker，线性，共享和状态：一个完全抽象的游戏语义理想化的Algol与积极的表达式，在：第297-329卷。402G. McCusker，J.Power/Electronic Notes in Theoretical Computer Science 265（2010）389[3] Bucciarelli，A.，T. Ehrhard和G. Manzonetto，A relational model of a parallel and non-deterministicλ-calculus，in：LFCS107-121[4] Cattani，G. L.和G. Winskel，Preheaf models for concurrency，in：Computer Science Logic：10thInternational Workshop Proceedings，Lecture Notes in Computer Science1258（1997），pp.58比75[5] Hyland，M.，M. Nagayama，J. Power和G. Rosolini，A category-theoretical formulation of engeler-style models of the untyped λ-calculus，in：Proc. MCFSIT 2004，Electronic Notes in TheoreticalComputer Science volume 161，2006，pp. 43比57[6] Kelly，G.M.，[7] Mac Lane，S.，“Categories for the Working Mathematician,” Springer-Verlag, Berlin,[8] McCusker，G.，干扰的句法控制的完全抽象关系模型，在：Proceedings，Computer Science Logic（CSL）2002，Lecture Notes in Computer Science2471（2002），pp.247-261[9] McCusker，G.，关于类Algol语言中坏变量构造函数的语义，在：S。Brookes和P. Panangelman，编辑，Proceedings，第十九届编程语义学数学基础会议，蒙特利尔，2003，理论计算机科学电子笔记（2003）。[10]McCusker，G.， A graph model of imperative computation，Logical Methods in Computer Science6（计算机科学中的逻辑方法）（2010），pp. 1-[11] 奥赫恩，P.W.，A. J. Power，M. Takeyama和R. D. Tennent，Syn