Gödel 系统 T 的 Gentzen 风格单子翻译
计算机科学中的逻辑
2020-05-06 v2 编程语言
逻辑
摘要
我们引入一种由弱单子概念参数化的 Gödel 系统 T 的语法翻译，并证明相应的逻辑关系式基本定理。我们的翻译在结构上对应于经典逻辑的 Gentzen 负翻译。通过实例化单子与逻辑关系，我们揭示了 T 可定义泛函的著名性质与结构，包括可优性、连续性与杆递归。我们的开发已在 Agda 证明助手中形式化。
关键词
引用
@article{arxiv.1908.05979,
title = {A Gentzen-style monadic translation of G\"odel's System T},
author = {Chuangjie Xu},
journal= {arXiv preprint arXiv:1908.05979},
year = {2020}
}
备注
17 pages. Changes: (1) remove the restriction of satisfying the monad laws in the definition of nuclei, (2) add a unified theorem of logical relation. This paper will appear in FSCD 2020