环境演算模型研究: 过滤器与流动性

网址：http://www.elsevier.nl/locate/entcs/volume62.html18页移动环境M. 科波湾德扎尼钱卡利尼DipartimentodiInformatica，Univer sita`degliStudidiTorinocorso Svizzera 185，10149 Torino，Italia，{coppo，kanani}@ di.unito.it摘要本文的目的是调查的可能性，发展过滤器模型的结石代表的流动性。我们将为Ambient Calculus的变体定义一个模型。这个模型被证明是完全抽象的上下文对等的概念，考虑到在顶层的环境。1介绍Ambient Calculus[7]是一种计算演算，允许活动进程在站点之间移动并与站点交互，已成功地作为Web模型提出。由于它的兴趣，最近已经开发了一些关于这个或衍生系统的各个基本方面这些研究的主题主要是类型系统（最终证明了各种属性，如安全通信[8]或安全性[6，14，5]），证明系统[9]，抽象解释[16]和流分析[11]。到目前为止，还没有人尝试过定义微积分的外延式模型。定义环境演算模型的一个主要困难是找到一个抽象的对应概念的流动性。一个有前途的工具，克服这一困难似乎是“逻辑”语义的概念，其中域描述的抽象过滤器的逻辑公式表示的性质的条款的演算。演算本身可以提供基本的工具来描述它的语义。在本文中，我们研究的可能性，开发过滤器模型结石代表流动性。我们将定义，特别是，一个模型的一个变种的环境演算。相对于[15]中定义的上下文等价的概念，这个模型是完全抽象的。指称语义学的[1]部分由MURST在'99 TOSCA中提供支持2002年由ElsevierScienceB出版。 V. 操作访问根据C CB Y-NC-N D许可证进行。2程序的逻辑和进程行为的逻辑表征，如Hennessy-Milner逻辑。这种语义可以通过类型赋值系统引入，其中类型由包含关系排序类型是作为表示术语属性的逻辑公式，而类型包含是作为隐含。一个术语的解释对应于所有可以分配给它的类型的过滤器。所有类型过滤器的集合（这是一个域）确定了微积分的指称模型，在这个意义上，一个术语的指称可以以组合的方式给出这种构造在[3]中首次应用，[2]得到λ演算的模型。在同一行中的研究涉及λ-演算的扩展，通过具有并发特征的算子，如[20，4，12，13]。特别是在[4]中，交集型算子被看作是从“可能”的角度表示非确定性选择的基本工具在[18]中，Hennessy基于类型系统和模态逻辑之间的折衷提出了高阶并发过程由此产生的过滤器模型原来是完全抽象的操作语义的基础上的概念测试和在[17]中，对于FACILE语言的核，也证明了类似的结果高阶过程的一个滤波器模型在[10]中使用相同的方法来构建π演算的过滤器模型在本文中，我们考虑一种称为自开放环境演算的语言，它通过增加进程的开放能力来扩展[7]的系统虽然在环境演算中，一个进程只能打开在其同一级别上运行的进程，但在我们的系统中，一个进程也有能力，执行一个新的动作，打开其封闭的环境，将自己提升一个级别so作用与[7]的酸运算密切相关，并且在标准Ambient演算中无法内部表示然而，正如在结论中所指出的，我们的模型也适用于标准的环境演算，但在这种情况下，完整性失败。用于定义模型的类型系统也可以被看作是一个证明系统，用来表示环境和过程属性。具有这些目的的证明系统也由Cardelli和Gordon提出（参见例如[9]）。特别是[9]介绍了一个包括模态算子的证明系统。 文[9]的逻辑语言与我们的逻辑语言有很大的不同，它在表达环境的性质方面更强大，但它不能直接表达“P能够执行开放动作”这样的性质此外，[9]的系统可以表达内涵属性（如P是空过程），因此它不适合作为构建上下文语义模型的基础，其中属性需要具有外延意义。2语言自开放移动环境演算是移动环境演算的扩展[7]。在标准的环境演算中，3AM.≡.||移动能力（环境可以进入和退出其他环境），但打开动作没有对称的对应物。过程P可以打开发生在其相同水平的环境b（即，与b）同时进行，通过行使一项行动，打开b。但是一个进程没有办法打开他运行的环境，把自己提升一个级别。这种行动，允许如此原始，似乎确实合理的分布式环境中，不应该有，至少在最高级别，任何等级结构，然后移动和开放的能力的对称应该是预期的。在本文中，我们只考虑了表示移动性的基本核心语言，特别忽略了用于限制和通信的操作符应可按照[10]的思路介绍这些措施。环境和过程让 是一组由a，b，c... 和 是...的集合 动作，范围为m，n，...，对于所有的环境变量a∈ A，包含in a，out a，open a，so a。过程的集合P（由P，Q，R，.. . ）定义由.P：：=0| M. P| A[P]| P. P|！P.我们假设“。“优先于““。所以mα。β读作（m.α）β。我们将m写成m的缩写。0的情况。通常，结构同余关系被定义为是同余的最小自反、传递和对称关系，并且：.• 满足!P！P. P;• 使经营者。交换的，结合的，0作为零元素。进程的行为由图1中定义的归约关系表示。请注意，so操作允许进程打开其封闭环境。此操作与其他操作（in，out，open）正交，并且不能在标准环境演算中进行内部模拟。注2.1Cardelli和Gordon在[7]中讨论了原始酸，其还原规则是：.a [acid. Q] → P. Q他们拒绝酸，因为它允许电子。将环境捕捉到它永远无法退出的位置例如，过程（v k）[k]。a[in b.acid.in k]]捕获环境b，因为：..（v k）（k [0]. a [in b.acid.in k]）。 b [P] →n（v k）k [b [P]]现在，由于限制（νk），b[P]不能再与环境的其余部分相互作用，特别是不能从k移动。类似地，我们可以使用so来捕获环境b：..（v k）（k [0]. a [in b.so a.in k]）。 b [P] →n（v k）k [b [P]]4⇓→....（红色）a [b]。 Q]。 b [R]→b [a][P. Q]。R]....（红色）a [b][c][d][e] Q]。 R]→a [R]。 b [P. Q]..（红色自开）很快，很快。 Q]→P. Q..（红色打开） 打开AP。 a [Q]→P。 Q..（R − par）P → Q<$P。 R → Q。 R（R−amb）P→Q<$a [P] →a[Q]（R−）PPP→QQQ P→QFig. 1.减少唯一的区别在于，S0需要从内部打开的环境的名称A作为参数。我们认为引入一个合适的类型系统，禁止在限制范围内出现作为so的观察等效性在环境演算中，表示可观测量的自然候选者是环境。下面的观测前序的定义采用了在原始系统中提出的可观测的概念[15]。定义2.2.(i) 我们说过程P表现出环境a，记作Pa如果P[Q]. R对于某些过程Q，R。(ii) P±Q，如果对于所有上下文C[]和环境a： C[P]aC[Q]a.(iii) 如果P±Q和Q±P，则P=Q。备注2.3不适用证明P→Q蕴涵Q±P，但一般P→Q=/Q。 或设P1=opeNa. a[b[0]]和P2=b[0]。 则P1→P2butP1=/P2（记C[]为[−]）。3类型与多态λ演算的类型赋值系统类似，类型被视为无类型对象的属性，而不是对象所在的域。类型旨在提供有关与它们相关联的进程的部分信息我们的类型语言必须有足够的表达能力来完全描述进程行为。我们需要同时考虑环境，动作和平行5∧∧≤−≤ ≤ ≤ ≤≤≤N T..类型构造函数。此外，交叉类型构造函数被添加来表示非确定性。类型的集合T（范围为α，β，γ，.. . ）则定义为：.T：：=ω| M. 不|A [T]|不. 不|T..类型ω表示对所有过程都成立的性质 注意α。 β是类型一个过程可以在两个并行运行的分量中同时显示属性α和β，而α β是一个过程的类型，它可以以不确定的方式显示属性α和β，但通常沿着不同的约化路径。我们假设它的优先级最低。在将类型与进程联系起来时，我们必须考虑两个不同的形式系统。一个是表示类型的逻辑结构，由它们的蕴涵关系（表示）确定，另一个是将类型分配给进程。类型的逻辑结构被形式化为表示蕴涵的偏序关系我们写α β是为了表示性质α包含性质β。 我们写αβ如果αβα。然后是由下式导出的等价关系：.类型蕴涵的形式规则如图2所示。请注意，如备注2.3中所指出的，执行一个动作对应于能力的丧失这是形式化的公理组Rule（out in）考虑到这样一个事实，即在Rule（red in）中，在消耗了ina操作之后，a内的进程总是被允许执行一系列out a，ina操作。规则（in-out）也有类似的动机。交集表示 一个过程。s具有α<$β型，如果它可能表现出性质α和真值。tyβ。 Axiom（. . （2）这一点至关重要。公理.（ω1），（ω2）和规则（cg−. ）暗示，≤α，即平行组合校正-要求提高能力。此外，使用（ω −id），（ω1），（. 1），（cg−. ）的情况下，（ω − ≤），（ω2），我们得到.....α。 β ≤ α。 β α。 β ≤ α。 ω ω。 β ≤ α ≤ β，也就是说，并行的能力类型将始终被视为模≤。 请注意，≤。都被保存了下来与ω的交和平行合成。行动erat。或和，是一种联系。因此，例如，我们可以明确地写α。β。γ。 并联组成类型的交集也被认为是模置换，类型的交集被认为是模置换。南岛d次重复（规则（rules（−id），（−l），（−r））。平行组合α1。..... . 你 好 。 . . αn有时用向量−→α表示符号 类型α1的交集... α n将表示为i∈{1. n}αi. 在在这种情况下，i∈{1. n} αi 表示β<$αi对于某个i∈ {1 ···n}。一个关键的技术概念是正常类型。定义3.1（i）正规类型的集合以如下方式归纳定义：(a) ω∈ N。α。β6α∗∗β αβ.• 的交换性和分配性。........（。1）α。β≤β。 α（. 2）（α. β）。 γ ≤ α。（β. γ）• 关于ω的• 分布性.（ω 1）α ≤ ω （ω 2）α≤α。ω....（[]） a [α <$β] ≤ a [α]<$a [β]（.α. （β <$γ）≤（α. β）β（α. γ）（。m. （α<$β）≤m.α<$m.β• 序列化.......（。 . 1）m.α。 β ≤ m。（α。 β） （. . 2）m.α。n.β ≤ m。（α。n.β）n. （m.α. β）• 减少........（在）a [在b中。β]。b [γ] ≤ b [a [α. β]。γ]（out）a [b][out a.α. β]。γ] ≤ a [γ]。b [α. β]....（自开）一个[如此]的。α。β] ≤ α。β（open）open a.α. a [β] ≤ α。β（out−in）in a.out a.in a.α≤in a.α（in−out）out a. in a.out a.α≤out a.α• 同余α≤βα≤β.α≤ γβ≤δ（cg−[ ]）（cg−act）（cg−. ）的 。.a[α] ≤a[β]• 及物性• 逻辑m.α≤m.β（反式）α≤β β≤γα≤ γα。 β ≤ γ。δ（−id） α≤α <$α（−l）α<$β≤α（−r）α<$β≤β（−≤） α≤α<$β≤β<$7∧ ≤ ∧图二.类型蕴涵规则8≥≤≤ ≤ ∧ ∧∧≤−→−→.≤ ≤ N × N.(b) ω。其中φ∈N。(c) m.φ∈ N，其中φ∈ N。(d) a[. 其中φ∈N。(e) φ。其中φ，φ∈ N.(ii)如果是ω或形式（c），则正规类型是容易的也正常类型看到模置换，重复和平行的组合与ω。令φ，χ. 范围超过正常类型。一般来说，正常类型与ω不同的有形式。[]..[注]（或。 −[→]（矢量表示法）φ。 a11。... . a n nφ。一其中φ是容易的或者是缺失的（或者，等价地，是ω），并且n 0的情况。法线类型不包含交点。一个正常类型代表一个过程，在这个过程中，在每个环境中，最多有一个动作可能被执行。然而，由于在不同的环境中可以同时启用不同的动作，因此留下了非确定性定义3.2设0为等式。艾瓦伦关系定义。遵守规则通过在规则中替换为0获得（. 1），（. 2），（ω2），（[ ]），（. ），（。 ），（。. 2）（反式）图2。我们可以通过对类型的结构归纳来证明，每个类型都是0等价的，模置换和与ω的平行复合，到一个唯一的类型，正常类型的交集。 该等式可以是0 b。 通过反复地“推出”交叉点，基本上是通过（[]），（。 a和（。）。引理a3.3对于所有α ∈ T t，这里是正规型φ1，...， φ n（n ≥ 1），使得α≤0i∈{1. n}φ i。 类型i∈{1. n}φ i称为α的标准形，记为nf（α），并且它是唯一的模置换和与ω的平行复合.在下面的意义上，环境相对于正常形式是不活跃的引理3.4设φ，−a−[→φ]是正规类型。则φ<$nf（α）if f.φ。 [2019 -04 - 25][2019-04-25].α。a[b]）。引理3.5设nf（α）=φ . 然后(i) nf（ a[ α]）=i∈I a[φ i].i∈Ii(ii) nf（m.α）=i∈Im.φi...(iii) 设nf（ β）= .j∈J<$j。则nf（α. β）=i∈I，j∈Jnf（φi. 1997年）。(iv) nf（nf（α）. β）= nf（α. β）。蕴涵关系可以专门化为正规类型。 让N表示由图3的规则定义的这种关系。9≤在 规 则 N 的 r.h. s 。 是 正 常 的 类 型 只 要 L.H.S. 是 正 常 的 ， 除 了 规 则（openN）和（self openN），因为两个正常类型的并行组合通常是不正常的。注意，在规则（自开N）中，正规类型可以是ω，或者等价地，它可以缺失。我们需要一些技术定义和引理。101−→−→−−在b.φ中。C.φ。C.出a.φ。C..φ。C.• 的交换性和分配性。....（。1N）φ。≤N φ 提供φ。正常.......（。2N）（φ. ）。 φ ≤Nφ。 （注： ），则（？ ）。正常• 关于ω的.（ω 1 N）φ ≤Nω（ω 2 N） φ。ω≤Nφ• 序列化• 减少.（。.N）m..φ。 a[m] ≤m。（.φ。 （a）（inN）a[. −[→]]。b[m]≤. −→。b[a[[]（outN）a[b]. −[→]]。]≤.. −→a[]b[[]]（self openN）a[. −[→χ]]。ψ≤. -[→χ]，对于所有的n=nf（.）所以a.φ. C ..N. Cφ。ψ.（open N）open a.φ. a[n] ≤Nn，对于所有的n ∈ nf（φ. ）（out−inN）in a.out a.in a.φ≤in a.φ（in−outN）out a.in a.out a.φ≤out a.φ• 同余（cg []N）φ≤Na[ φ] ≤N a[ φ]. N（cg actionN）φ≤N<$m.φ≤Nm. φφ≤Nφ≤N（cg −.）的。- 是的 ∗• 及物性φ。a[φ] ≤Nφ。a[]（transN）φ≤N≤Nφ≤NNN11图三.普通类型12⟨⟩S≤≡≤≤Sss||S≤1.2 µ。B.12定义3. 6（i）一个特征对（c.p. 简称）是一对m，−a−[→φ]，其中m是一个动作，−a−[→φ]是一个平行的环境成分，包含正常的类型(ii) 特征序列（c.s.简称）是序列S=P1，...，c.p.的Pn定义3.7设φ是易类型。C. S。与φ相关联，φ以如下方式定义：(i) Sω=πM. −−→−→.(ii) S. （φ a[]）= m，a[]· Sφ其中φ是容易的，·表示连接（如果-a-[→ω]没有元素，我们称之为ω）。注意，如果φ=m。（m. （。 −[→]）。−a−[→]）则Sφ=m，−a−[→]·m，−b[→]·Sµ很容易看出，简单类型和c. s.之间存在一一对应关系。 如果S是一个C。 设τS表示对应于S的易型。 所以 τSφ<$φ，反之亦然。设1，2为c. s.，混洗乘积12是它们所有可能的交织的集合。以下性质的证明是常规的。.引理3.8设φ，φ是易类型。 然后， 当且仅当S∈ Sφ|| S.下面是表示正规类型的蕴涵性质的一个关键引理。引理3.9设φ. ，n，n，x是y的正态分布。假设φ≤Nχ且φ≤Nχ。 然后，对于所有的vnf（。（1）有一个f（？（1），故n =n。证据只要证明引理假设φN ≠ 0和φ χ就足够了。一般性质可以通过传递性容易地得到。然后，在φN的证明上通过归纳法进行证明。 最困难的情况是，N由规则（openN）和（self openN）得到。我们讨论前一个案例。的证明后者类似。..设φ. =opena. a[σ]和nf（ρ. σ）。根据规则（开N），我们有一个打开a. a[σ]N。 使用引理3.4，可以假设w.l.o.g.ρ，σ和很容易，在这种情况下，也必须很容易。此外，根据引理3.4，我们假设m=m。否则，证据就是三小瓶。让我们.ζ ∝ nf (ψ. ）..也就是说， 由引理3.5（4）， σ。 ）。 这意味着S<$∈ Sρ|| Sσ ||S. 更详细地说，让S1成为C.S. 通过从S中消除Sσ的元素而获得同样的命令。r，其中它们发生在Sσ中。 那么我们必须有τ S1 <$nf（ρ. ），以及nf（σ. τ S1）。.我们走吧。注意，通过Lemma。3.5（2）.，对于每种类型的µnf（ρ. 我们有一个VE打开a。µ。 . a[σ]nf（.打开一个. .ρ。 a[σ]。 ）。. .事实上，由（。. 2），打开a. a[σ]。≤0打开a。（ρ. ）。a[σ]<$α对于某13个类型α。14≤∧≤►►（ω）P：ω（m）P：α► m.P：m.αα。P：α（amb）（。）的。.► a[ P]： a[ α]► P：α！P：β► P. Q：α。 β► P： α α≤ β（！）►！P：.α。β（≤）► P：β见图4。类型推理规则...打开a.τ S1. a[σ] nf（open a.ρ. a[σ]。 ），然后.打开a.τ S1. a[ σ] ≤ N.由于σ_nf（σ. τ S1）。✷本节的主要引理涉及正规形式和≤N到≤。引理3.10设α≤β。则对所有的φnf（β），存在φnf（α）使得φ≤N。证据 B. 在α≤β 的 证 明 上 的 y 归 纳 法 。最困难的情 况是 规则（cg−）。），使用引理3.9和3.5（3）处理。✷推论3.11设φ，φ是正规型。 则φ≤φ当且仅当φ≤Nφ。4类型推断由于我们的类型与进程非常相似，因此设计类型分配规则是非常自然的。它们在图4中表示。让−表示从图4的规则中通过消除（）获得的系统中的推理。请注意，系统只有各种构造函数的介绍规则。排除规则被rule（）代替，它也引入和排除（见命题4.5）。下面是演绎的一种标准形式：证明是通过演绎的归纳法引理4.1若αP：α，则r e是类型α<$su c h，使得α−P：α<$且α<$≤α。像往常一样，我们可以通过一个简单的归纳演绎证明一个生成引理。15引理4.2（生成引理）（i）α0：α当且仅当α≤ω;16∧∈ ±∈T≤⟨±⟩FT TP....(ii) m.P：α当且仅当m. P：β且m.β≤α;(iii) α[P]：α当且仅当α −P：β且α[β]≤α（对于某些β）;(iv) 好吧Q：α当且仅当<$−P：β，<$−Q：γ和β。对于某些β，γ，γ ≤ α;(v) 快！P：α当且仅当β i（1 ≤ i ≤ n）和β1。......这是什么？ . β n≤ α，对于某些β1，...，βn。前面的引理说，一个项的类型可以从其子项的类型中以统一的方式获得，这将保证我们将在下一节构建的过滤器模型的组合性。因为我们是在一个在类型赋值级别，这意味着类型在主题扩展下被保留当然，主语归约不应该成立;例如，用规则（红色开放）归约一个过程P相反，全等进程具有相同的类型。这两个属性都可以是通过使用引理4.2对λ和→λ引理4.3（主语同余）PQ和 Q：α引理4.4（主语扩展）P→C →Q， Q：α最后，我们可以通过使用引理4.2对过程进行结构归纳来证明，（I）αβP：αβ► P： α β在我们的系统中是可以接受的。命题4.5（（I）的可容许性）P：α和P：β意味着P：αβ，第一条规则（1）是可以接受的。5过滤器模型我们利用上一节的类型分配系统来定义环境演算的过滤器模型。我们主要遵循[10]的发展路线。设D是一个前序。D的子集L是滤子，如果L是非空上集，即，LL和llimplementlL的每一个有限子集在L中有一个最大下界。考虑具有第3节中定义的包含的类型集。有限非空类型集合的最大下界是集合中类型的交集我们可以观察到，集合（）的滤波器在下面的意义上是一个模型。对于所有P，定义.[[P]]={α∈ T. {\displaystyle{\fnarrow}}{\displaystyle {\fnarrow}。17≤f∈FT±P根据规则（ω），（）（）（）所有P. 主题扩展现在可以重新表述为以下声明：如果P → <$Q，则[[P]]<$[[Q]]。过滤器模型自然地通过子集包含来排序。过滤器上的包含导致项上的排序。定义5.1设P，Q∈ P.当且仅当[[P]] ≠[[Q]]时，P±FQ。序关系F可以通过如下类型的推导来容易地表征。命题5.2设P，Q∈ P。 P±FQ当且仅当，对于所有α，► Q： α。我们将证明过滤器模型完全反映了操作语义，即，它是充分的、完整的，也就是说，它是完全抽象的。充足充分性证明需要对类型和演绎进行双重归纳。遵循标准的方法，我们通过引入将类型作为术语集的可实现性解释来拆分此归纳。其基本思想是，过程P属于类型α的解释当且仅当α可以为P导出。首先我们给出正规类型的解释，然后我们建立所有类型的解释，考虑引理3.3和3.10。在定义类型的解释时，我们将使用比过程更强的归约概念。定义5.3约化关系~over 通过向图1的规则添加以下规则来定义：..（seq）m.P. Q ~ m。（P. Q）例如：（1）a.（a.in）a.（4）a.（5）a.（6）a.（7）a.（8）a.（9）a.（10）a.10很容易证实这一点。~不修改收敛的概念，即。 的P∈ a当且仅当P ~∈ a[Q]. R对于某些过程Q，R.关于~的定义的标准归纳表明，主题扩展性质也适用于~约化。引理5.4 P~∞Q和 Q：α18.≤∈►≤►..作为项集合的正规类型的解释是由结构归纳给出定义5.5正常类型的解释定义如下：(i)[[ω]]=P(ii) [[m.φ]]={P |P ~ m.Q使得Q ∈ [[φ]]}.(iii) [[a[φ]={P |[Q]. [1]，故Q为Q。(iv) [[φ. a[]={P |P ~Q。[a][b][a][a][b][a][b][b][a][b][a][我们需要证明正规型包含关系在正规型解释方面的可靠性。为了达到这个目的，我们需要下面的引理，它的证明与引理3.9相似。.引理5.6设φ，. 你应该是正常人。故P∈[[φ]]和Q∈[[φ]]蕴涵P。Q∈对于所有的φ nf（φ. ）。类型包含关系的可靠性可以通过对N定义的归纳来证明。最有趣的情况是公理（开N）和（自开N），可以用引理5.6来处理。引理5.7设φ，φ是正规类型。然后φ≤N<$蕴涵[[φ]<$[<$]]。我们现在可以定义所有类型的解释定义5.8任意类型的解释定义如下：[[α]]=φnf（α）[[φ]]。从引理3.10和5.7我们得到了关于类型解释的类型包含关系的可靠性。5.9如果α ≤ β，则[[α]]<$[[β]]。正如预期的那样，类型解释完全匹配类型赋值系统。定理5.10（α的可靠性和完备性）α P：α当且仅当P ∈ [[α]].证据可靠性通过对P：α的推导的归纳来证明，使用引理5.9的规则（）。至于完备性，根据定义，它可以证明如果P[[φ]]，则P：φ，当φ是正规的。这个证明可以通过使用关于φ的主题展开对φ进行结构归纳来完成（引理5.4）。✷现在我们能够通过类型化来描述收敛性引理5.11（资源属性）<$P：a[ω]当且仅当P <$a。19►∈公司简介CCφφφωx为oh.x为oh.x为oh.x为oh证据 .P：a[ω]当且仅当（根据定理5.10）P[[a[ω]]当且仅当（根据定义5.5）P~a[Q]. R对于某些过程Q，R.✷我们现在可以得出充分性证明的定理5.12（精确性）若P±FQ，则P± Q。证据 如果[P]由引理5.11，我们得到[P]：a[ω]。 这与PFQ暗示[Q]：a[ω]，因此我们可以得出结论 [问]a再次使用引理5.11。✷完整性我们的完备性证明依赖于构建过程T x，y，其中φ是正常类型，x，y是新鲜的环境名称wi。对于φ。他们的意图是这样的对于所有正规类型φ， x[P]。T x，y≠y当且仅当P=φ。 过程P在为了技术上的方便，测试以前被封闭在环境X在建立这些术语时，有一个收敛于z的过程是有用的，当且仅当它与一个同时收敛于x和y的过程并行。引理5.13设w是一个新的环境名。让Hx，y= w[ in x.out x.in y.out y.z[ out w]]。.然后是H x，yz。Pz当且仅当Px和Py。过程T由正规型上的结构归纳定义。在定义它们时，我们假设有无限的环境名称来源，并且能够选择新的环境名称，而不会与我们正在测试的进程中出现的环境名称冲突。定义5.14[测试术语]设φ是一个正常类型，x，y是环境名。过程Tx，y在φ上以如下方式归纳定义：• Tx，y=p[in x.out x.y[out p]]• Tin a.φ=a[p[in x.so p. a.in v.in z]]...z，y. v [z [open x.t [out z.out v.open v.open a]。 打开t。 T φ• Tout a.φ=p[in x.so p.in a.in z v.in]..z，y. v [a [z [open x.t [out z.out v.open v.open a]。 打开t。 T φ• Topen a.φ=p[in x.so p.a[in v.in z]]..z，y. v [z [open x.t [out z.out v.open v]。 打开t。 T φ• T所以a.φ=p[in x.so p.in z.in a v.in]..z，y. v [z [a [open x.t [out z.out v.open v]]]。 打开t。 T φ20...φφφφ≡►• Tx，. yφ a[φ] =p[在x.in a.so p.出v.in w x.in]..[w]打开a.t[ out w.out v.open v]].x，q. T w，z. Hq，zzx，ya[]• Tx，.y ωφ.=Tx，. yω a[]=Tx，y. 打开t。 Tφ。-是的其中，我们假设所有环境名称（p，q，v，w，x，y，z，.. . ，除了a）介绍-在每个T的定义中引入的x，y是新鲜的。我们称之为Tx，y，表示为EN（Tx，y）。φ φ注意，所有项Tx，y只有在它们并行运行时才是可约的在顶层显示X的环境中，需要还原它们以产生顶层显示Y的工艺。所以它们都必须以正确的方式与x相互作用才能完成这项工作，如下面的引理所示。引理5.15设φ是一个正规类型，Q是一个不包含任何属于EN（Tx，y）的不同于x的环境名的过程。然后.x，y= 0。 ∗Q. Tφ y 意味 Q →x [P]。Q和φP：φ。证据这个证明是通过正规型φ的归纳法得到的。如果φ ω，证明就容易了。归纳步骤是在φ的情况下。作为一个例子，我们给出了φ在a.φ中的情形。其他案件的证据也类似。让S= a[ p[ in x.so p.out a.in v.in z]]... v [z [open x.t [out z.out v.open v.open a]。打开tx为oh.z，y..z，y则T在a中，φ = S。 Tφ。 自Q. S. 通过 归纳假设，我们有..（1）Q. S→πz[P].Q其中P：φ。通过构造，所有出现在S中的名字都不能出现在Q中，除了x和a。那么请注意，要获得（1），需要以下事实。• v必须打开，z没有办法退出v。 但只有在以下情况下，v才能打开开V被执行。• 这只有通过允许环境t在顶层退出，执行动作out z.out v，并被打开才有可能。但这只有在先执行open x• 要 执 行 open x ， 我 们 必 须 在 z 中 有 ambientx ， 但 只 有 p 在 输 入 x 和selfopening之后，才能在v和z中移动x。• 现在p必须与x并行才能进入它。这只有在Q在包含ina动作的顶级环境x上表现出来时才有可能，即。..• 不