环境演算中的安全环境模型及其过滤器模型的研究

理论计算机科学电子笔记104（2004）217-234www.elsevier.com/locate/entcs一种安全环境的伊内斯·马加里亚一、二Dipartimento diInformaticaUniversit`adiTorino Torino，Italy马达莱娜·扎奇3Dipartimento diInformaticaUniversit`adiTorino Torino，Italy摘要过滤器模型的定义被扩展到环境演算的一个变体：安全环境演算。这些类型是通过初等和高阶动作构造的，这些动作定义了进程可以做的动作。类型的蕴涵规则允许将移动的并行在通过引入的类型系统获得的过滤器模型中，任何进程都被解释为它的所有类型的集合类型赋值系统的结果是相对于给定的语义是此外，由过滤器模型诱导的偏序关系与观测等价进行了比较：该模型被证明是适当的，但它不是完全抽象的。关键词：环境演算，安全环境演算，类型，过滤器模型1介绍广域网的一个基本方面是障碍：局部性、通信、移动性和安全性的概念假设部分是1由IST-2001-33477项目、Co finn '01 CoMeta项目、Co finn'01 Napoli项目和IST-2001-33477 DART项目提供部分支持供资机构不负责对本文所列结果的任何使用。2电子邮件：ines@di.unito.it3电子邮件：zacchi@di.unito.it1571-0661 © 2004由Elsevier B. V.出版，CC BY-NC-ND许可下开放获取。doi：10.1016/j.entcs.2004.08.027218I. Margaria，M. Zacchi / Electronic Notes in Theoretical Computer Science 104（2004）217-由于需要跨越障碍，因此具有特殊的重要性。Mobile Ambients（MA）演算[5]是一种描述移动计算的过程演算 移动的单位是环境n[P]，它表示一个名为n的封闭多线程进程P的有界空间。环境可以嵌套，可以并发运行。在环境中，进程可以进行计算并与同一环境中的其他并行进程交互，但不能与其他环境中运行的进程交互。为了与不同环境的过程交互，过程可以执行移动能力：in m、out m和open m以进入或退出其他命名的环境或溶解环境边界。 移动的环境对象经历动作，因为它无法控制移动是否发生以及何时发生。为了给进程提供工具来保护自己免受不必要的移动，人们提出了MA的一个变体：安全环境（SA）演算[12]。SA通过向三个移动性动作添加三个对应的协同动作：in m、out m和openm来从MA获得。在SA中，跨越障碍总是两个环境之间握手的结果因此，环境行为是迁移环境施加的主观控制和共同作用被消耗的环境给出的协议的结果。相互作用的引入是为了研究一种危险的干扰形式，即“一个过程的活动由于活动而被破坏或破坏”的情况。其他的过程环境演算中一个有趣的主题是研究语义等价的适当概念和建立这种等价的方法[6]，[14];为环境演算提出的主要等价关系是基于环境的可观察性的上下文等价[5]。在[9]中，通过滤波器模型研究了MA变体过程之间的等价性，结果完全绝对跟踪时间取决于连续性方程uivalenceet=obs。我的意思是-通过类型系统签名，其中类型表示进程的属性。本文致力于安全环境，并提供具有范式的类型的进程，“顺序”类型的交集这样，一个过程就被描述为它的行为的所有可能的轨迹的集合。此外，受[13]的标记转移系统启发的类型系统被用来定义一个过滤器模型，其中SA过程像往常一样被解释为它们的类型的集合。类型集之间的包含关系导出了一个序关于进程的工作组。 类型赋值系统在给定的语义下，证明了该模型是适当的，并且证明了该模型在如下意义下是适当的：PFQ蕴涵PobsQ。I. Margaria，M. Zacchi / Electronic Notes in Theoretical Computer Science 104（2004）217-219|• 名称：n∈N;• Capabilities：c∈Cc：：=单位：m|处m|开M|在m|处m|打开m;• 过程：P∈PP：：=0 |C. P| P1|P2|（νn）P|！|! P.Fig. 1. 进程语法2微积分图1给出了演算的语法。 为了简单起见，在本文中，我们省略了通信。N表示环境名称的集合，范围为n，m，.; C能力的集合，范围为c，d，.P是过程的集合，由P，Q. . . 限制算子（νn）是环境名的一个结合物，并导致了过程P（fn（P））的名称自由出现和α-转换的通常概念在《易经》中，操作符. 优先于并行合成|C.P|Q读作（c.P）Q。nil进程0经常被省略，所以c可以是一种简写梭0的情况。图2中定义的结构同余和归约规则给出了演算的操作语义。对于外归约规则，我们遵循[13]中提出的变体，要求由目标计算而不是由环境m来执行环境m之外的迁移的协同能力out m。这种选择是由于给予接收环境对运动的控制的目的在进程演算中，定义进程行为等价的标准方法是may-testing等价：当两个进程被放置在相同的上下文中时，如果它们满足相同的观察谓词，则它们在上下文上是等价的对于MA，提出的观察谓词[5]是在过程的顶层发生的环境，其名称不受限制。实际上，在过程的顶层存在环境n，表示P通过n与环境交互的可能性。在[12]中，对于SA，在跨越边界需要授权的情况下，我们使用的是[12]中定义的简化，如[13]中所介绍的，只需要存在开放的协同能力。220I. Margaria，M. Zacchi / Electronic Notes in Theoretical Computer Science 104（2004）217-≡→⇓∗是最小等价关系：(i) 包括α-转化(ii) 由所有运营商(iii) 满足以下规则：- P|QQ|P（结构参数通信）- （P|Q）|RP|（Q|（R）（结构杆件）- P|0元（零杆结构）-（νn）0 0（结构零分辨率）-我知道P！P|P（结构重复部分）-我知道0 ≡ 0（结构零重复）-（νn）（νm）P（νm）（νn）P（结构研究）-n∈f n（P）implies（νn）（P|Q）CUP|（νn）Q（结构ResPar）-n=/mimplies（v n）（m[P]）m[（νn）P]（结构分辨率和环境）→是最小前序关系，它：(i) 除了prefixing之外(ii) 满足以下规则：— m[在n.P中]|Q] |S] → n [ m [P|Q]| R| S]（红色） |S](Red-In)— m [n][out] m.P |Q] |R]|输出m.S → n [P |Q] |m [R] |S（红色）— 开放式 |R] → P|Q| R（红开）|R(Red-Open)— P<$Q，Q→R，R<$S<$ P→S（红色结构）图二.结构同余与约化关系定义2.1（i）过程P呈现环境n：P n，如果P→n→（ν→−m）（n[o penn. Q|R]|S），对于S，R，S（n∈/{→−m}），(ii) 如果对于所有上下文C [ ]和环境n：C [P]<$n， C[Q]n.(iii) 如果P=obsQ且Q=obsP，则P=obsQ。注2.2注意，P→ P→Q意味着Q等于P，但一般来说，它并不意味着P=Q;f或exampl e，l etP=o penn。0|penn. 0|m[0]]和Q = m [0]，PQ ， 但 对于上下文[-]，P n，而Q不收敛到任何环境n。I. Margaria，M. Zacchi / Electronic Notes in Theoretical Computer Science 104（2004）217-2213类型类型系统已经被提出用于移动演算，其目标基本上是提供一种控制工具：控制环境的移动性[4]，交换的值[7]，没有严重的干扰[12]。不同的是在[9]中为MA提出的类型系统的目标：描述进程行为，以便提供一个给出其语义的工具。这也是我们SA的目标;我们寻找的过程语义是一种跟踪语义，其中过程的特征在于它可能执行的所有动作序列。因此，在类型的定义中，我们想要捕捉行动的概念。在[13]中，转移系统的标签是行动，被定义为能力的原始定义的扩展。事实上，每一种能力都会产生一种行为，但是，当插入到环境中时，它可以引发更高阶的行为。事实上，由于n.P中的进程，当插入到适当的环境中时，可以执行n中的动作，然后它的行为是进程P中的一个，以同样的方式，进程m[in n.P]，放置在适当的环境中，有能力将环境m移动到环境中n，然后它继续进行一些行为。为了描述这种连续性，MerroandHenness使 用 了 约 束 （ ν→−m ） （

