π-演算中无卫递归的消除  

ON REMOVING UNGUARDED RECURSIONS IN THE π CALCULUS

作　　者：林惠民[1] 

机构地区：[1]中国科学院软件研究所

出　　处：《软件学报》1997年第5期321-326,共6页Journal of Software

基　　金：国家自然科学基金;中国科学院"九五"基础性研究重点项目

摘　　要：本文提出消除π－演算中无卫递归的公理，证明了将该公理加入到正则π－演算受卫递归子集上的证明系统后。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.

关 键 词：进程代数 Π-演算 互模拟 证明系统 无卫递归 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]