Y. Li/Electronic Notes in Theoretical Computer Science 138
(
2005
)
61
过程,并且这些转换描述了
在P
中
独立于操作变量的行为。
我们
将注意到
,
P
{
R/X
}
−
α
→
P
J
{
R/X
}
,
如果
P
−
α
→
P
J
在
我们的LTS。此外,我们还开发了一种
新的技术来探索开变量所在的上下文,该技术将分析P{R/X}仅由于R的副本
而导致的行为。注意,如果P=C[X],并且C是静态的,
co
n
t
ext,
nd
R
−
α
→
R
J
,
n
C
[
X
]
{
R/X
}
−
α
→
C
[
R
J
]
{
R/X
}
在我们
的
框架w
o
rk
中.
第三个目标是发展新的技术来解决
高阶微积分中
的困难问题,如同余问
题,因式分解定理,并以更直观的方式组织理论结构首先,我们把因子分解
定理作为一个比其他作者在高阶微积分中不同语义下更基本的结果直观地
说,这个结果告诉我们,可以通过使用触发器替换和私有资源来模拟高阶替
换我们直接证明了P{R/X}和νk(P{↑k/X}|k我们采用的技术与高阶替换的
细粒度公式密切相关它不再需要使用同余性质,这表明因子化定理是高阶微
积分中一个相当独立的结果。
进一步证明了高阶代换的同余性质,
因式分解定理的简单推论
本文的其余部分组织如下:第2节陈述了本文将考虑的演算的语法第三节
详细阐述了我们语言的归约语义,以及我们研究上下文标记语义第4节详细
说明了上下文标记的转换语义,并介绍了演算中相应的互模拟
。第
五节证明了
互模拟的因子分解定理和同余性质。第6节将展示我们的标记转换语义和归
约语义之间的对应关系第七部分是结论及相关工作。
2
语法
我们探索的语言类似于Sangiorgi在[8]中提出的高阶π-演算的第二个片段,
它满足以下限制:(1)所有对象都是一元的,(2)每个过程都是有限可描
述的,(3)只允许有保护的选择,(4)只允许过程传输(或者过程是唯一
的通信值)。 在这个演算中,可以避免复制,因为递归和复制可以在我们的
演算中使用限制和并行组合来模拟
,
如Alfresen [5]所示
。
但为了方便起
见,我们引入了所谓的资源程序k P
,
它是一个被k永远引用的服务器进程,
并在被引用后生成P的副本-