行为与共归纳重写：理论计算机科学的高效实现

"这篇文档是理论计算机科学电子笔记的一部分，主要探讨了行为重写和循环共归纳重写这两个概念，作者是Joseph Goguen、Kai Lin和Grigore Roșu，他们来自加州大学圣地亚哥分校的计算机科学与工程系。这篇论文是一个邀请演讲的记录，详细介绍了如何利用标准重写实现行为重写，并展示了它们在验证行为性质方面的应用，特别是在BOBJ系统中的实现。" 在计算机科学中，行为重写 是一种推理规则，它不局限于传统的逻辑规则，而是关注于行为逻辑的较弱推理。行为重写与标准重写共享一些概念，如终止性和连续性，但它的焦点在于处理无限数据结构、行为细化和共归纳证明。行为规范 是用来定义模型（即实现）必须符合的逻辑要求，它可以区分可见和隐藏的行为，确保在特定的不可否认性意义上，可见行为的平等性是严格的。 共归纳重写 是一种证明行为等价性的算法，它结合了行为重写和循环共归纳的概念。这种方法允许在证明过程中使用共归纳假设，增强了与归纳的对偶性。循环共归纳重写在实际应用中表现出强大的能力，即使没有完整的算法也能完成某些证明。在BOBJ系统中，这种重写策略被用于自动化地生成共基，并处理系统的并发连接。 这篇论文中提到的研究受到了美国国家科学基金会和日本信息促进机构（IPA）的资助，特别是IPA的CafeOBJ项目，该项目属于其高级软件技术计划的一部分。尽管篇幅有限，论文省略了部分证明和定义，但假设读者对代数规范、定理证明以及OBJ语言有一定的了解。在论文中，作者使用BOBJ系统展示了一些例子，包括不同类型的惰性函数流程序的等价性。 这篇论文为读者提供了深入理解行为重写和循环共归纳重写技术的窗口，强调了这些技术在理论计算机科学和计算工程中的重要应用，特别是在验证和比较复杂系统行为时的能力。