nQ ） （ sealso[6] ， [12] ） ; 约 束 （ ν→−m ）（

nQ）模型将这种连续性视为一种概率，在此之后，执行一个动作，将环境n留在过程P之内，将过程n留在过程Q之外;→−m表示由P和Q。我们遵循这个建议，所以我们的类型T集合除了包含由能力和协同能力（基本动作）诱导的六个动作之外，还包含五个高阶动作，确切地说，由m[in n]诱导的动作entermn，由m[out n]诱导的动作exit mn，由n[in n]诱导的动作enter n，由n[m[out n]]诱导的动作popmn和由m [ outn]诱导的动作free nn[打开n].对（entermn，enter n）、（popmn，out n）、（free n，open n）是所述匹配对。请注意，这里考虑的out语义的定义允许匹配对（popmn，outn）的动作处于相同的环境嵌套级别。类型T的集合的形式定义在图中给出3 .第三章。先决条件1定义需要作为延续的标准类型的动作，而Prefixes2定义一个由具体化（ν→−m）（σ>nτ）遵循的矩阵，其中，σ是进入环境n的过程的类型，τ是进入环境n的过程的类型，→−m是由σ和τ表示的原始过程。在方程uel（ν→−m）（<σ>nτ）TQ中，表示n（ν→−m）（<σ>n（τ））的具体化|Q）），其中as（ν→−m ）（<σ>nτ） ²Q表示steconcretionn（ν→−m）（<（σ|222I. Margaria，M. Zacchi / Electronic Notes in Theoretical Computer Science 104（2004）217-∧∧}• 前缀1：µ：：= in n|外出;外出|打开n|在n|外出;外出|打开n|popmn|free n;• 前缀2：α：：=输入mn|退出mn|输入n;• 作用：γ：：= µ|α;• Types：σ：：=ω|µ.σ|α。（ν→−m）（<σ1>nσ2）|n[σ]|（νn）σ|| σ1|σ2|σ1∧σ2图三. 类型定义Q）>nτ）。除了动作之外，作为类型构造器，我们考虑环境，限制，并行组合和交集。类型ω表示对所有过程都为真的性质，而交集模型一个动作γ被称为与环境n相容，如果γ∈ {in m，out m，in n，open n，exitmn，否则不相容。如果γ与n不相容，则类型n[γ.σ]被称为死锁。类型的自由名称的概念是常见的;记住，前缀的下标名称的出现不能被认为是自由出现。在类型集T上定义了一个偏序关系≤; σ≤τ，表示性质σ包含性质τ;στ i <$σ≤τ且τ≤σ。类型蕴涵规则如图4和图5所示。Action规则定义了更高阶的操作，而Reduction规则则将一个操作的执行对应于能力的丧失这一事实形式化。通常，归约规则的右手边称为契约。与我们的目标特别相关的是序列化规则，它可以被解释为将动作的并行组合转换为交错动作序列之间的非确定性选择第一个四个序列化规则表明，类型γ. （σ|τ）的能力比γ.|τ，因为它可以与它的环境相适应，作为第一个运动，只有作用量γ，而γ.σ|τ除作用于γ外，还可能超越由τ型引起的其它运动。最后两个规则说，两个前缀类型γ1.σ的并行组合|τ等价于不同路径之间的非确定性选择;如果动作γ1和γ2不匹配路径，有两个：一个从移动γ1开始，另一个从移动γ2开始。如果两个动作γ1和γ2匹配，则存在第三个选择：执行归约。为了简单起见，在图中。5.前缀类型的表示法已经被扩展，使得γ.σ同时表示前缀1类型（因此σ表示一个类型）和前缀2类型（因此σ表示一个凝结）。 所以在表达式I. Margaria，M. Zacchi / Electronic Notes in Theoretical Computer Science 104（2004）217-223ii∈[1···n]⊂||形状为γ1。（σ γ2.τ），（σ γ2.τ）表示类型之间的通常平行合成，如果γ1是初等作用，则表示（σ2（γ2.τ）），否则表示（σT（γ2.τ））。类型被认为是模。通过与ω的相交和平行合成来保持。类型的并行组合被认为是模排列，类型的交集被认为是模排列和重复。σ 表 示 正交性σ1<$σ2<$σn; τi∈[1···n]σi表示s有τσi，其中s是σi。一个关键的概念是顺序类型。顺序类型对执行一系列操作的进程的行为进行建模。定义3.1（i）序列类型的集合ST被归纳地定义为如下：|.|α。（v→−m）（n =1>n=2）(ii)顺序类型的权重定义如下：|=零|=0|= 1 +|ϕ |如果µ free n|if µfree n或 µ/= popmn=2 + |ϕ|否则|α. （v→−m）（n=2）|=2+|ϕ1|+的|ϕ2|为了证明每一种类型都可以用顺序类型的非确定性选择来表示，我们使用了res，unfold和ser函数。它们的正式定义相当复杂，可以在附录中找到这里我们只作一个非正式的描述。函数res由序列类型定义的结构归纳法定义，它是一个由名称s→−n和一个等价的类型递归组成的等式顺序类型，使得：res（→−n ，n）（ν→−n）<$.函数ser和unfold是通过对权重的同时归纳来定义的。ser接受两个顺序类型x，x作为参数，并返回一组顺序类型，使得：∈ ser（|χ函数unfold接受一个名称n和一个顺序类型n作为参数，并返回一组顺序类型，使得：<$∈unfold（n，<$）<$n[<$]我们现在可以证明，每一个类型都有一个唯一的范式模置换和与ω的平行复合。224I. Margaria，M. Zacchi / Electronic Notes in Theoretical Computer Science 104（2004）217-• 关于ω的— σ≤ ω− σσ |ω— （νn）ωω−n [ω] ω• 并行合成的交换性和结合性|-σ|ττ|σ−（σ|τ）|Qσ |（τ|Q）• 交叉点— σ∧τ≤σ σ ∧τ≤τ−σ≤σ ∧σ— σ≤σJ和τ≤τ J<$σ<$τ≤σJ <$τJ− ρ|（στ）（ρ|σ）（ρ|τ）-n[στ]n [σ]<$n [τ]−µ。（στ）µ.σµ.τ-α（ν→−m）（<στ>nρ）α. （ν→−m）（<σ>nρ）<$α。（ν→−m）（τ>nρ）-α（ν→−m）（<σ>nρτ）α. （ν→−m）（<σ>nρ）<$α。（ν→−m）（σ>nτ）• 行动• 减少— m[in n.σ]输入mn. （nω）— m[out n.σ]出口m. （<ω >nm[σ]）— n[in n.σ]进入;进入（<σ >nω）— n[开n.σ]自由的，自由的— 出口，出口，出口（<σ >nτ）popmn. （n [σ] |τ）— n[γ.σ]ωifγ 与n不相容-输入mn。（v→−p）（<σ1>nσ2）|进入;进入（v→−q）（<τ1>nτ2）≤≤（ν→−p）（ν→−q）（n[σ1|τ1]|σ2|τ2）— popm.σ| outn. ≤σ|τ— 开放的，开放的|自由的，自由的 ≤ σ |τ见图4。 类型蕴涵规则（第一部分）I. Margaria，M. Zacchi / Electronic Notes in Theoretical Computer Science 104（2004）217-225∈i∈[1···n]ii• 限制-（νm）n[σ]n [（νm）σ]m/= n— （νn）（νm）σ（νm）（νn）σ-（νm）（σ|τ）σ|（νm）τm∈/fn（σ）-（νm）（στ）（νm）σ（νm）τ— （νm）γ.σωifm∈fn（γ）— （νm）γ。σγ。（νm）σifm∈/fn（γ）• 序列化-µ.σ |τ≤µ。（σ|τ）— 输入mn. （ν→−h）（<σ>nτ）|ρ≤entermn。（ν→−h）（<σ>n（τ|ρ））— 出口，出口; （ν→−h）（<σ>nτ）|ρ≤exitmn。（ν→−h）（<σ|ρ>nτ）— 进入;进入（ν→−h）（<σ>nτ）|ρ ≤输入n。（ν→−h）（<σ>n（τ|ρ））— γ1.σ|γ2.τγ1。（σ|γ2.τ）<$γ2. （γ1.σ|τ） 如果γ1和γ2不匹配Q=1. （σ|γ2.τ）<$γ2. （γ1.σ|τ）如果γ1和γ2匹配，ρ是契约• 同余-σ≤τn[σ]≤n [τ]−σ ≤ τµ.σ ≤µ.τ— σ≤τ（νm）σ ≤（νm）τ−σ ≤τσ|ρ≤τ|ρ• 及物性（n）Iffn（ρ）<${→−h}=Φ-σ≤τ &τ≤ρ⇒σ≤ρ图五. 类型蕴涵规则（第二部分）引理3.2对于所有σT存在唯一的类型σ，其中σ 是等价类型，i∈[1···n]<$i. 本文给出了σ的标准形，记为nf（σ）.证据证明是通过类型的结构归纳，使用函数res，ser和unfold。226I. Margaria，M. Zacchi / Electronic Notes in Theoretical Computer Science 104（2004）217-nf（ σ）ζ∝ nf( σ), χ∝ nf( τ)≤►(v) nf（σ|τ）=<$∈ser（χ，<$），χ<$ nf（ σ），nf（τ）(i) nf（ω）= ω。(ii) nf（μ.σ）=μ. σ。(iii) nf（α. （<σ>nτ））=（α. （nx））。(iv) nf（n [σ]）=n ∈unfold（n，n），n ∈ nf（σ）n.(vi) nf（στ）=nf（σ）<$nf（τ）(vii) nf（（ν→−n）σ）=n=res（→−n，n），n f（σ）n.Q例3.3σm[见n.in m.ω|开m.ω]nf（σ）=退出mn。（<ω >n（输入m。（mω）出口mn。（<ω >n（免费m.in m.ω））免费的m.out n.in m.ωnf（n [σ]）= popmn. （输入m。（mω））popmn.free m.in m.下面的引理，通过归纳法证明了类型和范式之间的引理3.4（i）i∈I <$i ≤ j∈ Jχj意味着对于每个j∈J，i∈I，使得i≤ χj。(ii)设σ≤τ。 则对于每个χnf（τ），存在一个χnf（σ），使得X≤ X。4类型推断类型通过类型分配系统与进程相关联，该系统由图1的规则定义。六、我们可以通过简单的归纳演绎证明以下引理：引理4.1（生成引理）（i） 我的 σ ω;(ii) c.P：σi 对于某些τ;(iii) n[P]：σi 对于某些τ;(iv) n（νn）P：σ i n （ν n）P：τ且（νn）τ≤σ 对于某些τ;(v) CUP|Q：σ iP：τ，Q：ρ和τ|ρ≤σ 对于某些τ，ρ;(vi) 快！P：σ i P：τi（1 ≤i≤n）和τ1|......这是什么？| τn ≤σ对于τi（1 ≤i≤ n）.I. Margaria，M. Zacchi / Electronic Notes in Theoretical Computer Science 104（2004）217-227≡→⊆► n[P]：n[σ]引理4.1有和的定义，允许我们陈述主语同余性质（全等过程有相同的类型）和主语扩展性质（在主语扩展下类型被保留）。证明是通过归纳演绎。引理4.2（主语同余）<$P：σ和 PQ⇒Q：σ。引理4.3（主语扩展） 和P→QQ⇒P：σ。5过滤器模型通过类型系统构造过滤器模型是广泛用于λ演算及其扩展的方法[1]，[2]，[3]。过滤器模型也用于高阶并发过程[10]，[11]，以及[9]中的移动环境。 让我们回顾一下过滤器的定义。设是一个预序。D的一个非空子集L是一个过滤器，如果它是一个上集，即d∈L，并且d≤DJ蕴涵DJ∈L，且L的每个有限子集在L中有一个最大下界.我们模型的定义域是，并且是集合包含关系。请注意，交集运算符在是一个完备的代数格，因此每个连续函数f都有最小不动点fix（f）。引理5.1 是一个完备的代数格。如果A≠T，则↑A表示由A生成的滤波器，通过关闭（ω）P：ω（ix）► P：σ c∈C► c.P：c.σ（amb）P：σ n∈ N（|）压力：σ（res）（！）► （νn）P：（νn）σ（）P：σP：τ （≤）► P：στ见图6。类型推理规则P1：σP2：τ► P1|P2：σ|τ► P：哦！ P：τ► ！P：σ|τ► P：σ σ≤τ► P：τ228I. Margaria，M. Zacchi / Electronic Notes in Theoretical Computer Science 104（2004）217-⊆ ⊆⊆P×→↑{||∈∈ }A下有限交和由（上闭A下）≤。设par：F（T）F（T）F（T）是定义为par（F，G）=σ τσF和τG.证明函数par连续是模型中类型的解释是通过函数由类型的结构归纳法定义的。定义5.2函数F − F：P →F（T）定义如下：• 0↑{ω}• P=↑ {c.σ|σ∈ P<$}• 中文（简体）=↑ {n [σ] |σ∈ P<$}• CUP|Q=par（P，Q）• （νn）P=↑ {（νn）σ|σ∈ P<$}• 快！P_x = f_x（λ_X∈F（T））. par（Par，X））通过引理4.2，我们可以证明，过程的解释是可以为它导出的所有类型的定理5.3<$P<$={σ |P：σ}对滤波器的包含产生了对过程的序关系<$F，在这个意义上P<$FQ当且仅当<$P<$F <$Q<$。 显然，由定理5.3，得出P<$FQ当且仅当对所有σ，<$P：σ蕴涵<$Q：σ。一个关键的问题是顺序关系F和观察关系obs。我们证明，PFQ意味着PobsQ，而反例表明，相反的是不正确的，所以该模型是足够的，但它不能完全抽象。充分性的证明是通过类型解释完成的，以一种相当标准的方式定义。这种解释可以很容易地证明类型分配系统是健全的和完整的关于所获得的语义。我们将F（T）的每一个类型与一组滤波器相联系（类型解释），并且证明了过程P的解释属于类型σ的解释当且仅当σ可为P导出。对于类型解释的定义，我们需要一个更强的过程约简的概念，它不会修改环境收敛的概念定义5.4归约关系~over是通过在图2的归约规则中增加以下规则来定义的：C.P|Q~c. （P |Q）（红色序列）引理5.5（i） P~Q和Q：σP：σI. Margaria，M. Zacchi / Electronic Notes in Theoretical Computer Science 104（2004）217-229⇓||∈ { }（ii）P niP~ （v→−m）（n[o penn. QR]S）（n/→−m）对于一些工艺 Q，R，S。类型的解释分两步完成：首先定义顺序类型的解释，然后使用范式的定义来构造泛型类型的解释。定义5.6序列类型的解释由结构归纳法定义如下：• ω• c.|P~c.Q和Q∈}• 自由的n.自由={P|开的，开的|R和Q|R∈}• popmn.|P~n [m [out n.Q]] |R和m [Q] |R∈}• 中间人; （v→−h）（n<$2）n={P|P~∞（ν→−h）（m[inn.Q]|R）和d且m [Q]∈1且 R∈ <$$>2<$}• 我的名字。（v→−h）（n<$2）n={P|P~∞（ν→−h）（m[outn.Q]|R）and且m [Q]∈2且R∈1}• 主持人; （v→−h）（n<$2）n={P|P~∞（ν→−h）（n[inn.Q]|R）和d且Q∈1且R∈2}定义5.7泛型类型的解释由以下定义：σ为了证明类型赋值的可靠性，我们需要一些引理，特别是必须证明类型解释与蕴涵关系一致引理5.8（i）P∈蕴涵（νn）P∈，对所有的nf（（νn））.(ii) 设χ和χ是两个连续类型。则P∈且Q∈χ蕴涵P|Q∈，对于所有的nf（|χ）和m [P]∈<$对于所有<$<$nf（m [<$]）.(iii) σ≤ τ意味ǁσǁ ⊆ ǁ τǁ证据(i) 通过顺序类型的结构归纳。(ii) 通过同时感应的重量。(iii) σ≤τnf（σ）≤nf（τ）对于每个χnf（τ），存在一个χnf（σ）使得χ≤χ<$P∈ <$σ<$蕴涵P ∈<$τ<$。230I. Margaria，M. Zacchi / Electronic Notes in Theoretical Computer Science 104（2004）217-QQ定理5.9（σ i的可靠性和完备性）σ i ∈ σ i，σi∈σi。证据对于规则（≤），使用引理5.8（iv）通过演绎归纳法证明了可靠性。 关于完备性，对于序列类型证明：P∈P：是足够的。这可以通过使用定义5.7、引理5.5和引理4.1对权重进行归纳来证明。我们现在可以证明，有一个类型的特点收敛到一个环境。引理5.10P：free n.ω iPn证据（=）P：free n.ωP∈free n.ωP~|R和Q|R∈ω定义5.6平 引理5.5（ii）（n=）P<$n<$P~n（v→−m）（n[o penn. Q|R]|S）byLemma5. 5（二）⇒ ►P：n [open n.ω] |ωby 学科拓展n.ω by（≤）rule.Q定理5.11（不确定性）如果P<$FQ，则P<$obsQ。证据Q为了表明模型不是完全抽象的，让我们考虑过程PQ：P = n [in n. 0个字符]Q= n [m][out n.open m. 0 |在...中，在...中0]|打开，打开; 0它们在序关系<$F中是不可比较的，因为对于P是可导的，类型为entern。（<ω >nω），而相同的类型对于Q是不可导的，反之亦然，类型开m.out n。（<ω >nω）对于Q是可导的，C[P]⇒C[P]：自由n.ωC[Q]：自由n.ω引理5.10因为Q有P的所有类型⇒C[Q]n引理5.10I. Margaria，M. Zacchi / Electronic Notes in Theoretical Computer Science 104（2004）217-231但P不是。在序关系中，P <$obs然而P <$obsQ，事实上对于非平凡上下文C[−]，如果C [P]<$h对于某个环境h，则C[−]必须通过展示出n的余能力来允许从n的迁移，因此它必须具有形式C [−| outn]，但C [Q| outn] →n [P]|所以没有办法在P和Q之间找到一个区别的上下文。这一事实并不确定--prising：Merro和Hennessy [13]已经注意到了在构思一个有区别的动作输入上下文时的困难。6结论我们已经通过安全环境的类型系统构建了一个过滤器模型，遵循[9]中定义的移动环境的过滤器模型。我们类型的基本元素是可以被认为是环境的原子移动的动作。我们证明了每个类型都有一个范式，它是序列类型的交集;这一事实允许将动作的并行组合表示为交错动作序列的非确定性选择。这个模型是适当的，但不是完全抽象的。在[9]中，是一种新的能力，即自开n，使过滤器模型完全抽象。我们推测，在SA中，增加自开n能力应该允许获得完全抽象的过滤器模型，但它应该扭曲了精神。的微积分。另一方面，自开n及其相应的外部环境中的共同作用并不修改微积分。在未来，我们希望研究一种方法来获得一个完全抽象的模型，或者通过更强的类型包含概念，或者通过向功能添加新的功能（cfr。[13]中的密码）。研究的其他有趣的论点是这种类型的系统的应用到格雷夫斯干扰的问题[12]和这个系统和周围结石的逻辑之间的联系，[8]，[14]。引用[1] S. Abramsky和C.H. L. 昂Lazy lambda演算中的完全抽象信息与计算，105（2）：159[2] H. Barendregt，M. Coppo和M.德扎尼-钱卡里尼一个过滤器lambda模型和类型赋值的完备性。符号逻辑杂志，48（4）：931[3] G.布多（严格）并行函数的Lambda演算。信息与计算，108（1）：51[4] L. Cardelli，G.Ghelli和A.D. 戈登移动环境的移动类型在j.维德曼，P. van Emde Boas和M.Nielsen，编辑，ICALP史普林格出版社232I. Margaria，M. Zacchi / Electronic Notes in Theoretical Computer Science 104（2004）217-× → ×→[5] L. Cardelli和A.D. 戈登移动环境。FoSSaCS'98，LNCS第1378卷，第140-155页，柏林，1998年史普林格出版社[6] L. Cardelli和A. D.戈登移动环境的等式属性。FoSSaCS'98，LNCS第1578卷，第212-226页，柏林，1999年史普林格出版社[7] L. Cardelli和A. D.戈登移动环境的类型。在POPLPress.[8] L. Cardelli和A. D.戈登随时随地移动环境的模态逻辑。在POPL北京：人民出版社，2000年。[9] M. Coppo和M.德扎尼-钱卡里尼高阶移动环境的完全抽象模型在VMCAI史普林格出版社[10] C. Hartonas和M.轩尼诗具有高阶值传递的函数式/并发语言的完全抽象性。信息与计算，145（1）：64[11] M. 轩尼诗高阶过程的完全抽象指称模型信息与计算，112（1）：55[12] F. Levi和D.桑吉奥吉控制环境中的干扰。在POPLPress.[13] M. Merro和M.轩尼诗安全环境中的互模拟一致性载于SIGPLAN Notices，31（2002年1月Press.[14] D. 桑吉奥吉环境逻辑的外延性与内涵性在POPLPress.7附录定义7.1（i）函数res：（N×S）→S由序列类型定义的结构归纳法定义如下：— res（→−h ，ω）=ω-res（→−h ，µ. ）=µ。r es（→−h ，n）iffn（μ）<${→−h}=Φ— res（→−h ，µ. n）=ωtherwis e-res（→−h ，α. （v→−m）（n =1>n=2））==α。（ν→−m）（ν→−h）（α1>n<$2）iffn（α）<${→−h}=Φ— res（→−h ，α. （v→−m）（n ≥1>n≥2））=ω otherwis e(ii) 函数ser：（S S）2S和unfold：（N S）2S通过对权重的同时归纳来定义。a) 为|ϕ| +的|ψ|所以，我们要以这样一种方式来定义ser（φ，），即对于每一个∈ser（φ， |≤ w ;| ≤ w;b) 为|φ|我们用这样一种方式定义展开（n，φ）：对于每一个functions（n，φ）： |≤ 1+ w。|≤ 1+ w.I. Margaria，M. Zacchi / Electronic Notes in Theoretical Computer Science 104（2004）217-233基本步骤：a) ser（ω，ω）=ωb) unfold（n，ω）=ω诱导步骤：a) 我们区分以下情况：-ε=μ.φ1，ε=ω：ser（ε，ε）={ε}— φ = μ.φ1，φ = ν. φ1，μ，ν不匹配：ser（，）={µ.|<$∈ser（<$1，ν.<$1）}<${ν.<$|{\displaystyle{\mathbb {}— φ = μ.φ1，φ = ν. φ1，µ、ν匹配：ser（x，x）={x |χ ∈ ser（<$1，<$1）}<${μ.<$|<$∈ ser（φ1，ν.<$1）}<${v.|{\displaystyle {\mathbb {}-μ=μ。φ1， φ=α。（v→−m）（n =1>n=2）：ser（，）={µ.|<$∈ser（<$1，<$）}<${α. （ν→−m）（<π1>nχ）|χ∈ser（μ. φ1，φ2）}-α= α。（v→−m）（n≥2）， n= β. （v→−q）（m ≥1>m≥2），α、β不匹配：se r（n，n）={α. （v→−m）（ n nn）|<$∈ser（<$2，<$）}<${β. （ν→−q）（<χ1>mχ）|χ∈ser（<$2，<$2）}—=输入pn。（v→−m）（n1>n n<$2）和nd=输入n。（v→−q）（m≥2）：se r（n，n）={enterpn. （v→−m）（ n nn）|<$∈ser（φ2，<$）}<${entern. （v→−q）（nx）|χ∈ser（φ，φ2）}{\fnSimHei\bord1\shad1\pos（200，288）}|n=res（→−m→−q，n J）， n J∈se r（n1，n2）||<$1∈ unfold（n，χ），χ ∈ ser（φ1，<$1）和<$2∈ser（φ2，<$2）}234I. Margaria，M. Zacchi / Electronic Notes in Theoretical Computer Science 104（2004）217-n∈（ n，n）b) 我们区分以下情况：— =µ.unfold（n，n）={ω}如果µ与n不相容={输入nm。（m）|<$∈ unfold（n，<$）} if μ = outm={enter n. （nω）|如果n中的μ =，则{n∈ unfold（n，n）}={free n.}ifµ =open n-α = α。<（1>n2）：unfold（n，n）={ω}如果α与n={popmn.|<$∈ser（χ，<$2），其中χ∈unfold（n，<$1）}如果α=exitmn给我7分。2（i）如果εi是等价型pe，（ν→−m）εres（→−m，εr）(ii) 如果n是顺序类型，则n[n]展开n(iii) 如果 和χ是序列类型，|χ∈ser（χ，χ）证据 以其义，以其义。Q