非对称^(χ≠)-演算的基同余

The Ground Congruence for Asymmetric ^(χ≠)-Calculus

该文研究非对称χ≠-演算的基同余.文中引入一组L-互模拟关系,并确定基互模拟就是由L-互模拟定义导出的12个互异的互模拟关系中的最小关系,给出了某些L-互模拟的开模拟性质,利用开模拟性质引入开基互模拟概念,并证明开基互模拟与基互模拟是一致的,构造了基于基同余的可靠和完备的等式系统,最后给出了基同余的完备性定理.

This paper studies the ground congruence on asymmetric χ^≠-processes. L-bisimilarities on asymmetric χ^≠-processes are introduced. The ground bisimilarity in asymmetric χ^≠- calculus is ascertained to be equal to the bottom element among all of L-bisimilarities. Some open simulation properties of L-bisimilarities are exposed. Then an open version of the ground bisimilarity based on open simulation properties is introduced and the two relations are proved to coincide. A sound and complete equational system is constructed for the ground congruence. Finally a complete theorem based on the open version is proved for the ground congruence.