π演算中的移动过程的有限多态性类分配系统

理论计算机科学电子笔记136（2005）117-132www.elsevier.com/locate/entcsπ-演算的序列类型塞尔吉奥·马德雷斯1伦敦帝国理工学院计算机系英国伦敦SW7 2AZ。摘要我们引入通道序列类型来研究π演算中建模的移动过程的有限多态性。我们将每个通道关联到一组交换类型，并且我们要求输出进程发送其中一种类型的值，输入进程接受该组中任何类型的值。我们的类型分配系统享有主题减少，并保证没有通信错误。我们给出了几个多态性的例子，我们用严格的交集类型规则编码λ -演算。关键词：多态性，移动进程，交叉类型，联合类型，编码。1介绍交叉类型是在20世纪70年代后期由Coppo和Dezani-Ciancaglini [5]引入的，目的是定义λ演算的类型系统，其中类型通过β转换保持，并且每个拥有范式的项从那时起，交叉类型被广泛研究，并找到了许多应用，从Reynolds为Forsythe编程语言[17]的多态性工作开始。从编程语言的角度来看，交集类型表达了关于程序的有限但无限的信 息 量 ， 称 为 无 限 多 态 性 。 例 如 ， 算 术 函 数 可 以 被 赋 予 类 型Int→IntReal→Real，这意味着它在其参数1电子邮件：maffeis@doc.ic.ac.uk。由微软剑桥研究院和EPSRC电子科学基金支持。1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.06.012118S. Maffeis/Electronic Notes in Theoretical Computer Science 136（2005）117（通用多态性），或者在参数（和结果）是整数或实数的情况下提供两种不同的实现（特别多态性）。我们认为，一个类似的方法（指定的一组类型的消息，一个通道可以交换）可以采用类型的通信进程演算，并产生更多的可扩展性比通常的存在/通用的方法多态性。我们研究了π演算的无穷多态性[13]，这是一种基本的形式主义，用于推理并发和移动进程。Berger，Honda和Yoshida最近关于泛型的研究[3]强调了π演算中通信通道的两个端点如何在泛类型和存在类型量化方面发挥双重作用。因此，我们发现，通道的交集和并集类型不能分开，必须立即考虑我们所谓的序列类型，诉诸科波和德扎尼-钱卡格里尼使用的原始名称。我们将每个通道关联到一组交换类型，并要求输出进程发送其中一种类型的值，输入进程接受该组中所有类型的值。我们还考虑了当集合为空时的情况，这对应于交集类型规则的常数ω：与空集相关联的通道不能用于通信。相关工作。文献[5，7，2]中提出了一些重要的交叉型指派系统.严格交集类型在[19]中被引入，它们的主要类型性质在[20]中被研究这些方法之间的比较可以在[21]中找到。交叉类型已被用于定义λ演算[2]、π演算[8]和Mobile Ambients [6]的变体的滤波器模型。无论如何，[8]的方法和目的与本文的方法和目的不同。特别地，用于过滤器模型的类型被分配给过程，并且非常接近地反映过程结构（包含用于复制、输入、匹配、并行组合等的构造器），而我们只给通道类型，我们的类型只是代表通道可能的交换类型的集合。我们的类型系统旨在防止通信错误，而不是精确地描述术语的行为在π演算中，多态性在其各种不同的形式中得到了广泛的研究：泛[9，24]，谓词[23]，存在[18，16]和泛型[3]。一种不同的方法是[10]中的方法，它定义了一个基于输入和输出排序元组的排序推理系统（类似于我们的类型序列）。他们的系统与我们的系统是不可比较的，因为它采用了一种名义方法而不是结构方法，它不享受主语还原，为了防止交流错误，它诉诸于一致类型的辅助概念，例如，排除了通道的可能性，S. Maffeis/Electronic Notes in Theoretical Computer Science 136（2005）117119交换类型不同，这可以在我们的系统中接受。据我们所知，这篇论文代表了在π演算的背景下研究有限多态性的第一次尝试。论文的结构。在第二节中，我们介绍了多元π-演算及其基本类型。在第3节中，我们通过一个类型赋值系统来介绍序列类型，该类型赋值系统具有主语归约的特性，并保证没有通信错误，我们还给出了有限多形性的例子。在第四节中，我们给出了一个将严格交集类型规则的按名调用λ-演算编码为序列类型的π-演算的保类型编码。在第5节中，我们以一个扩展的例子来结束，展示如何使用序列类型来类型化归纳定义的多态数据结构。2π演算2.1语法和语义为了简单起见，我们使用π演算的多进变体[13]，而没有沉默的动作前缀和混合选择。设N是通道名称的可枚举集合，范围为x，y，z，w。 对于元组x1，我们使用不包含x的元素，. . ，xn，并且当n个参数n不重要时，我们将x n写入。PROCESSAREGENEVENYP：：=0|P|P|！P|（νx）P|y（x）.P|yx.P空进程由0、P|Q是P和Q的平行合成，！P（replication）表示P的无限拷贝数，（vx）P表示P中的名字x，y（x_x_y），P表示沿通道y进行n次输入的过程y，其中变量x_x_y在P中，y_x_x_y在P中，P是沿y进行x_x_y输入的输出过程y. 本文将这一问题归结为结构同余关系，定义为满足约束名的α-转换的最小同余关系，给出了（|，0）和下面报告的公理（νz）00（νz）（νw）P（νw）（νz）Pz/∈ fn（P）<$（νz）（P|Q）可持续发展|Q ！PP|！P我们使用标准的语法约定，在过程中省略尾随零，并将x.P和x.P写入空元组沿通道x的输出和输入。约简语义是进程上最小的二元关系−→满足表1中给出的规则。公理（COM）负责沿着通道y传递值zn。120S. Maffeis/Electronic Notes in Theoretical Computer Science 136（2005）117（COM）y（x<$n）.P|y<$z<$n<$.Q −→P{z<$n/x<$n}|QP−→QP−→PJ（C-R ES）（νx）P −→（νx）Q （C-P AR）P |Q −→ P J|Q（S结构） N<$NJNJ−→MJMJ<$MN−→M表1减少规则当两个进程试图在同一通道的两个端点上进行通信时，会验证通信错误条件。定义2.1我们将过程上的错误谓词定义为P† ⇐⇒P（νz）（P1|y（x<$n）.R|你知道的。其中m/= n。如果不是P<$的情况，我们写P/<$。2.2基本类型分配系统π演算的基本Curry风格类型分配系统，如[18]所示，是基于将交换类型与每个通道相关联的环境Γ（部分函数），描述可以通信的对象基本类型和环境的正式定义是（B-T型）S，T：：=[T]（T型环境）Γ：：= Γ，x：T|∅Thestateme ntx：[T]me statxisachannelexchanginggtuplesofvalueswithhetype ss p e s p e s p especificdbyT. Ifx=x1， . . . ，xn和T_n=T_1， . . Tn，我们使用正交符号xn：Tn，对于x1：T1， . . ，xn：Tn. Ifrcontainsx：Twwriter（x）=T. 表2中给出了这类信号处理规则，并定义了绑定名称的上到字母转换。这是一个公认的结果，基本类型系统满足在归约下保持类型的标准属性，并保证良好类型的进程不会发生通信错误。定理2.2（[18]）（i）若Γ <$P且P→Q，则Γ <$Q. （ii）如果ΓP然后是P/†。S. Maffeis/Electronic Notes in Theoretical Computer Science 136（2005）117121（PAR）PP|Q（无）Γ ►0（REP） P你好！P（RES）Γ，x：TPΓ（νx）P（B-IN）r（z）=[T]r，x：TPrz（x）.P（B-OUT）Γ（z）=[T]Γ（x）=Trzx.PP表2π演算的基本类型赋值系统。注意，从定理2.2和规则（PAR）可以得出，如果P在环境Γ中不包含通信错误，则它的导数以及通过将P与关于相同环境的良好类型的其他进程并行组合而获得的系统也不包含通信错误在整个论文中，我们将重复使用符号，Γ，S，T：精确的含义将始终从上下文中清楚3通道序列类型3.1序列类型分配系统π演算的序列型赋值系统是基本型赋值系统的适当推广。在该新系统中，信道X可以是类型Pes{[T]1];. . ;[Tn]}，用对偶解释，x的类型有时是一个整数，因此， [T]=1 。 . [Tnnn[T1]n. . . 在序列中的类型的N[Tn]这一明显的奇怪性质可以通过考虑[3]中研究的名称作为输入或输出时的类型之间的对偶性来理解，并通过比较下面的规则（S-IN）和（S-OUT）与λ演算中并和交类型的经典消去规则。信道序列类型的正式定义如下：（S-T类型）S，T：：={[T1];. . . ;[T<$n]}，n≥0（T型环境）Γ：：= Γ，x：T|∅其中，a_c_h_n_m_x是一个简单的（possibly_emp_y）集合{[T_i];. . . ;[Tn]}，这些交换类型又是信道序列类型。为了可读性，我们将单例序列类型{[T]}写成[T]，并使用保留名称122S. Maffeis/Electronic Notes in Theoretical Computer Science 136（2005）117ω表示空集上的序列，其直观含义是相应的信道不能用于通信。 形式[T，[S]]的类型是通过通道的方式来实现功能的专用角色，对于可读性，有时会被T→S缩短。序列类型的类型分配系统由表2的规则给出，其中规则（B-IN）和（B-OUT）被替换为Γ（z）=π {[Tπ1];. . ;[T<$n] }i∈1.. n. Γ，x：TiP（S-IN）（S-OUT）rz（x）.PΓ（z）=π {[Tπ1];. . ;[T<$n] }i∈1.. n. Γ（x）=TiΓPrzx.P规则（S-IN）可以直观地解释为将规则（B-IN）应用于通道z的每个可能类型，并且规则（S-OUT）是对偶的，使用（B-OUT）在通信对象的至少一个可能类型类型系统在约简下保留类型，并保证类型良好的进程不会在通信中出错。定理3.1（i）若Γ <$P且P→Q，则Γ <$Q。（ii）如果Γ ≠P，则P/†。3.2示例我们展示了如何ω可以用来类型的条款，其中包含的潜在错误，只有在执行过程中无法到达的点例3.2（ω的相关性）过程x（y）。（zy）|z（w，y）.Q）可类型化，若Γ（x）=ω. 在这个假设下，永远不可能输入一个带有主语x的输出前缀，因为规则（S-O UT）要求x至少存在一个交换类型。 因此，这个过程永远不会减少到一个包含顶级通信错误的错误。相反，过程xy|例如，x=y：T，x：{[T]; [T，T]}可以被键入x y，y，但是没有一个试图在x上输入的进程可以被组合到这个进程，因为规则（S-I N）对由通道x绑定的变量的数量强加了两个不兼容的条件。因此，无法验证通信错误条件。 上述两个过程都不能在排除通信错误的π演算序列类型可以用来表示多态性，这并不奇怪。下面我们举两个具体的例子。例3.3（通用多态性）亲核的标准定义S. Maffeis/Electronic Notes in Theoretical Computer Science 136（2005）117123⎫cessId的行为类似于π演算中的恒等函数，由下式给出：！Id（x，y）.yx一个进程可以发送任何值v和一个新的通道z，并在z上接收相同的值v。上面的术语对于下面（νz）Id a，z.z（w）.P（νz）Idb，z.z（w）.Q但是如果a和b碰巧有不同的类型，那么它们的并行组合就不能在基本类型系统中类型化。直观地说，通道ID应该对所有类型T都是可类型化的，使得x：T和y：[T]。 使用序列类型，我们可以为任何（有限）类型集赋予一个类型。例如，我们证明了给定Γ={a：T，b：S，Id：T {T→T;S→S}}，上面给出的三个过程的合成是良型的：Γ（νz）Ida，z.z（w）.P|（νz）Idb，z.z（w）.Q|！Id（x，y）.y（1）我们展示了推导过程中有趣的部分Γ（νz）Id a，z.z（w）.Pby（T-PAR）（2）Γ1=Γ，z：[T]， Γ1∈Id ∈a，z∈.z（w）.Pby（T-RES）（3）Γ1（Id）=<${T→T;S→S}<$Γ1α：T，z：[T] ⎭（4）（）Γ1z（w）.PΓ（νz）Id b，z.z（w）.Qby（T-PAR）（5）r2= r，z：[S]，r2=Id b，z=.z（w）.Qby（T-RES）（6）Γ（Id）=<${T→T;S→S}<$2⎬Γ2πb：S，z：[S]⎭（7）（）Γ2z（w）.Q你好！Id（x，y）.yxby（T-P AR）（8）rId（x，y）.yxby（T-REP）124S. Maffeis/Electronic Notes in Theoretical Computer Science 136（2005）117{\fn（9）Γ（Id）=T→T;S→SΓ，x：T，y：[T] by（S-IN）（10）Γ，x：S，y：[S]S. Maffeis/Electronic Notes in Theoretical Computer Science 136（2005）117125关键点是（4）、（7）和（10）。在前两种情况下，我们只需要检查可能的元组T，[T]和S，[S]中的一个的沿着Id的通信参数，在后一种情况下，我们必须检查最终输出yx对于x，y假设的两种类型都是良好类型的，再次是T，[T]和S，[S]。例3.4（Ad-hoc多态性）在这个例子中，我们展示了在多态通道y上接收的值可以以两种不同的方式使用，这取决于它的类型。为了做到这一点，我们必须提供两个不同的实现（在这种情况下是z上的输出），并用一个输入（分别在1和2上）来保护它们中的每一个，用于识别多态值的特定类型（这里用w表示）。过程（v one，two）（y（z，x）. （xz）|one（z）.z a|二（z）.za，a）|yb，one|y=c，两个y）可以在环境中键入r =a：T，b：[T]，c：[T，T]，y：n {[T]→[T];[T，T]→[T，T]}例3.3和例3.4中给出的两个过程都可以在Turner [18]的多态系统中类型化;在第5节中我们展示了一个不能在该系统中类型化的例子。4λ演算的编码4.1λ-演算的严格交类型我们在下面报告了van Bakel关于λ演算的严格交集型赋值系统的定义，沿着[19]的路线我们从自然演绎风格中调整定义，并在交集中使用类型集，下面，让α是一个类型变量。（严格类型）τ：：= α|... ; τn} → τn≥ 0（S型）σ=τ {τ1;. ; τn}n≥ 0（B ASIS）B：：= B，x：σ|∅我们用ω表示空交集，并将τ写成τ {τ}。我们用B表示一个基，它是从变量到严格交的部分函数126S. Maffeis/Electronic Notes in Theoretical Computer Science 136（2005）117类型 严格推导是：（→E）BM：{τ1;. ; τn} → τN：τ1. N：τnBMN：τ（n≥0）B，x：σ<$M：τ（→I）B<$λ x.M：σ→τ（xE）B（x）=π {τ1;. ; τn}（n≥1，i∈ [1. n]）Bx：τi注意在规则（→I）中x可以有严格的交集类型σ。术语M对于基B有类型σ，记为B<$SM：σ，如果σ=ω，或者如果σ = π {τ1;. ; τn}，对于所有i∈ [1. n]，BM：τi.我们在下面报告了这个类型系统的一些有趣的性质（来自[19]）：(i) 项M有正规形当且仅当存在不含ω的B，σ，使得B<$SM：σ。(ii) 项M有首正规形当且仅当存在B，τ使得B<$M：τ。(iii) 一个项M是强可正规化的当且仅当存在B，σ使得B<$SM：σ和ω不出现在B，σ中或任何推导步骤中。4.2编码到π演算中下面我们报告按名称调用λ演算到π演算的无类型编码，如Ostheimer和Davie[14]所提出的。编码在连续通道a上是参数化的，该连续通道a用于传送评估项的结果。[[x]]a=xa[[λ x.M]] a=（νf）（a<$f <$|！f（x，b）. [[M]]b）[[MN]] a=（νb，x）（[[M]] b|b（f）. （fx，a|！x（c）.[[N]]c））我们给出了严格类型到序列类型的翻译，这是Turner [18]给出的基本类型的翻译的适当扩展（为了编码的目的，我们假设在我们的类型系统中也有类型变量α⟨⟨α⟩⟩=α我的天{τ1;. ; τn} → τ =[{[[τ1]];. ;[[τn]]}，[τ]]类型变量保持不变，而函数类型在包含参数类型的交集的编码的通道类型中转换为序列，其中每个类型是包含相应参数的编码的双重嵌套通道，以及包含S. Maffeis/Electronic Notes in Theoretical Computer Science 136（2005）117127结果类型的编码。基础和判断的翻译如下：⟨⟨B, x: ∩{τ1;... ; τn}=B，x：{[[τ1]];... ;[[τn]]}[[B M：τ]]a= B，a：[τ][[M]] a翻译保留类型，如下面的定理所述定理4.1如果B<$M：τ，则[[B<$M：τ]] a.证据 通过对M.(i) x：如果B≠x：τ，则规则（E）已被应用，我们知道，B = BJ，x：τ {τ1;. ;τn}，其中对于某些i，τ=τi。 我们需要证明⟨⟨BJ⟩⟩,x: ◦{[[⟨⟨τ1⟩⟩]];... ; [[τn]]}，a：[τ]xa，它遵循规则（S-OUT）。(ii) λ x.M：如果B=λ x.M：λ {τ1;. ;τn} →τ，则规则（→I）已经被应用，并且我们知道B，x：<${τ1;. ;τn}M：τ. 通过归纳假设，我们有：B，x：{[[τ1]];... ; [[τn]]}，b：[τ][[M]]b.我们需要证明，|！f（x，b）. [[M]]b）对于r=⟨⟨B⟩⟩,a: [[◦{[[⟨ ⟨τ1⟩ ⟩]];... ;[[τn]]}，[τ]]。通过（RES）它表面上显示其中r 1= r，f：[n {[[n n nτ1} n]];. ;[[τn]]}，[τ]] af|！f（x，b）.[[M]]b.根据规则（P AR）和（S-O UT），左边的术语是正确类型的。 通过规则（P AR）和（R EP）我们需要证明Γ 1<$f（x，b）。[[M]]b.由于f是一元交集，应用规则（S-IN），足以证明Γ 1，x：{[ ;[[τn]]}，b：[τ][[M]] b，这是通过对归纳假设进行弱化而得出的。(iii) M N：如果B<$M N：τ，则规则 （ →E ）已经被应用，并且我们有B<$M：τ {τ1;. ; τn} →τ，且对于所有i∈ [1. n]，BN：τi. 推理类似于前一种情况，非平凡点是规则（S-IN）在子项x（c）上的应用。[[N]]c其中x具有从函数参数导出的交集类型。 该规则要求使用从前提B<$N：τi导出的所有n个归纳假设。Q注4.2定理4.1意味着如果B∈SM：σ，其中σ=π {τ1;. ;τn}且n≥1，则我们也可以在π演算中通过定义πS来确定M的编码。另一方面，如果σ=ω，我们不能对M进行类型化，因为例如在变量项的情况下，我们在Γ中对x没有任何约束。正如van Bakel所指出的那样，在将一个项归约到其标准形式的过程中被删除的那些子项，以及不能以其他方式键入的那些子项，实际上需要ω。编码通过将ω分配给在约简期间将被简单地丢弃的输入变量来反映此属性，因为如所解释的那样，128S. Maffeis/Electronic Notes in Theoretical Computer Science 136（2005）117在例3.2中，ω可以用在π演算中，以避免键入已知永远不会被计算的输入的延续π-演算中的一个λ-项的编码可能会接收到与λ-演算类型的编码不同的类型，因为规则（RES）给出了自由度。然而，如果我们把π-演算系统中的每一个导子都赋给由应用的编码产生的限制名，则某些类型在λ-类型的映象中，我们也可以证明定理4.1的逆方向。定理4.3如果[[Bρ]和[[ρ1]];. ;[[<$$>ρn<$$>]]}，其中ρ是严格类型，则B <$M：τ。证据通过对M的归纳，类似于定理4.1的证明，使用关于可以为限制名称假设的类型Q前面的定理有一个有趣的结果，上面报道的严格类型分配系统的性质（1-3）可以转移到π-演算中的λ-项的图像。此外，由于编码保留了终止性[14]，在（3）的情况下，我们获得了一组终止π过程（编码图像中的那些）的基于类型的表征，其大小与所有强归一化λ项的集合一样大。进一步研究的一个有趣的主题将是直接表征可与序列类型（有和没有ω）相类型化的π备注4.4我们选择了Ostheimer和Davie的按名称调用（CBN）λ演算编码而不是Milner的编码，因为前者更接近Turner使用的优化按值调用（CBV）编码（已经在[ 11 ]中提到）。这两种编码在简单类型的λ-演算的情况下在π-项上导出不同的类型（参见[18]），但具有相似的性质。在序列类型的情况下，我们无法为优化的CBV编码定义类型化编码。问题出现在变量项的编码中，即[x]] a= a<$x<$。给定这个定义，判断x的类型：{τ1;. ; τn}x：τi不被保留，因为通信对象x比主体a具有更多的类型（与点(1)（定理4.1）。我们把它留给未来的工作，以调查米尔纳5多态归纳数据库众所周知（参见Milner [12]）如何在π演算中编码数据结构。例如，我们在下面报告列表和列表操作的编码S. Maffeis/Electronic Notes in Theoretical Computer Science 136（2005）117129”[18]《明史》：“。！零（r）。（v l）（rl| ！l（n，c）.n）！cons（h，t，r）. （v l）（rl|！l（n，c）.c h，t）！ccat（l，m，r）. （νn，c）（ln，c. （n.rm|c（h，t）。（v s）（ccatt，m，s）|s（res）。consh，res，r））过程（νr）nilr.r（l）.P为连续P创建一个新的空列表l。如果P依次是（νr）consh，l，r.r（m）.Q，那么Q知道一个名为m的列表，它的第一个元素是h，尾部是空列表！l（n，c）.可以使用上面给出的操作ccat在通常的π演算方法中，递归类型对于类型列表2是必要的。此外，即使列表上的所有操作都是通用的，并且适用于任何类型的数据对象，π演算的简单递归类型系统一次只能为一种数据类型输入操作。 例如，它将排除（完全合理的）术语（v intr，strr）（ccatint 1，intl 2，intr int n）|ccat字符串strl 1、strl 2、strr|P）其中P可以从intr接收两个整数intl1、intl 2列表的级联，并且从strr接收两个字符串strl1、strl 2列表的级联。在我们的类型系统中，可以对这个项进行类型检查，例如在环境Γ中，r（cca，t）=r（{l，L（h，k）}）|0≤h≤m，0≤k≤n}{SL（h，k）} |0 ≤ h ≤ i，0 ≤k ≤ j}）Γ（intl 1）= IntLn Γ（intl 2）=IntLmΓ（srtll）=StrLiΓ（strl2）=StrLj在这里我们使用了IL（h，k）=（IntLh，IntLk）→IntLh+kSL（h，k）=（StrLh，StrLk）→StrLh+k序列类型赋予我们表达无限多态性的能力，归纳数据结构[2] Turner在[ 18 ]中指出，Church编码的列表（很难被视为列表本身，因为选择尾部不是常数时间操作）可以在多态π演算中类型化，而不使用递归类型。130S. Maffeis/Electronic Notes in Theoretical Computer Science 136（2005）1176结论和今后的工作我们已经引入了π演算通道的序列类型的概念，由于通道类型的内在对偶性，它扮演了交集和并集类型的角色。我们已经证明了一个Curry类型的赋值系统享有主题归约，并保证没有通信错误，我们已经给出了与此纪律的条款类型的例子我们已经给出了严格相交类型的λ演算的保型编码，导出了一个相当大的终止π项集（从计算上讲）的基于类型的特征：这些终止π项是由强规范化λ项的编码产生的。这暗示了我们的类型系统的不确定性.我们已经证明了序列类型可以用于归纳定义的多态数据结构。我们把它留给未来的工作，主要类型和decidabil性质的正式研究Pierce [15]之后，一种加强可判定性的方法是采用类型化系统（Church风格），用类型注释限制和输入变量。或者，秩2交集类型已经被研究，例如在[22]中作为交集类型化学科的可判定限制，其仍然享有许多有趣的性质。我们系统的秩2的相应概念可以直接定义，秩2的交集类型可以转换为相同秩的序列类型。我们猜想定理4.1和定理4.3的一个类似的成立，但我们把它留给未来的工作，以研究限制子系统的形式性质我们研究交叉类型的最初动机是试图为eπ演算[4]给出一个有表现力的结构类型系统，e π演算是π演算的一个扩展，其中通道由名称向量（同步向量）标识。在eπ中，一个自然的选择可以是用构成同步向量的名称的类型的交集来键入信道我们希望这条线的研究是有前途的，鉴于能力的演算编码忠实的密码原语和分布式演算。在Ambient演算的背景下研究序列类型也是有趣的，特别是与Amtoft等人 [1]关于ML-样多态性的工作进行比较（其中主要类型仅适用于Ambients的限制性片段），并且其中形状类型的使用可以被视为这是一种无限多态的形式。除了引言中提到的滤波器模型的定义[8，6]之外，这项工作构成了过程演算中交叉类型的第一个研究，我们希望这将成为该领域进一步研究的灵感。S. Maffeis/Electronic Notes in Theoretical Computer Science 136（2005）117131致谢。这项工作的灵感来自于与Ste Escheren van Bakel关于eπ演算的polyadic同步类型我感谢匿名推荐人提供的有益意见和建议。引用[1] Amtoft，T.，H. Makholm 和J. Wells，Polya：移动环境的真型多态性，技术报告HW-MACS-TR-0015数学和计算机科学学院Heriot- Watt大学。出现在IFIP-TCS'04的会议记录中（2004年）。[2] Barendregt ， H. ， M. Coppo 和 M. Dezani-Ciancaglini ， A filter lambda model and thecompleteness of type assignment，Journal of Symbolic Logic48（1983），pp. 931-940[3] 伯杰，M.，K. Honda和N. Yoshida，Genericity and the pi-calculus，2620.[4] Carbone ， M. 和 S. Ma Joueis ， 关 于 π- 演 算 中 多 进 同 步 的 表 达 能 力 ， Nordic Journal ofComputing10（2003），pp. 70比98[5] Coppo，M.和M.Dezani-Ciancaglini，基本功能理论的扩展，λ-演算，Notre-Dame Journal of Formal Logic 21（1980），pp. 685-693.[6] Coppo，M.和M. Dezani-Ciancaglini，高阶移动环境的完全抽象模型，在：VMCAI255-271。[7] Coppo ， M. ， M. Dezani-Ciancaglini 和 B. Venneri ， 可 解 项 的 函 数 特 征 ， Zeitschrift furMathematische Logik und Grundlagen der Mathematik（1981），pp.45-58.[8] Damiani，F.，M. Dezani-Ciancaglini和P. Giannini，移动过程的过滤器模型，计算机科学中的数学结构9（1999），pp. 63比102[9] 盖伊，S。J.，一个多进π演算的排序推理算法，在：第20届ACM SIGPLAN-SIGACT编程语言原理研讨会论文集（1993年），pp。429-438.[10] Liu，X.和D. Walker，A polymorphic type system for the polyadic pi-calculus，in：Proceedingsof the 6th International Conference on Concurrency Theory（1995），pp. 103-116[11] 米尔纳河，作为进程运行，INRIA RR-1154。（《计算机科学中的数学结构》2（2），1992年修订版）。（1990年）。[12] 米尔纳河，多进π-演算：教程，在：逻辑和代数的规范，施普林格出版社，海德堡，1993年。[13] 米尔纳河，J. Parrow和J.Walker，A calculus of mobile processes，I and II，Informationand Computation100（1992），pp.1比40，41比77。[14] Ostheimer，G. K.和A. J. T. Davie，π-演算刻画一些实用的λ-演算约简策略，技术报告CS/93/14，圣安德鲁斯大学数学与计算科学系（1993）。[15] 皮尔斯湾C.的方法，“交叉类型和有界多态性编程”，博士。Carnegie Mellon University（1991）.[16] 皮尔斯湾C.和D. Sangiorgi，多态π演算中的行为等价，J。ACM47（2000），pp. 531-584.[17] 雷 诺兹 ，J.C. ，程 序设 计语 言的 初步 设计 ， 技术 报告 CMU-CS-88-159 ， 卡内 基梅 隆大 学（1988）。[18] Turner，D. N.，“多态Pi演算：理论与实现”，博士。论文，爱丁堡大学（1995年）。132S. Maffeis/Electronic Notes in Theoretical Computer Science 136（2005）117[19] van Bakel，S.，交叉类型学科的完全限制，理论计算机科学（1992），pp. 135-163。[20] van Bakel，S.，严格类型赋值系统的主类型方案，逻辑与计算杂志3（1993），pp. 643-670。[21] van Bakel，S.，Intersection type assignment systems，Theoretical Computer Science（1995），pp. 385-435[22] van Bakel，S.，Rank 2 intersection type assignment in term rewriting systems，FundamentaInformatica2（1996）.[23] Vasconcelos，V.T.，Pi演算中的谓词多态性，在：并行架构和语言欧洲，1994年，pp。425-437[24] Vasconcelos，V. T.和K.本田，主要的打字计划在一个polyadic π演算，在：第四届并发理论国际会议论文集（1993年），pp。524-538A受试者减少和安全性引理A.1（加强）若Γ，x：T<$P且x/∈fn（P）则Γ <$P.引理A.2（弱化）如果Γ <$P，则对任意类型T和任意x/∈ dom（Γ），Γ，x：T<$P。前面的两个引理都很容易通过P上的结构归纳得出。引理A.3（代换引理）如果Γ，x：T≠ P且r（y）= T，则r，x：TP {y/x}.证据 通过对P.• 0：基本情况，平凡。• P|Q：使用P和Q的归纳假设和规则（P AR）。• ！病人：微不足道。• （νz）P：给定Γ，x：T（νz）P和Γ（y）=T首先我们把z转化为新的名字w。根据规则 （ RES ），对于某个类型S，我们有Γ，x：T，w：S<$P{w/z}，并通过归纳假设Γ，x：T，w：S<$P{w/z}{y/x}，通过（RES）和α转换，我们得到了Γ，x：T<$（νz）P{y/x}，其中我们使用了w是新的这一事实。• zw.P：通过句法推理，使用规则（S-O ut）的最右前提的归纳假设。• z（w）.P：结合前两点。Q引理A.4（主同余）如果Γ <$P且P<$Q则Γ <$Q。证据 通过归纳法，对“无”的定义进行了归纳。 我们证明了（νz）（P|Q）P|（νz）Q，其中z/∈fn（P），因为其它的都很容易. 从Γ ε（νz）（P|Q）S. Maffeis/Electronic Notes in Theoretical Computer Science 136（2005）117133根据规则（RES），对于某种类型S，我们有：|Q，通过规则（PAR）我们有，Γ，z：S<$P和Γ，z：S<$Q，通过引理A.1我们得到Γ <$P。 利用（R ES）我们得到了Γ（νz）Q，利用（P AR）我们得出了Γ P|（νz）Q.另一个方向是对称的，并且使用弱化而不是增强。Q主语归约（定理2.2.i）。若Γ <$P且P→Q，则Γ <$Q。证据 通过对P → Q推理深度的归纳。• （COM）：supposey（xn）.P|y<$z<$n<$.Q −→P{z<$n/x<$n} |Q和Γy（x<$n）.P|我也是。Q. By（PAR）有一个very（x<$n），P和rrry<$z<$n<$.Q.By（S-OUT）wever（y）=r {[T1];. . . ;[T<$m]}，Γ（z<$）=T<$i，且dΓ <$Q. By（S-IN）wealsover，x∈：T∈j∈P，对于n，y，j，特别是f或i。通过应用引理a（引理aA.3），我们得到了Γ，x∈：T∈j∈P{z∈/x∈}，并且由ys加强和d（PAR），我们得到了ΓP{z<$n/x<$n} |Q.•（C-RES）：通过（RES），归纳假设，再通过（RES）。•（C-P AR）：通过（P AR），归纳假设，再通过（P AR）。•（结构）：通过引理A.4，归纳假设，再通过引理A.4。Q安全性（定理2.2.ii）。如果Γ ≠P，则P/†。证据我们证明了对所有的P，如果P<$，则不存在使得Γ<$P的Γ。通过定义− <$wehavethatP<$（vz<$）（P1|y（x<$n）.R|你知道的。Q）Wheeem n. 我们用矛盾来说明假设r∈P，根据引理A.4，我们将证明了：Γ_∞（νz_∞）（P1|y（x<$n）.R|你知道的。Q）。 分别使用（RES）和（PAR）我们得到了规则（S-IN）和（S-OUT）的两个子导子，分别得到了结论：r∈yr∈y（x∈n）.R和r∈yr∈w∈m. Q. both规则的第一个条件是强制y具有唯一性pe{[T]1];. . ;[Tj]}. 通过（S-IN）的第二个条件所有这些T恤都必须具有相同的，准确地说，为了与xn匹配，但通过（S-Out）的第二个条件，我们不满足xh，有元数m，因此假设m n是矛盾的。 如果y有类型ω，则不可能导出（S-OUT）的第二个先决条件。Q