Proving Behavioural Apartness
arxiv(2024)
摘要
Bisimilarity is a central notion for coalgebras. In recent work, Geuvers and
Jacobs suggest to focus on apartness, which they define by dualising
coalgebraic bisimulations. This yields the possibility of finite proofs of
distinguishability for a wide variety of state-based systems.
We propose behavioural apartness, defined by dualising behavioural
equivalence rather than bisimulations. A motivating example is the
subdistribution functor, where the proof system based on bisimilarity requires
an infinite quantification over couplings, whereas behavioural apartness
instantiates to a finite rule. In addition, we provide optimised proof rules
for behavioural apartness and show their use in several examples.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要