一句话：首次系统定义并证明 HOL 中 Types-to-PERs 相对化的可容许性，并实现 Isabelle 按需相对化工具。
在 HOL4、HOL Light 和 Isabelle/HOL 等基于 HOL 的交互式证明器中，将基于类型的陈述相对化到集合上可提升证明效率，但此前缺乏统一定义与可容许性分析。本文首次系统研究 HOL 的 types-to-sets 相对化，并推广为 types-to-PERs（偏等价关系）形式。作者证明，在包含数据类型与余数据类型等容器类型的实用 HOL 片段中，types-to-PERs 相对化是可容许的：原类型化陈述可证则其 PER 化对应陈述可证。该结果还蕴含带局部类型定义的 HOL 公理扩展可容许。作者将相对化实现为 Isabelle 工具，可按需对 HOL 定理执行相对化。
Relativizing statements in Higher-Order Logic (HOL) from types to sets is useful for improving productivity when working with HOL-based interactive theorem provers such as HOL4, HOL Light and Isabelle/HOL. This paper provides the first comprehensive definition and study of types-to-sets relativization in HOL, done in the more general form of types-to-PERs (partial equivalence relations). We prove that, for a large practical fragment of HOL which includes container types such as datatypes and codatatypes, types-to-PERs relativization is admissible, in that the provability of the original, type-based statement implies the provability of its relativized, PER-based counterpart. Our results also imply the admissibility of a previously proposed axiomatic extension of HOL with local type definitions. We have implemented types-to-PERs relativization as an Isabelle tool that performs relativization of HOL theorems on demand.
@article{paperbot2072,
title = {Admissible Types-to-PERs Relativization in Higher-Order Logic},
author = {Andrei Popescu and Dmitriy Traytel},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {POPL},
year = {2023},
doi = {10.1145/3571235}
}