amb算子的指称属性及其失败

理论计算机科学电子笔记173（2007）221-239www.elsevier.com/locate/entcsAmb破坏了良好的指向性，Ground Amb保罗·布莱恩·利维1伯明翰大学，伯明翰B15 2TT，英国摘要麦卡锡的amb算子没有已知的指称语义，它的基本运算性质-上下文引理，细化相似性和凸双相似性的兼容性-长期以来一直是开放的。在本文中，我们给出了一个单一的例子程序，演示了这些属性的失败。 这表明不可能有任何指向良好的指称语义。然而，我们表明，如果琥珀色是在地面类型只，那么所有这些业务性质举行。关键词：McCarthy's amb，应用模拟，Howe方法，定点，CIU定理，上下文引理1介绍1.1的问题McCarthy这不同于普通的（不稳定的）非决定性MHMJ，如果M或MJ可以发散，则可以发散尽管它表面上很简单，一直是语义学研究的一个尴尬。它拒绝了指称建模和令人满意的操作处理，导致两个重大的开放问题[6]。第一个问题来自应用互模拟的概念，在[1]中在非类型化设置中引入，后来在类型化设置中研究[3]。应用双相似性被巧妙的方法证明是一个一致性[5]。这种方法在确定性和不确定性环境下都有效，但如[8]中所解释的，它在存在amb的情况下不起作用。因此，在存在amb的情况下，应用性双相似性是否是全等仍然是一个问题。1电子邮件地址：pbl@cs.bham.ac.uk1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.02.036222P.B. Levy/Electronic Notes in Theoretical Computer Science 173（2007）221第二个问题是上下文等价，我们把趋同和趋异都在非确定性设置中，这被认为比应用互模拟更粗糙。上下文引理指出，两项M和MJ在任何环境中（即，在任何关闭替换）必须在上下文上等效。这在[5，6]中在不稳定的非确定性设置中显示，但它是否在amb存在的情况下保持开放。在本文中，我们给出了一个例子，同时回答这些问题和一些变体使用前序，而不是等价关系的否定。我们给出了两个在任何环境下都必须重新计算的程序M和MJ被视为等价的，即使我们使用应用性双相似性的更精细的关系另一方面，存在上下文C[·]，使得C[M]可以发散而C[MJ]不能。这表明，在设定amb时，不可能将一个术语作为一个从环境到行为的函数。没有指称语义学建立在这样的原则可以工作。为了公式化这个例子，我们需要在非接地类型上使用amb。在一个只给amb提供基类型的微积分中，我们将证明，这些开放性问题可以得到一个相对的回答。本文的结构如下。在第2节中，我们使用一个小的按名称调用（CBN）演算来描述我们的结果，没有函数类型。这使得示例程序易于理解。然后，在第3-注1.1我们的示例程序适用于类型化演算（可能包括递归类型）。这与[7]相反，其中研究了带有amb的无类型懒惰λ-演算对于这个演算，我们的例子不起作用（除非添加了排序），开放的问题仍然是开放的。2小型按名称调用演算2.1的问题在本节中，我们考虑一个具有基类型和一元和类型的按名称调用演算，如图1我们将一元和类型构造函数写成L，将pm写成“pattern-match”的缩写。我们把rec x写成diverge。X.如图2所示的操作语义遵循[16]的公式。对于每个类型A，我们定义一个集合[A]如下：[bool]=P{true，false，false}[1]=P{T，N}[LA]= P（{upB|B∈ [A]}<${<$}）(We可以选择从幂集中排除空集，但这并不实质上改变我们的论点。）对于每个闭项M：A，我们通过A上的归纳来定义它的运算意义[M]∈[A]：P.B. Levy/Electronic Notes in Theoretical Computer Science 173（2007）221223类型A：：=bool|1 |LA方面r，x：AM：AΓx：A（x：A）∈Γrec x.M：ArM：ArMJ：AMHMJ：ArM：ArMJ：AΓMambMJ：A顶部：1ΓM：1ΓN：BrM;N：BM：AT-100M：LArM：LAr，x：AN：Br = pmM作为上x。 N：BFig. 1. Call-By-Name语言def• 如果M：bool，则[M]={true |M true}{false |M false}{|M}def• 如果M：1，则[M]={top|Mtop}{|M}def• 如果M：LA，则[M]={up [N] |MupN}{|M}。当[M]=[MJ]时，我们称两项M，MJ：A是凸双相似的如果A是一个基类型，我们说它们在行为上是等价的。凸双相似性是鲁棒的，因为下面的结果，其证明，我们推迟节。3 .第三章。命题2.1如果闭项M，MJ：A是凸双相似的，则C[M]和C [M J]对于任何类型的任何上下文C[·]是凸双相似的，具有类型A的洞。假设我们希望精确地识别闭基项，当它们在语义上等价时。如[9]中所解释的，不能使用diverge≤true的域语义。因为那时真H发散≤真H真=真但是，如果amb是单调的，我们也有true=if（falseambdiverge）then diverge else true≤if（falseambtrue）then diverge else true=真H发散因此，真H diverge=true，与行为等价性相矛盾。因此，在任何非决定论的域语义中，要么真H diverge和真被识别（如Hoare事实上，没有指称模型的地面行为等效这种演算是已知的。我们说两个开项Γ<$M，MJ：B是224P.B. Levy/Electronic Notes in Theoretical Computer Science 173（2007）221以下封闭式术语为终止术语T：：=真|虚假|顶部|向上M收敛关系MT-归纳定义MTMHMJTMJTMHMJTM[rec x.M/x] ΔTrec x. MTMTMambMjMJTMambMjMtrueNTifMthen thenNelseNJT真的假的假的MfalseNjTifMthen thenNelseNJT顶部顶部MtopNTM;NT上M下MMupP N[P/x]pm M为上x。NT发散谓词M-共归纳定义MMjMMHM jMHM jifMthenN elseN jM[rec x.M/x]MMjM true Nrec x. MMMambM jM top NifMthen thenN elseN jM falseN jM;NM;NifMthen thenN elseN jMP N[P/x] Npm M为上x。Npm M为上x。N图二. 按名称调用演算P.B. Levy/Electronic Notes in Theoretical Computer Science 173（2007）221225JJ−−→J−−→(i) 当M[N/x]和M[N/x]是双相似的，−−→每个Γ-环境N/x(ii) 当C[M]和C[MJ]对于每个具有位于ΓB的洞的背景C[·]在行为上等价−−→J−−→(iii) CI equivalent−−→对于每一个Γ-环境N/x，都是观测等价的。[6]中的两个公开问题，在一个丰富的设置中用函数类型和递归类型来陈述，如下所示。(i) 凸应用双相似是同余吗(ii) CI对等是否意味着语境对等？ （这样的结果被称为a上下文引理或CI定理。）这些问题也有使用前序而不是等价关系的变体。在不稳定选择的背景下，所有这些问题都得到了积极的回答[5，6，12]。但似乎不可能将这些技术应用于amb[8]。因此，问题仍然是开放的。2.2反例我们现在将给出一个例子来否定地回答这两个问题（以及前序变量）。定义项x：L1<$M，MJ：L1如下。defM =（up top）amb（pm x as up z. up（top H z））J定义M= up（top H pm（x amb up top）as up y. 年）的defM=MHM对于任何闭项M [N/x]：L1，项M[N/x]和MJJ[N/x]在行为上是等价的。(This是真的，即使我们在每个类型上引入一个常数来表示空集。• 两者都不能分开。• 两者都能够返回P，对于某些P使得P

