Journal of Software
1000-9825
1997
8
5
321
326
article
π-演算中无卫递归的消除
ON REMOVING UNGUARDED RECURSIONS IN THE π CALCULUS
本文提出消除π－演算中无卫递归的公理，证明了将该公理加入到正则π－演算受卫递归子集上的证明系统后，所得到的证明系统在π－演算全体正则子集上关于互模拟等价的可靠性和完备性.
Axioms for removing unguarded recursions in the π calculus are proposed. It is shown that these two axioms are sound with respect to bisimulation equivalence, and are sufficient to reduce any unguarded recursively defined processes into guarded forms. Hence, by adding these axioms to the proof systems for guarded regular π calculus, complete proof systems for the whole regular π calculus are obtained.
进程代数; π－演算; 互模拟; 递归进程; 证明系统;
Process algebras; π calculus; bisimulation; recursive; processes; proof systems.;
林惠民
LIN Huimin
jos/article/abstract/19970501