游戏，全抽象和完整的完整性（二）_数学联邦政治世界观

2.3表示语义

2.3.1类型作为域

部分数据空间的一般结构特性是什么？ Dana Scott（1970）详细阐述的计算数学理论是该问题的答案，它将一般被称为域作为基本结构的部分排序集。域的部分顺序描述了元素携带的“信息”的定性概念。在这样的框架中，通过引入代表信息的缺失，通过引入新的元素来重新改造发散是自然的。当x⊑y处于此部分订单时，

y与x一致，并且（可能）比x [...]更准确，因此x⊑y意味着x和y想要近似相同的实体，但是y提供有关它的更多信息。这意味着我们必须允许“不完整”实体，如X，仅包含“部分”信息。（斯科特1970：171）

由此产生的部分有序的组还应具有近似序列，特别是无限链x0⊑x1⊑的性质应该会聚到包含Xi累积提供的信息的限制。相同的结构也在Kleene 1952（SECS中的第一次递归定理的证据中有利于剥削

定义2.3（完整的部分订单）。完整的部分顺序（CPO）是部分有序的设置⟨d，⊑⟩，具有最小的元素⊥，使得d的元素的每个增加的链x0⊑x1⊑...... D的元素具有最小的上限⨆nxn。

给定任何SET X，我们通过添加一个新元素⊥获取的SET X-{⊥}为X‖编写x⊥。根据其信息量，通过设置x，y∈x⊥，根据其信息量来命令x⊥的元素是自然的，

x⊑y。⟺（x =⊥或x = y）。

形式X∞的部分有序结构称为平域，其中我们具有BOOL = {TT，FF}⊥和num =n⊥，其将用于解释PCF的地面类型。

对域的一般要求是每个元素是其有限近似的限制，因为可以完全配制的有限度（或紧凑性）的概念，这些概念可以完全配制在部分顺序结构方面：

定义2.4（CPO的有限元素）。如果D是CPO，则对于每个增加的链x0⊑x1⊑，元素d∈d是有限的if

d⊑

⨆

xnīxi（dīxi）。

对于D∞D，符号A（d）表示D以下的一组有限元; A（d）是D. D. D. Unitione元件的一组有限元也称为Compact。

观察到SET X的有限子集正是X的完整晶格的有限元素。它也很有用的是观察到这个定义仅部分匹配我们的直觉：例如，在CPO中考虑有限元∞+ 1

0⊑1⊑2⊑⋯⊑∞⊑∞+ 1。

定义2.5（代数CPO）。如果对于每个d∈d，则D是代数的，则具有增加的x0⊑x1⊑......为D的有限近似

d =

⨆

xn。

如果D是代数，我们说有限元形成D的基础。

需要在代数CPO上的最后一个完整性假设，以便获得适合解释PCF的域名：

定义2.6。给定CPO D，如果x⊆d有一个上限，我们说x是一致的，并且当x = {x，y}时，写入↑或x∈y。如果每个x∈D这样↑具有最小的上限，则始终完成。

以下域的概念被证明是非常方便作为编程语言的语义语言的框架（Scott 1982）：

定义2.7（域）。域是一个始终如一的完整代数CPO，其数量是可数的。

2.3.2高级可计算功能的抽象理论

我们如何在域的元素上使用隐含的信息的概念来开发摘要的可计算性概念？显然，可计算函数应在单调上保留其输入中的信息的任何增加：f（x）⊑f（y）x⊑y。特别是，严格的功能f：d→e过扁平域，f（⊥d）=⊥e的那些是单调的。

考虑域{0,1}∞的元素是有限且无限的位0,1，其中u⊑v如果是无限的，则为U = v，或者U是有限的，U是v的前缀。可计算函数需要的是什么属性作为论点，无限序列⟨b1，b2，b3，..... 作为一个示例，函数搜索：{0,1}→b⊥，其值为tt，如果为u∈{0,1}∞，则为1，否则为⊥。思考序列⟨b1，b2，b3，...⟩，如一次给定一个元素：在该过程中获得的初始段是{0,1}∞的增加的有限元链，

⟨⟩⊑⟨b1⟩⊑⟨b1，b2⟩⊑⟨b1，b2的，b3⟩⊑...

具有⟨b1，B2，B3，......作为极限（即，最小上限）。通过单调性，我们有一个相应的增加的价值链

搜索（⟨⟩）⊑search（⟨b1⟩）⊑search（⟨b1，b2⟩）⊑search（⟨b1，b2的，b3⟩）⊑...

