Pi演算的一种变例及其开互模拟

摘要

开互模拟关系是一种特殊的且非常重要的互模拟等价关系,它将替换嵌入到定义中去,这使得它本质上就是一个同余关系,而不需要像迟、早互模拟同余关系那样进行额外的定义.本文把变量和通道当作两种不同的名来进行处理,只有变量可以被实例成通道名,而不同的通道名永远都不会相等,这使得开互模拟关系的定义非常简单.本文的主要贡献在于给出了这种开互模拟关系的公理化系统,并对其完备性进行了证明.