Safety and conservativity of definitions in HOL and Isabelle/HOL
Safety and conservativity of definitions in HOL and Isabelle/HOL
复制标题
HOL 和 Isabelle/HOL 中定义的安全性和保守性
DOI：
10.1145/3158112
复制
发表时间：
2018
影响因子：
--
通讯作者：
Andrei Popescu
中科院分区：
文献类型：
--
作者：
Ondřej Kunčar;Andrei Popescu
传统上，定义被认为是在已知一致的逻辑之上引入概念的安全机制。与任意公理相反，定义原则上应该被视为一种缩写形式，因此可以在不失去可证明性的情况下远离理论进行编译。特别是，定义应该形成纯逻辑的保守延伸。这些属性对于现代交互式定理证明器至关重要，因为它们确保了逻辑的一致性，以及完整/认证函数式编程的有效环境。我们为高阶逻辑（HOL）证明了这些属性，即安全性和保守性，高阶逻辑（HOL）是一种在多个主流定理证明器中实现并受到数千用户依赖的逻辑。 HOL 的一些独特功能，例如在定义新类型时要求提供非空证明以及无法展开类型定义，使得这些属性的证明以及安全性的制定变得非常重要。我们的研究还考虑了 Isabelle/HOL（基于 HOL 的证明者家族的流行成员）所提出的 HOL 定义的本质变化。当前的工作对最近的结果进行了改进，该结果表明 Isabelle/HOL 定义的属性和一致性较弱。
Definitions are traditionally considered to be a safe mechanism for introducing concepts on top of a logic known to be consistent. In contrast to arbitrary axioms, definitions should in principle be treatable as a form of abbreviation, and thus compiled away from the theory without losing provability. In particular, definitions should form a conservative extension of the pure logic. These properties are crucial for modern interactive theorem provers, since they ensure the consistency of the logic, as well as a valid environment for total/certified functional programming.We prove these properties, namely, safety and conservativity, for Higher-Order Logic (HOL), a logic implemented in several mainstream theorem provers and relied upon by thousands of users. Some unique features of HOL, such as the requirement to give non-emptiness proofs when defining new types and the impossibility to unfold type definitions, make the proof of these properties, and also the very formulation of safety, nontrivial.Our study also factors in the essential variation of HOL definitions featured by Isabelle/HOL, a popular member of the HOL-based provers family. The current work improves on recent results which showed a weaker property, consistency of Isabelle/HOL's definitions.
登录
查看更多内容
DOI：
10.1007/11805618_16
发表时间：
2006
期刊：
Arch. Formal Proofs
影响因子：
--
作者：
Steven Obua
通讯作者：
Steven Obua
阿朗佐教堂
影响因子：
0.6
作者：
R. Shore
通讯作者：
R. Shore
DOI：
10.1016/j.entcs.2018.10.009
发表时间：
2018
期刊：
Journal of Automated Reasoning
影响因子：
--
作者：
A. Gengelbach;Tjark Weber
通讯作者：
Tjark Weber
基于 FOAS 的 HOAS 对系统 F 的强标准化
DOI：
10.1109/lics.2010.48
发表时间：
2010
期刊：
2010 25th Annual IEEE Symposium on Logic in Computer Science
影响因子：
--
作者：
A. Popescu;Elsa L. Gunter;Christopher J. Osborn
通讯作者：
Christopher J. Osborn
具有绑定和替换的语法的递归原则
DOI：
10.1145/2034773.2034819
发表时间：
2011
期刊：
Proceedings of the 16th ACM SIGPLAN international conference on Functional programming
影响因子：
--
作者：
A. Popescu;Elsa L. Gunter
通讯作者：
Elsa L. Gunter