如果搜索（⟨b1，b2，b3，...⟩）= tt，那么必须有一个有限的初始段⟨b1，b2，...，bn⟩，其中搜索（⟨b1，b2，...，bn⟩）= tt，这将是无限序列⟨b1，b2，b3，...⟩函数的累积值。通常，可计算功能F：D→E应该（是单调和）的特性，必须通过在输入x上提供有限量的信息来已经可以获得输出f（x）上的有限量的信息。这相当于斯科特最初引入的连续性概念在他对域的可计算函数理论中：

定义2.8（连续功能）。如果⟨d，⊑d⟩，⟨e，⊑e⟩是cpo和f：d→e是单调，f是连续的

f（

⨆

一世

西安）=

⨆

一世

f（十一）

对于每个越来越长的链x0⊑x1⊑...⊆d。

从指语义的角度来看，连续功能的基本属性D→D是他们承认最小固定点，其结构可以均匀和连续进行：

定理2.1（连续函数的固定点定理）让F：D→D是连续功能，x∈d是x⊑f（x）。然后是元素

⨆

n∈n

f（n）（x）

是最小的，这样f（y）= y。

定义2.9。连续F：D→D的最小固定点是D定义的D元素

修复（f）=定义

⨆

n∈n

f（n）（⊥）。

来自d到e的连续功能，对于CPO⟨d，⊑d⟩，⊑e⟩，形成一个CPO [D→e]，通过设置为f，g：d→e：

f⊑g⟺∀d∈d.f（d）⊑eg（d）。

[D→E]是域，如果D和E是D和E，而固定（⋅）：[D→D]→D是连续的。对CPO的进一步建设，也延伸到域，非常频繁地是笛卡尔产品：给定CPO的D，E，他们的笛卡尔产品被定义为对⟨d的设置d×e，e⟩和e∈e，命令点：⟨d，e⟩⊑⟨d'，e'⟩如果只有d⊑dd'和e⊑ee'。我们可以以分类语言（Plotkin 1978，其他互联网资源）总结这些结构，并说其对象是域的类别并且其义务是连续功能的类别是笛卡尔封闭的。

2.3.3 PCF的连续语义

PCF的标准解释由一个CPOSDσ系列组成，每个类型σ，其中dnum =n⊥和dbool =b⊥，dσ→τ= [dσ→dτ]和PCF常数具有严格的连续函数的自然解释在适当的类型中，例如COND：b⊥→n⊥→n⊥→n⊥被解释为：

