Up-to techniques' represent enhancements of the coinduction proof method and are widely used on coinductive behavioural relations such as bisimilarity. Abstract formulations of these coinductive techniques exist, using fixed-points or category theory. A proposal has been recently put forward for transporting the enhancements onto the concrete realms of inductive behavioural relations, i.e., relations defined from inductive observables, such as traces or enriched forms of traces. The abstract meaning of such 'inductive enhancements', however, has not been explored. In this paper, we review the theory, and then propose an abstract account of it, using fixed-point theory in complete lattices.
翻译:"上至技术"代表共归纳证明方法的增强,并广泛应用于共归纳行为关系(如互模拟性)。这些共归纳技术存在使用不动点或范畴论的抽象表述。最近有研究提出将这些增强技术移植到归纳行为关系的具体领域,即从归纳可观测对象(如迹或迹的丰富形式)定义的关系。然而,此类"归纳增强"的抽象含义尚未得到探讨。本文回顾相关理论,随后利用完备格中的不动点理论,提出其抽象化描述框架。