但P/

。• 两者都不能返回到P，对于某些P使得P/P上。• 两者都能够向上返回P，对于某个P，使得P> top，而P> top，精确地说，如果N能够向上返回Q，对于某个Q，使得Q> top。因此M和MJJ是凸应用双相似的。因此，根据Prop.2.1，它们也是CI等价物。但它们在上下文中并不等同;例如，它们可以通过上下文defC[·]= pm（up top amb（rec x. [·]））向上。 u：1我们首先注意到，(i) 如果rec x.M等于N，那么通过求值归纳，我们有N=（top H）ntop，因此N不能发散J226P.B. Levy/Electronic Notes in Theoretical Computer Science 173（2007）221(ii) rec x.MJJ通过选择右边的选项，向上（顶部H C[MJJ]）(i) 得到C[M]/π。为了证明C [MJ] n，我们始终选择右边的选项。形式上，我们有{CMJJ， top H CMJJ} ±通过简单的coinduction，使用（ii）。这个例子排除了任何指向明确的指称语义，即术语的语义是环境的函数。 在操作上，M和MJJ描述[L1]上的相同内函数f，将C映射到{上{T}，上{T，上}}，如果D∈ [1]。（∈DupD∈C），以及{up{T}}其他-睿的但f有两个定点，即{up{T}}和{up{T}，up{T，}。运算论证告诉我们，[rec x.M]是前者，[rec x.MJJ]是后者。所以没有正确的方法来计算递归定点。（参见定点[13]中的例子2.3使用使用是一种特殊的背景语境，可以应用于封闭术语。• bool的使用是一个基础上下文，如果[·]则NelseNJ。• 使用1是一个背景语境[·];N.• LA的使用是作为up x的基础上下文pm[·]。 N.当C[M]和C[M]J对A的每一个使用C[·]都是等价的时，两个闭项<$M，MJ：A是使用等价的.更一般地说，两个开放条款J−−→J−−→rM，M：A是CIU等价的，当C[M[V/x]]和C[M[V/x]]在行为上−−→等价于A的每个Γ-环境V/x和每个使用C[·]。一个使用定理指出，使用等价意味着上下文等价。CIU定理是CI定理和使用定理的结合，说明CIU等价蕴涵上下文等价。这个定理（和前序变量）在确定性[18]和不确定性[6]的情况下都成立与CI定理一样，uses定理在amb存在的情况下失败。为了看到这一点，定义项M，MJ：L1如下：defM=向上发散HJ定义M=MH向上（顶部H发散）现在对于任何基项x：1<$N：C，项M到x.N和MJ到x.N都发散。此外，它们收敛于相同的事物，因为M和MJ“可能在上下文上所以M和MJ是等价的。但它们在上下文中并不等同;例如，它们可以通过C[·] =pm（[·]amb up top）作为x。X ：1个C[MJ]可以发散，而C[M]不能。P.B. Levy/Electronic Notes in Theoretical Computer Science 173（2007）2212272.4接地Amb在第1.1-如果我们只允许地面型的琥珀色，那么所有的问题都可以得到一个合理的回答。我们在Sect中证明了这一点。四、2.5强发散和弱发散正如[17]中所建议的，如果我们关心分支时间行为，区分不同类型的发散可能是合理的。当一个术语出现分歧时，• 始终保持一致，或• 最终的情况是，只有发散是可能的。这两种发散分别称为弱发散和强发散。例如，程序Pn选择n+ 1个布尔值。如果它们如果它们选择n+ 3个布尔值。 如果它们.. .可以弱发散，但不能强发散。C[MJJ]也是如此。我们声称M[N/x]和MJJ[N/x]对任何即使我们区分了这些类型的分歧，N仍然成立。 而且似乎很可能，Prop.2.1可以适用于更精细的互模拟概念，从而做出这种区分。因此，这种区别并没有破坏我们的榜样。为了将带有amb的λ-演算编码到π-演算中，[2]更进一步：不仅区分强发散和弱发散，而且完全忽略弱发散。我们的例子不适用，因为C[MJJ]不能分歧很大。注2.2如果我们把布尔选择看作概率的，0。5的概率为真，则程序Pn以大于>1−2−n的概率发散，如果n很大，则接近1似乎很难证明忽视这种差异是合理的，如果我们首先关心的是分歧。3按值调用演算对于本文中的操作技术，使用按值调用是最简单的它们可以适应按推值调用，因此也可以适应按名称调用，但代价是有些复杂。我们的演算类型如下：余电感定义A：：=i∈IAi|1|A×A|A→A228P.B. Levy/Electronic Notes in Theoretical Computer Science 173（2007）221其中I在可数集上的范围。我们使类型语法共归纳，以便我们得到等递归类型（即相等μx.A=A[μX.A/X]而不仅仅是同构）。我们共归纳地定义基类型为：C：： =i∈ICi|1|C×C我们省略了1的规则，因为它们与×的规则类似。我们使用细粒度的按值调用演算2，它显式地将值与普通项区分开来。因此有两个判断：Γ<$M：B表示M是B型项，而Γ<$vV：B表示V是B型值。语法在图中归纳定义。3 .第三章。r，x：A，rJvx：AV：AΓ，x：A<$M：B令V为x。M：BV：A返回V：ArM：Ar，x：A<$N：BrM到x。N：BΓvV：AΓvVJ：AJΓvV，Vj：A×AJrvV：A×AJr，x：A，y：AJ<$M：BV = x，y = y。M：BvV：AvV：AiΓ，x：Ai<$Mi：B（<$i∈I）Γ►v⟨ˆı,V⟩:i∈IAiˆı∈Ii∈I当{i，x <$.Mi}i∈I：B时，Γ，f：A→B，x：A<$M：BΓvrec fλx.M：A→BΓvV：A→B关于VW：BΓ<$Mi：B（Mi∈I）Γ<$choosei∈I.Mi：BΓ<$Mi：B（<$i∈I）Γ<$ambi∈I.Mi：B图三. 具有可数不确定性的图中给出了操作语义四、而不是定义归纳，我们定义它的补充归纳。这显然是等价的，但使推理更容易。注3.1我们可以用与我们的CBV演算完全相同的方法来处理第2节的CBN演算。事实上，前者是后者通过标准的thunking变换的片段[4]，将LA翻译为1→A。但这仅仅是因为CBN演算缺少函数类型。2 与类似的演算，如莫吉的一元语言[ 15 ]的比较P.B. Levy/Electronic Notes in Theoretical Computer Science 173（2007）221229如果我们希望包含CBN函数类型，或者更一般地，使用按推值调用[10]，我们将需要其他技术。由于这不是amb特有的，我们在本文中不处理它归纳定义（Inductive definition）M[W/x]mV设W为x。MVM[recfλx. M/f，W/x]100V（rec fλx.M）WVreturnVM<$WN[W/x]<$V M至x。NV[W/x]V下午10时，Was{i，x.M}ˆı∈I1995年M[W/x，WJ/y]下午10点，WJ as x，y。MVi i∈IMV∈Ichoosei∈IMi <$VMV∈Iambi∈IMiV必须收敛（归纳定义）returnVQMQW（MWN[W/x]Q）M到X。NQM[W/x]Ω设W为x。MQM[recfλx. 男/女，女/男]（rec fλx.M）WQ[W/x]X/Q下午10时，Was{i，x.M}ˆı∈I⇓M[W/x，WJ/y]下午10点，WJ as x，y。Mi i∈IQQMQ∈Ichoosei∈IMi<$QMi<$Q（<$i∈I）ˆı∈Iambi∈IMi <$Q见图4。 细粒度CBV定义3.2（i）一个闭关系R将一个关于存在于其上的闭项的二元关系和一个关于存在于其上的闭值的二元关系与每个类型A相关联(ii) 一个开关系R把每个rA与一个关于它所包含的项的二元关系联系起来，把每个值rv A与一个二元关系联系起来230P.B. Levy/Electronic Notes in Theoretical Computer Science 173（2007）221对于存在于其中的值，使得如果Γ<$MRMJ：B且Γ <$ΓJ，则ΓJ<$MRMJ：B，对于值也是如此。P.B. Levy/Electronic Notes in Theoretical Computer Science 173（2007）221231wSCwSCEURR(iii) 我们将项和值上的恒等关系写成id，将恒等关系限定为标识符的恒等关系写成idf(iv) 我们把E写为关于术语和价值的普遍关系（将一切与一切联系起来）。(v) 对于关系组合，我们按图解顺序写;(vi) 我们把R的自反传递闭包记为R的自反传递闭包。(vii) 如果R是一个开关系，我们写R0为限制R的封闭项和封闭值。(viii) 设R是一个闭关系。 我们定义R（R的开扩张）为−−→−−→当M[V/x]RN[V/x]为−−→从Γ到空上下文的任何替换V /x(ix) 设R是一个闭关系。我们定义Rw（R的弱化扩张）为当M和N都是闭的且M R N时，联系两个项ΓM，N：B的开关系。定义3.3（i）设R和S是开关系。我们定义R[S]（S到R的替换）为由项对组成的开关系，−−→−−→对于每对项Γ<$ M，N：B和每对项Γ<$M，N：B，−−→−−→置换ΓV /xΔ和ΓW/xΔ，使得MRN和VSWx 为每个（x：A）∈Γ.(ii)当idf≠ S且S[S] ≠S时，开关系S是置换的。定义3.4设R是一个开关系。(i) 定义R^（对R的可实现的定义）以满足操作相关性当θ=φ（因此I=J）时，将两项θ {Mi} i ∈ I和φ { N j } j ∈ J联系起来，MiRNi，对于每个i∈I。(ii) 当S^ ≠ S时，S是相容的。(iii) 我们定义R的置换相容闭包为包含R的最小置换相容关系。引理3.5设R是闭关系。 则RwSC^wSCRw^你好 因此R0RR0.证据RwSC=R w[R wSC^[[英]Rw^[E] EURRRw^wSCQ对于一个备份操作系统，下面的文件将很有用。定义3. 6如果R是一个不相关的关系，我们定义R`tobh封闭的相关关系，• 设V为x.M，使VJ为x。其中VRVJ和MRMJXwSCwSC232P.B. Levy/Electronic Notes in Theoretical Computer Science 173（2007）221我我• 返回V到返回VJ，其中VRVJ• M0到x。 M1到MJ到x. 其中M0R MJ和M1R MJ0 1 0 1• pm =V0，V1= x，y = 0. M到pm =VJ，VJ= x，y = x，y。其中V0RVJ和V1RVJ0 1 0 1和MRMJ• pm，Vas{i，x. Mi}i∈Itoo pm，VJ为{i，x. MJ}i∈I，其中VRVJ和dMiRMJ对于每个i∈I• （rec fλx.M）V到（rec fλx.MJ）VJ，其中MRMJ和VRVJ• 选择i∈I。 选择i∈I。 MJ，其中M iR MJ，对于每个i ∈ I我我•ambi∈I. M ito ambi∈I. MJ，其中M iRMJ，对于每个i∈ I。我我定义3.7设R是一个闭关系。(i) R尊重元组，当• ⟨ˆı,V⟩R⟨ˆıJ, VJ⟩:Σi∈IAiimpliesˆı=ˆıJandVRVJ:Aˆı,• V0，V1<$R<$VJ，VJ<$：A0×A1意味着V0RVJ：A0和V1RVJ：A1。0 1 0 1(ii) 当V R VJ：A→B对每个闭值W：A蕴涵V W R VJW：B时，R尊重函数(iii) 我们说，R是一个较低的应用模拟时，它尊重元组和功能，和M R MJ和M<$V意味着MJ<$V j的一些VJ，使V R VJ。此外，如果M R MJ和M蕴涵Mj，则R是一个低+发散的应用模拟。(iv) 我们说，R是一个较低的（resp。低+发散）应用互模拟op当R和R都较低时（分别为发散）模拟。(v) 当R是一个低+发散模拟和低互模拟时，我们说较低+发散模拟的对偶称为细化模拟在[6]中。我们将较低的应用相似性定义为最大的较低的应用模拟，其他类型的模拟也是如此定义上下文等价（和不等价）而不正式定义上下文是很方便的。定义3.8设R是一个闭关系。• R是may-preadequate当，如果M R MJ：A，其中A是基类型，且M∈n然后是M.当R和Rop都是may预适当时，它是may-适当的• R是预适的，当它是预适的，如果M R MJ：A，其中A是基类型，并且M，则Mj。当R和Rop都是预充分时，它是充分的定义3.9设Γ∈M，MJ：A为项。记R（M，MJ）为只与ΓJ<$M相关的开关系的替换相容闭包，MJ：A为ΓJ<$ Γ。我们说• 当R（M，MJ）0是可预充的时，M±OMJP.B. Levy/Electronic Notes in Theoretical Computer Science 173（2007）2212330000000• 当R（M，MJ） 可能是足够的• M±<$MJ当R（M，MJ）已经足够了• M<$MJ当R（M，MJ） 足够了。定义3.10（i）设M，MJ：A为闭项。 我们说M±<$UMJ，当对于任何基类型C和项z：A<$P：C，M到z的行为（值或散度）。 P包含在MJ到z的行为中。P.(ii)设V，VJ：A为闭值。 我们说V±<$UVJ，当对于任何基类型B和项z：A<$P：B，P[V/z]的行为（值或发散）包含在PJ[V/z]的行为中时。很明显，语境不平等±包含在±U中。我们在一般amb的设定中的唯一任务是证明Prop。2.1，或者更确切地说，在我们的CBV设定中的相应陈述。定义3.11一个封闭关系R被称为基于函数，当V R VJ：A→B意味着A是一个接地类型。命题3.12（i）设R是一个基于函数的低+发散应用模拟。 则RwSC0是较低+发散的应用模拟。(ii)设R是基于函数的低+发散应用互模拟。则RwSC0是较低+发散的应用互模拟。证据(i) 显然，RwSC0尊重函数，并且很容易证明它尊重元组。因此，如果WRwSCWJ：A并且A是接地类型，则W=WJ。这是通过对W的归纳得出的。我们不知道如何让RwSC0Rw`SC。Sup pposeMRwSC0MJ.By引理3.5，或者M R MJ^或M RM. J. 在后一种情况下，我们表明，通过酶解，可获得MRMJ或MRw`SCMJ。• 设M=（rec fλx.M0）W和MJ=（rec fλx.MJ）WJ，recfλx.M0RwSCrec fλx.M J和W RwSCW J。根据引理3.5，· M0RwSCMJ，在这种情况下，我们完成了，或者· rec fλx.M0Rrec fλx.MJ，在这种情况下W具有基类型，因此W=WJ第一段。 因此，M R MJ，因为R尊重函数。• 其他情况是微不足道的，使用RwSC尊重元组的事实接下来我们证明RwSC0是一个较低的应用模拟。我们需要证明，如果M<$V和MRwSC0MJ，则存在VJ使得MJ<$VJ和VRwSC0VJ。我们通过MV上的归纳来做这件事。当M R MJ是初始的情况下，S_（？）我们省略了细节，这是直截了当的。接下来我们证明，如果MJ<$Q和MRwSCMJ，则M<$Q;我们通过对MJ<$Q的归纳来做到这一点。M R MJ是平凡的，所以我们假设MRw`SCMJ。wSC234P.B. Levy/Electronic Notes in Theoretical Computer Science 173（2007）2210010000• 设M = M0到x. M1和MJ= MJ到x MJ和M0RwSCMJ和M1RwSCMJ.那么MJ也就是M0，如果M0 W，那么，1 0由于RwSC0是较低的模拟，因此存在WJ，使得MJJ和WRwSCWJ，我们有MJ[WJ/x]<$Q。由于M1[W/x]RwSCMJ[WJ/x]，我们1 1通过归纳假设，使M1[W/x] ≠Q因此，M0到x。M1，Q。(ii) 的推论（一）。Q4接地Amb4.1旨在我们的目标是证明以下结果。命题4.1当我们将amb的使用限制为接地类型时，(i) 分歧应用相似是一个替代的预一致(ii) 发散应用倍半相似是一个替代的预同余(iii) 发散应用双相似性是一个替换同余。(iv)±和±U重合，即 ±10U/SC是预先足够的。4.2分解一个关系以下内容将在以下各节中有用。定义4.2开关系S在闭关系R上分解，当S <$S^;R<$。命题4.3设S是一个在一个闭关系上分解的开关系R. 假设S尊重元组，R尊重函数。 则S0，仅限于项（即不是值），包含在S`; R中。证据假设MS0MJ.由于S在R上分解，存在MJJ，使得MS^MJJ和dMJJR MJ。 我们是用箱子换的。• 假设M=VW且MJJ=VJWJ且VSVJ和WSWJ。则V=rec fλx.M0，因此，通过分解，存在MJJ使得M0SMJ J和recfλx.M JJRV J. 由于R涉及函数，（rec fλx.MJJ）WJRVJWJRMJ。0 0• 在所有这些情况下，MS`MJJ，使用具有S r p ttQ4.3发散相似是一个预同余本节的目的是证明Prop。4.1.定义4.4开关系S如何适合于闭关系R，当• S在R上分解。P.B. Levy/Electronic Notes in Theoretical Computer Science 173（2007）221235000• S具有反应性、替代性和尊重功能性• S;R-硫代氨基甲酸酯命题4.5设R是闭预序，S是R上的开关系.(i) RS(ii) 如果S0<$R（例如，如果（S<$）0<$R），则R<$= S = S<$。(iii) 如果R尊重元组，那么S也尊重元组。证据(i) R=id;RS;RS(ii) 对于任何开关系S，我们有S S[id]。在我们的例子中，由于S是自反的，代入式，我们有SR。(iii) Sup posepuzzle，VS0J， VJ. 该rex是VJJ，因此VS0VJ和d你好，VJjRJ， Vj。 因为Rr es pectsvalu es，所以Vsvj=Vs vJ，并且v jvVJ。产品类型也是如此。Q定义4.6一个封闭关系R是一个上模拟，当它涉及值和元组时，M R MJ和MVJ。（MJVJV。（MVVR VJ））命题4.7设S是一个开关系，它如何适合于一个闭关系R关于函数和元组。(i) 如果R是一个较低的模拟，那么S0也是，因此S也是。op(ii) 若R是上模拟，S0是may-preadequate，则 S0是上模拟模拟，因此是S。证据S通过定义尊重函数，通过Prop.4.5（iii）尊重元组。第4.3节适用(i) 假设R是一个较低的模拟。 我们必须证明MS0MJ和M<$V对某个VJJ意味着MJ<$Vjj使得VS0VJJ。我们用MV进行归纳。这是标准的。(ii) 假设R是上模拟。我们必须证明MS0MJ和MVJ。（MJVJV。（M<$V<$V RVJ））我们通过M<$Q上的归纳法证明了这一点。我们现在知道，存在MJj，因此MS`MJj和MJJR MJ。设M=ambi∈IMi和MJJ=ambi∈IMJ和MiSMJ，对所有i∈I。我我这是一个新的表达式，它是一个新的表达式，它是一个新的表达式。 SoMjQ，soMJQ，soMjQ. IfMJn，then，sinceMSˆıMJ和Sop0我们知道，nSn。0 是可能的，我们有Mn，否则，我们继续如下。 我们首先展示M JJQV JJ。（MjjVjj1995年（MVVR VJJ））以如下方式。236P.B. Levy/Electronic Notes in Theoretical Computer Science 173（2007）2210100101100• 设M = M0到x. M1和MJJ= MJ到x MJ和M0SMJ和M1SMJ. 我们有M0Q，所以MjQ。如果MJ，则由归纳10 0假设存在W使得M0≠W且WSWJ。 所以M1[W/x]=Q，而M1[W/x]SMJ[WJx]，所以MJ[WJ/x]<$Q。如果MJ1到x MJ1则存在WJ使得MJJ和MJ[W J/x]<$V JJ. 则存在W使得M0≠W且WSWJ.以来M1[W/x] SMj[WJX]，存在V使得M1 [W/x]<$V且VSVjj。• 其他案件也是类似的。因此：• MJQ，根据需要• 如果MJ<$VJ，则存在VJJ，使得MJJ<$VJJ和VJJRVJ，因此存在V，使得M<$V和VSVJJ，因此VSVJ，根据需要Q命题4.8设R是闭关系。 则存在关系R→和R←这样，• R→是Howe-suitable环• R←op在Rop• R→=R←• R→R←是相容的。证据 参见[12]。 对于有限语法，可以使用标准的Howe扩展来R→和R←的对偶构造。Q为了证明Prop.4.1（i），设R为发散相似性。则R→在一个较低的模拟（即R）上是Howe-suitable的，所以R→0是一个较低的模拟，因此可能是- preadequate的。因此，R←0，因为它包含在一个预适关系中（即R← 0），是可能--已经足够了。R←操作在上仿真Rop上是、 R←0 可─奥普什所以R←0是一个上模拟。由于R→ R既是一个较低的模拟，又是一个较高的模拟的对立面，所以它是一个发散模拟，因此包含在R中。根据命题4.5（ii），我们有R=R→=R→。因此R←R←=R所以R←=R。 所以R<$=R→<$R←，这是相容的。4.1（ii）-（iii）的证明4.4CIU定理本节的目的是证明Prop。4.1㈣.定义4.9封闭关系R在排序是封闭的，当• V R VJ：A对任何项x：A蕴涵P[V/x]RP[VJ/x]<$P：B• M R MJ：B蕴涵M到x。P R MJ到x。P对于任何项x：A<$P：B。显然，在测序下，±NIU是封闭的。P.B. Levy/Electronic Notes in Theoretical Computer Science 173（2007）22123701001命题4.10设R是闭前序。 然后RSC在R上分解。证据 [6]Q定义4.11设S是一个闭关系，A是一个类型，V，VJ是集合类型A的封闭值。我们称VSQVJ，当<$VJ∈ VJ时。V∈ V。VS VJ.定义4.12设A是一个型，N是A型的闭项。(i) 对于闭值W：A，当对于每个基项，z：AP：i∈I1，如果P [W/z] n，则N到z。潘(ii) 对于A型闭值的集合W，我们称W ±QN，当对于每个基，术语z：AP：i∈I1，如果P[W/z]<$Q，对所有W∈W，则N到Z我是PQn。（N到Z。P<$n<$<$W∈ W。P [W/z] n）命题4.13（i）W ±QN蕴涵N <$Q。(ii)如果N≠Q，则{W|N <$QW} ±QN证据小 事 一桩。Q定义4.14当M R MJ：C时，闭关系R是必预适的，其中B是一个基类型，而M n。（MJnMn）.命题4.15设R是一个闭的前序，在排序下是闭的。让S是在R上分解的置换开关系。(i) S0S`; R.(ii) 假设R是may-preadequate。 若M ≠ V：A且MS0Mj，则存在一个闭值VJ：A使得VS0Vj且VJ±0Mjop(iii) 假设R是必须预适的。假设S0是may-preadequate，对于每个闭基值n。 如果M ≠Q且M S0M J，则存在A型闭值的集合VJ，使得{V|M <$V}SQVJ和VJ±QM J。证据(i) 设pm =V，W= x，y =。MS0N。则存在VJ，WJ，MJ使得V，W，S，V，J，M， M JRN。 则存在VJJ和WJJ使得VSVJJ和WSWJJ和<$VJJ，WJJ<$R<$V J，WJ<$。然后，由于R在排序下是封闭的，我们有下午10点，V JJ，W JJ和X，Y， M JR pmV J，W j as x，y.M JRN（rec fλx.M）VS0N的情形与Prop.四点三• 所有其他情况都与这些类似或微不足道。(ii) 我们用MV进行归纳。我们知道存在MJj使得MS`MJJ和dMJJR MJ。我们如何将该表达式表示为一个封闭的值VJ：A表示VSVJ和VJ±oMJ，如下所示。• 设M = M0到x. M1和MJJ= MJ到x MJ和M0SMJ和M1S M J. 我们有M0W和M1[W/x]V。根据归纳假设，238P.B. Levy/Electronic Notes in Theoretical Computer Science 173（2007）2211110100001010001W，W1W，W1W，WJ1存在WJ使得WSWJ和WJ±oMJ。因此，M1[W/x]SMJ[WJ/x]。通过0 1归纳假设，存在VJ使得VSVJ和VJ±oMJ[WJ/x]。我们需要VJ±oMJΣ0 到x M.J.J J J给定z：A<$P：i∈I1，设P [V /z]<$n. 然后M1[W /x]到z。潘所以M0到x. （J到Z。xP）n. So（MJ到x MJ）到z。潘• 其他案件也是如此。然后利用R的may-预充性推出VJ±OMJ。(iii) 我们通过归纳法对M_∞Q进行研究。我们知道存在MJJ使得MS`MJJ和d MJJR MJ。设M=ambi∈IMi和MJJ=ambi∈IMJ和MiSMJ，对所有i∈I。然后我我则存在一个MQ。通过诱导，我们发现了这些问题和问题。4.13（一）MJ<$Q，所以ambi∈IMJ<$Q，所以MJ<$Q。 设VJ为{n |M j n}. 通过Prop。4.13㈡拉吉吉我们有VJ±QMJ。要显示{n|Mn}SQVJ，我们推理如下。若n∈ VJ，则MJ<$n;由于MSMJ和Sop是may-preadequate，M<$n，且nSn由假设。否则，我们继续如下。我们首先证明存在A型闭值集VJ，使得{V| M<$V}SQVJ和VJ±QMJJ，遵循的方式。•假设M=返回W，并且MJJ=返回WJ和WSWJ。德费恩VJ是{WJ}，所以{V|MV}={W}SQVJ。 第4.13（ii）条告诉我们，{WJ} ±Q返回WJ。• 设M = M0到x. M1和MJJ= MJ到x MJ和M0SMJ和M1S M J. 我们有M0<$Q，所以存在WJ，使得{W|MW} SQWJ（一）WJ±QMJ（二）将对（W，WJ）的集合写成L，使得M0 ⇓ W和WJ∈WJ和WSWJ。对于每个（W，WJ）∈L，我们有M1[W/x]SMJ[WJ/x]，M1[W/x]<$Q，所以根据归纳假设，存在一个集合VJJ关闭值使得QJ{V|M1 [W/x] V} S0VW，WJ（3）JW，WJ±QMJ[WJ/x]（4）定义VJ为（W，WJ）∈LW，W，J。QJ J J我们显示{V|M0到x。M1V} S0V 如下 如果V∈ V 那么存在（W，WJ）∈L使得VJ∈ VJJ. 通过（3），存在V，使得M1[W/x]V和VSVJ。 由于M0是W，我们有M0到x. M1V。将VJ±QMJ显示为x。MJ，假设z：AP：1是一个基0 1i∈I项使得P[VJ/z]对所有VJ∈ VJ都<$Q。 将Q定义为MJ到z。xP. 为任何WJ∈WJ，（1）告诉我们存在W使得（W，WJ）∈L，且对于任意VJ∈ VJJ 我们有P [VJ/z]<$Q，所以通过（4）我们有MJ[WJx]到z。帕奎奥，即Q[WJ/x]<$Q。·通过（2），我们有MJ到x。因此，MJ<$Q，并且对于每个VJ，使得MJ<$VVP.B. Levy/Electronic Notes in Theoretical Computer Science 173（2007）2212390 0 0我