通过偏伽罗瓦连接与等价进行程序迁移

多种类型可表示同一概念。例如，列表与树均可表示集合。遗憾的是，这易导致不完备的库：某些集合操作可能仅见于列表，另一些仅见于树。类似地，在形式化验证中，子类型与商类型常用于构造新的类型抽象。此类情形下，人们往往希望将表示类型上的操作复用于新类型抽象，却徒劳无功：类型并不相同。为解决这些问题，我们提出一个通过等价迁移程序的新框架。现有迁移框架或面向依赖类型构造性证明助手，或使用单值性，或仅限于偏商类型。我们的框架（1）面向简单类型论设计，（2）推广了先前基于偏商类型的方法，（3）基于标准数学概念，尤其是伽罗瓦连接与等价。我们引入偏伽罗瓦连接与等价的概念，并证明其在（依赖）函数关系器、（协）数据类型与复合下的闭包性质。我们在 Isabelle/HOL 中形式化了该框架并提供了原型。本文为“Transport via Partial Galois Connections and Equivalences”（第 21 届亚洲编程语言与系统研讨会，2023）的扩展版。