理论计算机科学电子笔记173（2007）203-219www.elsevier.com/locate/entcs顺序性与新鲜名称J. Laird莱尔德1，2部英国苏塞克斯大学信息学摘要我们研究域理论的指称语义的CPS演算新鲜的名称声明。这是一个完全抽象的CPS翻译的目标，从nu演算与第一类延续。我们描述了一个概念的“FM分类”模型为我们的演算，一个简单的解释，由于欣维尔和皮茨的名称生成。我们表明，完全抽象失败（在第二）在最简单这种模型（FM-CPOS）的实例，因为存在并行元素。因此，我们定义了一个序列模型-FM-双序，基于关键词：延续传递风格，新鲜的名字，顺序性，FM集，全抽象。1介绍本文是一个新生成的名称在连续传递风格（CPS）设置的指称语义的研究。新生成的名称是许多计算效应的关键元素，并且本质上也是有趣的;它们可以用于表示秘密，例如加密密钥。函数设置中的名称的行为相当微妙，并且已经通过原型演算（如nu演算[7]）使用操作和指称技术进行了研究。皮茨和其他人所提倡的命名指称语义的一种方法本质上，FM集合是可数原子集合（表示名称）的排列群的作用，其中载体集合的每个元素仅依赖于有限个原子（其支持）：如果我们将项解释为载体集合的元素，则1 英国EPSRC资助GR/S721812 电子邮件地址：jiml@sussex.ac.uk1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.02.035204J. Laird/Electronic Notes in Theoretical Computer Science 173（2007）203群体行为对应于用一个名字替换另一个名字。因此，例如，我们可以将名称的类型解释为具有规范置换群作用的自然数的FM-集合（或在FM-cpo处的集合）N。Shinwell和Pitts [6]已经观察到，在这样的设置中，名称生成有一个简单而自然的延续传递式N的任何元素-从N到N的- 必须在每个不支持它的参数上取相同的值，所以为f提供新名称的结果必须是该值。当我们考虑普遍性问题时（它包含什么“垃圾”？），这种方法的局限性在限定于FM-cpo模型时可以看到。和完全抽象（它准确地反映了哪些等价物？）。在模型中存在并行元素，而不是语言，这意味着完全抽象将失败，就像PCF一样，此外，创建和生成新名称的术语之间的一些最简单的等价关系被破坏了。特别地，我们有一个函数p：<$N→ <$N使得p（f）=T，如果存在n使得f（n）= T，从而有效地允许f识别的名字被“猜测”。本文的主要目标是调查一个顺序CPS命名模型，通过在一个类别的工作“FM-bicpos”。这些都是简单地通过扩展FM-cpos与额外的结构，这样的功能，保持该结构（functions）是强序列。在[2，4]中引入了双稳态带有控制操作符的函数语言（SPCF）。在这里，我们将给出一个CPS目标语言的语义与名称生成操作。 有一个完全抽象的翻译到这个演算从（例如）nu演算扩展与第一类延续。我们可以直接证明我们的演算可以在任何具有有限乘积和指数的“FM-范畴”中得到合理的解释然后，我们研究的完整性性质的解释，表明，完全抽象的条款，直到四阶（即条款的类型包含多达四个嵌套的延续<$-运营商）。然而，完全抽象在五阶上失败了，这表明即使在这种外延的设置中，顺序性也不足以获得完全抽象。1.1相关工作已经提出了几个新生成名称的函数语言模型，包括Stark在[7]中描述的nu-演算的（等价）函子范畴和FM-集模型，mini-FreshML的FM-cpo CPS模型[6]，以及游戏模型[3]和[1]，也基于名义集。外延和内涵模型都给出了有限的信息等价的功能设置，丁与新鲜的名字，在外延的情况下，因为完全抽象失败，在低级别的类型，在更内涵（游戏）模型，因为完全抽象依赖于商，或允许通过存储泄漏的名称。虽然我们的语义不是完全抽象的，但它确实捕捉到了大量的碎片-J. Laird/Electronic Notes in Theoretical Computer Science 173（2007）203205Γv：Bv∈ {tt，<$}Γn：Nn∈NΓC：<$C∈{T，<$}Γs：NΓt：NT=t：Bs：BΓ bop（s，t）：Br，x：TTs：<$P最新消息：Nr：BIfr thens elset：si：Ti：i nΓ►⟨si|中文<<（简体）r，x0：T1，. . ，xn−1：Tn−1s：Γ λ（x0，.，xn−1）.s：<$ m，Ri= Ti+m。一个类型的阶是它的延续-嵌套深度-所以N，B的阶为0，n< nTi的阶为max {o（Ti）} |i≤n}且<$P的阶为o（P）+1。通过λ-抽象和应用，在值类型变量的上下文上形成术语，以及：返回类型的常数T（错误）和T（发散）一组名称（常量）{n |n∈ N}，一个条件，一个新名字生成器new：N和布尔表达式形成的tt，和平等测试的名称。我们将新的λx.s写成νx.s。术语形成/类型规则在表1中给出2.1操作语义操作语义（表2）由一个终止谓词给出，它位于返回类型的项s和值k的对s，k上，使得在s中出现的每个名称都小于k。注意闭项s：B只是命题逻辑206J. Laird/Electronic Notes in Theoretical Computer Science 173（2007）203T，ksk，k+1新南威尔士州s[→t/→x]，k（λ（→x）.s）n→tn，kns，kIf r then s else t，k|R|=TTt，kIf r then s else t，k|R|=表2CPS-nu-演算的运算语义在一组原子上，由相等语句n = m（对于自然数n，m）组成，因此具有布尔值的标准解释|S|. 我们写s如果存在k使得s，k和定义观察近似的标准概念-s4t如果对于任何返回类型的兼容上下文C [ ]，C [s]蕴涵C [t]-和等价-s t如果s 4 t和t 4 s。引理2.1（上下文引理）对于任何项s，t：<$P，s4t当且仅当对于所有项L：P，M L<$蕴涵N L <$。证据 遵循PCF [5]的标准证明。Q引理2.2如果s，t是没有显式名称的项，则s 4 t如果对于任何无名称的兼容上下文C[ ]，C [s]蕴涵C [t]。证据给定由上下文C[ ]区分的无名称项，我们可以通过将C[ ]中的所有显式名称替换为变量并使用new声明它们来获得区分上下文。Q正如在nu演算中一样，我们的演算中有一些有用的等价示例，它们捕获了演算中名称生成的各个方面，并且可以用于测试任何候选模型。这些与Stark [7]考虑的nu-演算等价有关，尽管它们不是后者的CPS翻译。这种等同的两个关键实例是：(i) 在类型N处：λκ.νn.κ λy。如果x = n，则Telse <$λy。- 是的(ii) 在<$$><$$>（N× <$U）类型下：λk.νn.k<$λf.νm.f<$m，λa.f<$n，λk.k<$λf.νm.f<$m，非正式地说，（1）成立，因为任何提供的类型为N的参数必须将其arging应用于不等于n的名称。（2）成立，因为任何提供的参数我们将使用语义手段正式证明这两个等价性。J. Laird/Electronic Notes in Theoretical Computer Science 173（2007）203207s=t=λκ.s<$λa.t<$λb.κ<$a=b<$v=λκ.κ<$v<$v∈{tt，<$}λx.s=λκ.κλ（x，z）.szst=λκ.s λ（a）.t λb.ab，κ如果s则t1，否则t2= λκ.s <$λa。如果a则t1<$κ<$else t2<$κ <$<$x = λκ. κ<$x<$。call/ccs=λκ.s<$λa.a<$λ（b，c）.κ<$b<$，κ<$new=new表3控制核演算2.2CPS翻译我们可以使用CPS-nu-calculus来解释语言，例如通过CPS翻译的nu-calculus。在这里，我们将给出用第一类延拓扩展我们的源演算是一个简单类型的，基于基础类型ν，o（名称和布尔值）的按值调用λ演算，具有常量：tt：o和：o，名称的相等测试，条件，新名称生成new：ν和带有当前延续的调用/cc：（（TS）T）T。我们可以通过标准的CPS translation（）将其解释为CPS-nu- calculus，将每个基本类型发送到相应的值类型，并将S转换为<$（S×<$T）。翻译取上下文中的术语x1：S1，.，xn：SnM：T到x1：S1，.，xn：Sn<$M：<$（<$T）在表3中给出。对于闭项s：o，如果s<$λb，我们可以写s <$tt。IfbthenTelse，0-很容易证明这符合nu演算的标准运算语义。因此，我们可以推导出控制核演算的项的观测等价的概念，根据定义，关于这个概念，CPS翻译是合理的;它也是完整的，因此是完全抽象的（推论3.7）。3CPS的语义在引言中简要介绍了Shinwell和Pitts [6]提出的名字生成的CPS解释在这里，我们给出了一个更正式的和一般的帐户，我们的CPS演算的语义在任何对于可数的“原子”集合G在集合A上的作用是连续的（关于A上的离散拓扑）当且仅当对于每个元素a∈A，存在有限子集k<$X使得π（x）=x对所有x∈k蕴含π·a=a。设v（a）是a的支集，是a的最小支集。一个FM-集（A，·）是一个具有连续G-作用的集合A，一个FM-序是一个具有偏序的FM-集（A，·）使得x≤yi ∈π·x≤π·y。一个FM-序D是一个FM-cpo，如果每个有向集X有界支撑（即使得{ν（x）|x∈X}是有限的）有一个最小上界。一个FM范畴是一个C范畴，它富含了一个连续的G作用，即：每个hom-set是FM-set-使得（π·f）;（π·g）=π·（f;g）和π·id=id.态射208J. Laird/Electronic Notes in Theoretical Computer Science 173（2007）203f是不变的，如果ν（f）= π。FM-范畴的基本例子是FM-集合（即对象是FM-集合，从A到B的态射是函数f：A→B，其中π·f定义为（π·f）（a）=π·（f（π−1·a）））。同样，我们有FM-FM的类别-序和单调函数以及FM-cpos和连续函数。注意，所有这些范畴都是笛卡尔闭的。我们也可以构造游戏和策略的FM-范畴[3，1]。我们不妨把原子的集合X取为N。设C是FM-范畴有限的产品。我们可以说C有布尔值、命名和对象，如果它包含对象B、N、N，使得：• B是终结对象与自身的不相交余积• C（1，N）由不同的映射{i|i∈N}使得π·i = π（i），并且存在一个“可判定的相等”态射eq：N × N → B使得<$n，m <$; eq = in l（n）当且仅当n = m.• C（1， n）由不同的不变映射{n，T}组成，使得f：N→n =g：N→n当且仅当n;f= n; g对所有n。在FM-集范畴中，B和N是两点集，N是具有标准G-作用的自然数集。在FM-cpos范畴中，B和N具有离散序，且在F中有F± T.新名生成常数new的解释来自于以下观察。引理3.1给定f：N→N，且m，n：1→N，m;f=n;f当且仅当m∈ν（f）n∈ν（f）.证 据在 不失 一般 性的 情 况下 ， 假设 对于 某 个m/∈ν（ f ） ， m ; f = T 。 设[mParticipin]∈G是交换m和n而留下所有其它点的自同构 如果n/∈ ν（f）则[mParticipin] 在 f 的 稳 定 子 中 ， 所 以 m; f = （ [n Participim]·n ） ; f = n;（[nParticipim]·f）= n;f= T。因此{l|l;f={\displaystyle {\frac {l}\，{f}\，}给定π∈G，设π·n = n，对所有n，使得n;f= n。则对于任何n，如果n;f= n，则n;（π·f）=（π−1·n）;f = n ; f= n;如果n;（π·f）=（π−1·n）;f= n，则π（π−1（n））= n = π（n），因此n;f= n。 因此π在f的稳定子中，所以ν（f）<${n |n;f = n; f当且仅当m ∈ ν（f）i <$n ∈ ν（f）为必需的.Q定义3.2假设C是一个FM-范畴，它有一个n-指数，即一个n-对象，对于任何对象A，有一个n-被A的指数n-A。 (So每个态射f：N→A有一个 设k是P（N）上的一个选择函数。C中的态射new：N→N是名生成器，如果对任何f：N→N，f根据引理3.1，f'; new = n ; f当且仅当n /∈ ν（f）.因为每个f：1→N有有限支集，{x|因此，f（x）=T}要么是有限的，要么是有限的，我们有新的; f' = T当且仅当{n|n;f= n}是有限的。因此，在FM-集范畴中，我们可以定义一个名称生成器：new（f）=T当且仅当{n|n;f= n}是有限的。这也是FM-序和FM-cpos范畴中定义良好的态射：为了证明它是有界连续的：假设FN是定向的，J. Laird/Electronic Notes in Theoretical Computer Science 173（2007）203209有一 个 boundedsupport，且supposen w（f） =f∈F.Then（.F）（x）=Ti<$存在f∈F使得f（x）=Ti<$存在f∈F使得x∈ν（f）。Hencebbon deneso f e s ortoffesortoFesofesoF）（x）=Tf所以，我们应该这样做。 F）=Areuired.给定一个FM-范畴，其中包含布尔对象和命名对象、有限乘积和n-指数、一个名 称 生 成 元 和 可 判 定 的 等 式 ， 令 [B]] =B ， [[N]] =N ， [[<$T]]= n[[T]] 和 [[<$inTi]]=<$i n[[Pi]。范畴结构产生直接的解释的操作和常数，和一个简单的证明的可靠性方面的操作语义。我们通过一个简单的结构归纳法建立了以下结论。引理3.3如果n ∈ ν（[[s]]），则n出现在s中。命题3.4（合理性）对于任何闭项，如果s，k ≠ T，则[[s]]= T。证据 通过归纳推导。 对于新规则，假设sk，k+1，因此n [[s]]，kn;app=T通过归纳假设。假设k不出现在s中，所以根据引理3.3，k/∈ν（[[s]），所以[news]]=[[s]];new=[[s]]，k;app=T。Q命题3.5（不确定性）如果[[s]]=T，则s ≠ T。证据 一个标准的可计算性谓词参数。Q因此，微积分的任何FM范畴模型在等式上都是可靠的-[s]]=[[t]]意味着s≤t-而任何FM阶丰富模型（其中t ≤T）在不等式上都是可靠的-[s]]±[[t]意味着s4t。作为我们语义的第一个应用，我们可以用它来证明控制nu演算的CPS翻译是完全抽象的。命题3.6 对于CPS 演算的每一个无名项 s：T，存在一 个 常数s^ ：T，使得[[s^]]=[[s]]。证据我们 证明 感应 对 长度 的 为 任意β-正规 term x1：T1，.，xm：Tm，y1：S1，.，yn：€Sm►S：Σ那里是一term x1：T1， .. . . ，xm：Tm，y1：S1→B， . . ，yn：Sn→Bs^：Bsuc hthat[s^]]（）=[[s [λ（a）.z1]a，λb. []. [λ（a）.z1α，λb. 对于任意值型为x1的β ：T1，.，xm ：Tm，y1 ：S1，.，yn ：€Sm ► s：R有一个te rmx1：T1，.，xm： Tm，y1：S1→ B，...，yn ： Sn→B组[[s^]]=[[λκ. κ∈s[λ（a）.z1∈a，λb. ⊥⟩/y1].. . [λ（a）.z1α，λb.[2017 -01 -01]举例来说s^：Rsuc hthat• Supposess=x≠1，λa. t2π，其中x：S→T=<$（S× <$T）. TheNs^=（λa. t^2）（xit^1）。• Supposes=yt，其中y：S。 这是一个很好的例子。• Supposes=λ（x，y）. t：S→T=<$（S× <$T）。则ns^=λx。呼叫/ccλy。（（λk. ^t））.210J. Laird/Electronic Notes in Theoretical Computer Science 173（2007）203QJ. Laird/Electronic Notes in Theoretical Computer Science 173（2007）203211^推论3.7从控制nu-演算到CPS-nu-演算的CPS转换是完全抽象的。证据 给定控制nu演算的闭项s，t：T，假设s/t。则存在一项λk.r：<$T使得sλk.r≠ 0 且 tλk.r≠ 0 。 设 v ： T→o=λk 。 call/ccλf. r[ftt/T ， （ f ） /k]Ten[[Ifv sthenTelsen]]=[[sλk. r]]=Tand[[If vt thenT else]]=[[s λk.r]]=，因此vs tt和vt/tt是所需的。Q在一般模型类中为CPS-nu-演算定义了一个（不）等式上合理的语义之后，我们可能会问：对于哪些类型，我们的模型在观测等价性方面是完全的如果我们考虑由FM-cpos和有界连续函数组成的模型，那么对于仅布尔和连续类型的微积分片段，完整性必定失败，因为模型包含并行元素。然而，该模型的非顺序特性也意味着它无法准确地反映与名称生成行为具体相关的等效性。例如，在类型N上的语言的封闭项的唯一上下文等价类是新的，λκ。T，λκ。，和λκ.κ n为每个名称n。然而，在FM-cpo模型中，有更多的功能从CNON到CNON，例如，p定义为p（f）=T，如果存在n使得f（n）=T。这足以打破F = λκ.ν n.κλx之间的等价性（1）。如果（x = n），则Telse ≠ λx。⊥- F（p）= ν n.p（λx. 如果（x = n）则Telse（n）= νn。T = T，且n（p）= n。因此，定义一个更准确地反映命名的模型的关键似乎是完全捕捉微积分的顺序性质，这就是我们在本文剩余部分中使用双序来实现的目标。4FM双目在双序的可能的等价定义中，我们给出如下：定义4.1A（X）双序[2，4]是一个元组（D，±，X），其中（D，±）是一个偏序（扩张序），X是D上的一个等价关系（X-相关），使得每个X-等价类是关于±的一个分配格，包含到D中保持二元交和联结。定义4.2FM-双序是一个元组（D，±，，·），其中（D，±，）是一个双序，（D，±，·）是一个FM-序，对每个d，e∈D，de蕴涵π·d<$π·e。D是FM-bicpo，如果（D，±，·）是FM-cpo，如果X，Y<$D是有界支撑的有向集，使得X<$Y（即对所有x∈X和y∈Y，存在xJ∈X，yJ∈Y，则x±xJ， y±yJ和dxJ∈yJ）ten。{xxxy}|x∈X<$y∈Yx y}=.X.Y.我们定义了一个FM-范畴FB，其中对象是FM-bicpos，从A到B的态射是有界连续函数f：|一| → |B|对于一个环x，fT[x]是一个与[f（x）]n相同的同态，即， 对于所有的x，y∈|D|则f（x）<$f（y），f（x<$y）=f（x）<$f（y）anddf（x<$y）=f（x）<$f（y）. 一一个具有T和n个元素的双序函数是严格的，如果f（T）= T和f（n）= n。212J. Laird/Electronic Notes in Theoretical Computer Science 173（2007）203笛卡尔闭包是通过结合CCCs中的相关定义而得到的。命题4.3 FB是双笛卡尔闭的。证据双序上的积和余积运算是直接（逐点）定义自底层集合上的运算，其中单元1和0是单点和空双序。给定FM-双pos D，E，我们定义指数DE为从D到E的和函数的集合，它们都是有序的，其中fgifxyimpliesf（y）↑↓g（x）anddf（x）g（y）=f（y）g（x）and f（x）g（y）= f（y）g（x）。必要的满足和联接是逐点定义的[4]这是一个证明bicpo。QFB有布尔对象、命名对象和命名对象，以及一个名称生成器-函数new（f）=f（v（f）c）是n，因为对于所有f，g，我们有new（fg）=（fg）（n（N−（v（f）v（g）=f（n（N−（v（f）v（g）v（n（N−（v（f）v（g）=new（f）v new（g）同样，new（fg）=new（f）new（g）。我们可以首先观察到我们的模型是双序贯的（即，相对于T和T元件两者顺序例如，它排除了并行复合par：× →，因为=par（，）/=par（T，）par（，T）=TT=T。更一般地说，以下是证明在[2]：引理4.4给定点双序A1，. ，An，每个严格的，单调的和非单调的函数f：A1×…对于某些i ≤ n（唯一的，如果Ai是非终结的），× An→T是i严格的（即πi（x）= T蕴含f（x）= T，πi（x）= T蕴含f（x）=T）。作为双稳态力与命名相关的一个例子，我们观察到，与FM-cpo模型不同，在N型没有“垃圾”。首先，定义pn∈N n = λx。若x = n则Telse n，且qn∈N = λx。如果x = n，则elseT命题4.5（N）的唯一元素是T，，{λk.k n|n∈ N}新的。证据 假设f：（N）不在{T，，new}中。那么存在着一些g：N≠0使得f（g）g（v（g）c）. 设f（g）=T，则g（n）=T当且仅当n∈v（g）.则g=n∈ν（g）pn，因此通过双稳性，f（pn）=T，对于某个n。以来f/= T，我们有f（pn）<$f（qn）= f（pn<$qn）= f（q n）=<$-即f（qn）=<$。因此f（g）=T当且仅当pn±g-即f=λg.g（n）。Q因此，该模型验证了等价性（1）。推论4.6 [[λk.νn.k <$λx. 如果x = n，则T else [λk.k <$λx. [编辑]我的律师。 [[λk. vn. k<$λx. Ifx=nth enTelse]]（f）=f（n）forf∈{T，n ew}{λk.k n|n ∈ N}。Q5完全抽象到三阶在本文的其余部分，我们将考虑我们的模型的完备性。因为它是拉伸的和有界连续的，我们可以证明充分J. Laird/Electronic Notes in Theoretical Computer Science 173（2007）203213抽象到n+1阶，通过证明所有元素或元素的有限基在n阶是可定义的。我们将使用的一个关键思想是类型- 我们写σ<$τ，如果有项x：σ<$inj：τ和x：τ<$proj：σ使得[[inj]];[[proj]是恒等式。在这种情况下，如果普适性在类型τ成立，那么它在类型σ成立-如果[[inj]]（e）可定义为M：τ，那么e∈[[σ]可定义为proj[M/x]。如[4]所示，可定义的撤回被用来显示语言的无名称片段的普遍性命题5.1普适性在每一个无名称类型都成立。证据 我们证明了对于某个k，l，Q，每个无名型都是（Bk）l的收缩核我们也有一个可定义的收缩B<$N，通过项x<$x= 0和如果y那么0else 1.引理5.2对于任意k，l，Nmax{k，l}+1我的律师。Wehave（N×Nmax {k，l}）=<$N max {k，l}+1。Q通过反复应用这个引理，我们得到：引理5.3对于任意二阶σ，存在k，l使得σ∈ <$$>（<$Nk× Nl）。引理5.4如果普适性在<$T成立，则普适性在<$（N × T）成立。我的律师。Givenf∈<$（N×T），supposem/∈V（f）=i1， . . ，in. LetMf=λ（x，→y）.Ifx= i1th enMλe. f（i1，e）n→yn. . Ifx= inth enMλe. f（in，e）n→y∈elseMλe. f（m，e）[x/m]→y则nifj∈ν（f），[M]]（j，e）=[Mf （j）]]（e）=f（j，e），且ndifj/∈ν（f），[M]]（j，e）=需要[[Mf（m）[j/m]]（e）=[mParticipatej]（[[Mf（m）]]（e））=[mParticipatej]（f（m，e））=f（j，e）。Q推论5.5普适性在<$Nk对任意k成立。注意，对于每个g，h∈Nk，g是一个格。此外，它是一个布尔代数：每个元素g∈Nk都有一个补g（定义为g（i）=ig（i）=T）使得gg=且gg=T。注意，每个严格映射f：（Nk）→f是一个布尔同态：如果f（g）=f，则f（g）=T，反之亦然，因为f（g）f（g）=f（gg）=f（T）=T。定义5.6一个元素p∈Nk<$$>是一个准原子，如果它是一个真原子--即p±g<$h蕴涵p±g或p±h--或者是一个文字是一个元素e，使得e或e是一个准原子。Givenikandn<∈N，letpn（i）：Nk≠λ（→x）. Ifxi=nth enTelsen. Giveni，（Nk × <$N l）的类型的近似的有限链的可定义性，并使用可定义的收缩和引理5.4将其推广到所有三阶类型。一个这种类型的（非常量）函数f首先用一个新的显式名称的k元组测试它的参数，并接收一个新的显式名称的l元组作为返回，它可以从中构造第二个名称的k元组，等等。因此，为了构造f的近似项的定义链，我们连续地提取这些k和l元组的表示，同时跟踪引入的名称。通过我们在前一节中的结果，我们可以认为严格函数f∈（Nk）表示一个“广义”的k元组的名字，每个名字可以是具体的-即f（p n（i））= T，如果第i个名字是n -或新鲜的因此，给定一组“已知名称”S，f ∈（Nk）λ κ，且a k - t up le of f n ames → a ∈ Nk，我们可以定义一个检验“等价到S“，当f不能从λκ中区分时，该检验基本上成立。κ→abyanobererh onon定义预处理的EqS（f，→a），以便对所有i≤k进行优化：• (i)fpn（i）=T蕴涵ai=n• (ii)若fpn（i）=n，则ai/∈S• (iii)对所有j≤k，fp（i，j）=T当且仅当ai=aj引理6. 1如果fν（d）≠S且方程S（fi→a），则nfd=d→a。证据对于 准原子 d ， 证明这 一点是 足够 的。 如果 d = pn （ i） ，则f（ d）=Timpliesai=nanddhenced（→a）=Tbydefinition（i）。如果f（d）=n，则f（pm（i））=Tforsom/=n-，其中ai=mandsod（→a）=n-orelsef（pm（i））=n，对于所有m∈N，因此通过（ii），ai/∈S，因此ai/∈ν（d），因此ain和d（→a）=areuired。 Ifd=p（x，y）thenf（d）=d（→a）by定义（iii）.Q设元素e∈（Nk×（Nl ∞））∞是参数的，如果e/∈ {T，∞}且对 于 eachchprimepn（i）eihe∞→a，d∞=e（π·→a）pn（i）forall→a∈Nk且d∈πG，或e（→a）pn（i） =e（π·→a）pπ（n）（i）forall→a∈Nk且d∈πG. 该parametricement表示一个广义的l-元组的名称，其中每一个是一个具体的名称，一个新的名称，或一些一个。给定f∈（（Nk×（Nl））和e∈（Nk×（Nl）），我们现在定义一系列在f和e之间传递的名称元组，从而定义一系列e的“显露片段”的近似给定 布尔 值 b1，.，bk， 和 姓名n1，.，nk+1， letcase [b1›→J. Laird/Electronic Notes in Theoretical Computer Science 173（2007）203217FFFFFn1，.，bk ›→ nk，nk+1] =ni，其中i是使得bi的最小值 =tt，或case [b1<$→n1，... bk <$→nk，nk+1] = nk+1，如果每个bi= n。对于每个i∈ω，我们定义：• 一组“启示的以及到目前为止在交互期间由e• f在第i步交互时提供的广义k元组名称; Φi（e）：（Nk）• 由e返回的名称的（参数化的）广义l-元组，i（e）：（Nk×（Nl（））。• a“重构”Γ i（e，d，S）：（N k ×（N l），关于一组名称S，它测试它的输入是否与已经由f提供的元组相等（直到S），并返回观察到已经由e提供的相应l-元组，否则表现为d。这些定义如下：U0（e）=ν（f）和Γ0（e，d，S）=df fΦi+1（e）=λh.f（Γi（e，（λ（a，b）.h（a）），Ui（e）.f f fi+1（e）=λ（→x，y）. Φf（e）λ→z。ez，→λw→. 你好1.. . tl，wheretj=case[（z1=wj<$wj/∈fi+1S ›→ x1），. （zk= wj<$wj/∈ S <$→ xk），wj].Ui+1（e）=Ui（e）v（Γi+1（e，Ui（e））ffffΓi+1（e，d，S）=λ（→x，h）. 如果方程S（Φi（e，S），→x）th en<$i（e）<$i→x，h<$elseri（e，d，S）<$i→x，h<$.ff f f现在我们用引理6.1证明以下事实。引理6.2如果ν（e）<$ν（f）<$S，则对于所有i∈ω，下列成立：• IfE qS（Φi+1（e），a1， . . ak）n<$i+1（e）<$i→a，q<$i=e <$i→a，q<$i.f f• 如果Γ i（e，T，S）± e ± Γ i（e，T，S）.f f• Φ n+1（e）/∈ {T，n}表示Φ i（e）/= Φ n+1（e）.f f f• 对于每个n，要么<$n+1（e）∈ {T，<$N}，要么Γ n（e，<$N，S）<$Γ n+1（e，<$N，S）。fff引理6.3给定一个无限长链，有界支集e1± e2±... ∈（Nk×（Nl））n存在m使得em= en，对所有n≥ m。证据 在K上的归纳。 对于基本情况，我们注意到，如果e±EJ∈（Nl<$$>）<$则e=T或e=eJ或eJ=T。对于归纳法的情况，假设我们有一个链e1±e2±. ∈N）），有界支撑S.则对每个i ∈ S，存在mi，其中emi（i）= en（i），对所有n ≥ mi. 此外，存在mJ使得对于所有j/∈ S，我们有emJ（j）= en（j）对于所有n ≥ mJ。 所以我们可以取m = max（{mJ}<${mi|i ∈ S}）。Q命题6.4对所有f，e，存在n使得Φ n（e）∈{T，n}。证据 设S = ν（f）<$ν（e）. 则如果
我的内容管理
展开