气孔导度（b）（x）（y）= {

x。如果b = tt

y。如果b = ff

⊥。如果b =⊥，

此外，操作员Y（⋅）被解释为适当类型的连续功能修复（⋅）。这是在斯科特1969B中考虑的解释，1973年Milner 1973。

E可能包含可用变量的可能性（其类型为基础b）略微复杂化术语的解释，使其取决于另一个参数，环境ρ映射每个自由变量x：τ的e到dτ的元素（如果后者条件满意，我们说ρ尊重b）。当然，当E关闭时，环境是无关紧要的。

PCF术语E：σ（从基础B）的标准解释是一个元素[[e]]ρ∈dσ，用于任何环境ρ，使得ρ的尊重b，由结构诱导而构建，将应用程序作为功能应用程序和λ - 抽象（连续）功能。更一般地，如果每个Dσ是CPO和Dσ→τ，则解释是连续的，连续函数dσ→dτ。

PCF模型是一种解释，满足相同类型之间的预期身份。我们将省略PCF模型的一般特征的细节，读者被提交给ONG（1995：SEC 3.2）和Berry，Curien，＆Lévy（1985：Sec。4），但只是指出必须采取的例子考虑到需要这样的一般性时，为了承认函数类型的元素不是，严格地说，函数的解释，我们必须假设一个应用程序操作系列

⋅στ：dσ→τ×dσ→dτ

这样，如果b⊢e1：σ→τ和b⊢e2;σ，[[e1e2]]ρ= [[e1]]ρέστ[[e2]]ρ∈dτ。对于所有元素F，g∈dσ→τ，f⊑g，如果x∈dσ的所有元素f，g∈dσ→τ，f⊑g，则为令人令人令人令人瞩目的if 对于所有元素F，g∈dσ→τ，f = g If且仅当f⋅x=g⋅x来说，模型是扩展的，则为所有x∈Dσ。模型的元素d∈dσ可定义在于e：σ，使得d = [[e]]。

2.4有关操作和表示语义

讨论完整抽象的常规设置要求我们介绍以下概念：

定义2.11（观察预订和等价）给定PCF术语E和E'的相同类型σ，我们写入e≾obse'（读取e是比e'的观察到少于e'），如果每个程序上下文c []有σ和任何值v的孔，那么

C [E]⇓v意味着C [E']⇓v。

我们说e和e'是观察到的等价物，并且如果e≾obse'和e'≾obse则写e≃obse'。

观察等价是一致的。 PCF术语上的另一个同时由模型中的表示的平等提供：

定义2.11（表示预订和等价）。给定PCF术语E和E'相对于基础B，我们写e≾dene'如果[[E]]ρ⊑[[e']]ρ尊重B.我们写e≃dene'如果e≾dene'和e'≾dene。

命题2.1（PCF的计算充分率）。以下两个陈述适用于PCF的标准模型，等同于：

对于同一地面类型E的任何两个PCF术语，e'，e≃dene'意味着e≃obse';

对于地面类型的任何闭合PCF术语E和该类型的任何值V，[[E]] = [[V]]如果且仅当e⇓v时;

我们现在可以在标准模型中对⊥的直观解释合理，地面类型被解释为平域：

推论2.1。对于地面类型的任何闭合PCF术语E，e⇑如果[[E]] =⊥。

在第1.3节中，我们已经确定了基于同义词，即术语解释的平等的非常一般的（公式）全抽象。在PCF中，其预期模型在所有类型部分排序时，我们可以定义更强大的属性：

定义2.12（不等式全抽象）。 PCF的连续模型⟨{dσισυντtypes}，[[⋅]]⋅⟩的PCF非常完全抽象，如果关闭术语E，E'，e≾obse'意味着[[E]]⊑[[e']]。

可明确是全抽象的关键，如米纳和幽灵的以下重要结果所示：

定理2.2。 PCF的连续令人垂直模型是完全抽象的，如果只有每个类型σ，dσ是一个有限元可定义的域。

我们现在转向PCF标准型号的全抽象属性的失败，如同绘图在他的经典研究中（Plotkin 1977）所示：

命题2.2。对于逐个名称评估，PCF的标准模型并不完全摘要。

证据是基于观察，我们可以构建识别并行或功能的PCF类型（BOOL→BOOL→BOOL）→NUM。具体而言，考虑定义定义的“测试”术语Ti，其中i = 0,1：

λf：bool→bool→bool.if（f⊥bool然后

如果（f⊥booltt）那么

如果（f ff ff）那么

⊥num

否则我

否则⊥num

然后，D [[t0]] por = 0≠= d [[t1]] por，其中por由表（4）定义，因此t0≃dent1不保持。但是，PCF中没有程序上下文可以分开T0和T1，因为POR不是可定义的。这可以通过组合方式表征在其（子）术语的评估过程中，作为曲素在活性物质中的评估过程中的评估过程所产生的依赖关系，作为Plotkin（Plotkin 1977：Lemma 4.2）。作为替代方案，可以建立一个计算的PCF模型，其功能享受弱序列性（我们在下面讨论的，在2.5.1节中讨论），因此，函数POR被排除在其中：沿着这些线路的完整正式证明在Gunter 1992中给出了（秒6.1）。

解决完整抽象问题的一个选项是扩展语言：Plotkin（1977）的显着结果显示，添加并行 - 或足够：

命题2.3。标准模型是完全抽象的语言PCF与并联或。

Milner（1977）已经表明，通过在每个类型σ上识别观察到的等效项，通过完成所得部分有序的设置将其部分有序的设置转换为CPO，通过将封闭术语设置为PCF的全抽象模型。

推论2.2。有一个独特的连续，令人垂直，不平等完全抽象的PCF，达到同构。

PCF的完整抽象问题在于找到构成完全抽象模型的域类和连续功能的直接描述。对此问题的解决方案需要精确的标准来评估模型的建议描述令人满意的程度。如果一个人接受“精确的最小条件，即jung＆stounton（1993）给出的”完全抽象问题的语义解决问题“（1993）给出的可能性，即以有效的方式描述PCF的合法版本的域Dσ（其唯一地面类型）BOOL），然后失败的故事试图给出完全抽象模型的这种直接描述是有道理的，通过LOADER（2001）的结果是：

定理2.3。有关合法PCF的观察等价不当。

但是，仍然可以找到一个有弹性完全抽象模型的直接描述（Abramsky等，2000：411）：

定义2.13（密集全抽象）。如果每个Dσ是代数，并且所有紧凑的元件都是可定义的，则PCF模型非常摘要。

追求这一发展的全部抽象问题导致我们对游戏语义，这将是下一节的主题。在此之前，我们概述了通过高阶顺序计算的语义表征来减少模型的主要尝试。

2.5朝向连续语义

PCF连续语义的全抽象失败的原因是存在评估需要并行计算的函数。现在，我们描述了一种通过与定义它们的域的结构相关的属性来表征功能的序列性的一些提议。这是对PCF全抽象问题解决的密集研究领域，以及它从它出现的一些洞察力非常自然地在第3节中讨论的游戏模型非常自然。另外，在顺序表征表征的尝试摘要也是一个非常有趣的演示在编程概念的语义分析中部分秩序的语言表现力。

直观地，顺序函数是评估序列的评估：这意味着可以安排其参数的评估，以便对函数的评估终止具有正确的值; 如果评估其中一个分歧，整个评估发散。在此过程的每个阶段，存在一个参数，其值需要在函数的输出中获取更多信息。为了考虑在语义级别的计算的这种因果结构，我们需要丰富域结构，以便元素上的顺序反映了计算事件的发生及其因果顺序。这提出了一种解释第2.3.1节中激励CPO的公理的信息的抽象概念的另一种方法。现在，

信息与（出现）事件有关：即发生这些事件的信息。例如，在n⊥的情况下，⊥可能意味着没有发生事件并且整数n可能意味着发生整数n的事件输出（或者在输入的另一个情况中）。（Plotkin 1978，其他互联网资源）

2.5.1稳定性

事件的一个解释将它们视为在评估表达式中的价值。该解释始于erry（1976）开发的递归程序的自下而上计算的上下文中，其中递归定义被翻译成显示表达式结果的依赖性的图表上的子表单抑制的结果。此背景自然而然地表明事件X的生产者的概念，作为一组必须发生的事件，以便x可能会发生。以部分订单，浆果（1976）定义的语言（1976）重新制定了这一观察：

定义2.14（稳定性）。让D1，...，DN，D为平板CPO和F：D1×...×DN→D单调（因此连续）。然后如果每一个都是稳定的

→

=⟨x1，...，xn⟩∈d1×...×dn有一个独特的最小元素m（f，x）⊑

→

这样f（m（f，

→

））= f（

→

）。

显然，并行或功能不稳定：值POR（⊥，TT）= TT = POR（TT，⊥）没有最小的生产者。稳定函数的显着性属性是它们允许构建一个新的PCF模型，其中Dσ→τ是解释Σ和τ类型的域上的一组稳定功能，这些功能是Σ和τ的类型，这些功能是斯科特域的改进（浆果1978）。从我们的角度来看，这些定义的重要结果是以下充分性结果（Gunter 1992：Chap。6）：

命题2.4。 PCF术语的解释为Di-域的元素，其中Dσ→τ是从Dσ与稳定顺序的Dτ的稳定功能的DI域，是PCF的计算充足的模型。

此结果完成了显示2.4末尾在第2.4节结束时为PCF连续模型的完整抽象的故障的参数，如果使用的序列性的非正式概念被形式化为稳定性。最近，PCF的稳定模型已被证明是PCF扩展的完全摘要（Paolini 2006）。

2.5.2顺序函数

由于Vuilleemin（1974）和Milner（1977），顺序的第一个定义表示，在扁平域上的N-ARY函数F在参数中是顺序的，如果F的顺序指数I，则取决于⟨x1，...，xn‖，使得输出信息的每增加增加必须在参数i上增加信息。例如，功能COND：b⊥×n⊥×n⊥→n⊥在任何输入元组中都是顺序顺序。事实上，它的顺序指数在⟨⊥，m，n⟩是1; 它的顺序指数在⟨tt，m，n⟩是2，其顺序指数在⟨ff，n⟩是3.但是在输入⟨⊥，⊥⟩处的函数por的序列指数没有：b⊥×b⊥→b⊥。

虽然所有顺序功能（在扁平域）是稳定的，但顺序比稳定性更强。例如，来自b⊥×b⊥×b⊥到B的连续功能定义为三个分配的最小连续延伸

⟨tt，ff，⊥⟩↦tt，⟨ff，⊥，tt⟩↦tt，⟨⊥，tt，ff⟩↦tt。

在参数中没有顺序索引⟨⊥，⊥，⊥⟩，但稳定，因为参数⟨tt，ff，⊥⟩，⟨ff，⊥，tt⟩，⟨⊥，tt，ff⟩是成对不一致的。

以下结果将支持添加到搜索顺序的语义特性：

命题2.5。让F：D1×××DN→D是连续功能，其中DI，D是n⊥或b⊥。然后f是顺序且仅当它在PCF中可定义时才。

（本章完）