古典論理に基づく計算系とその性質の検証

基于经典逻辑的计算系统及其属性的验证

基本信息

批准号：
17K00005
负责人：
桜井貴文
金额：
$ 2.5万
依托单位：
Chiba University
依托单位国家：
日本
项目类别：
Grant-in-Aid for Scientific Research (C)
财政年份：
2017
资助国家：
日本
起止时间：
2017-04-01 至 2024-03-31
项目状态：
已结题

来源：
https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-17K00005/
关键词：
古典論理ラムダ計算 α同値証明検証系 minlog 直観主義論理数理論理学検証

项目摘要

本研究の目的は古典論理に基づくの計算系に関する様々な性質を研究することであるが、本研究代表者は、これまでの研究で古典論理の計算系を型付ラムダ計算に翻訳する新しい変換を考え、その変換が簡約を保存するという性質を持つことを示した。具体的には、古典論理の計算系 lambda-bar-mu やその変種の lambda-bar-mu-tilde-CBN を lambda-conj-neg に翻訳する変換および lambda-conj-neg を型付ラムダ計算に翻訳する簡単な変換を考え、それらの変換を合成することで新しい変換を得ることができた。本研究では、それらの古典論理の計算系から型付ラムダ計算への翻訳に関する性質を計算機上の証明検証系で証明することを最初の目標としており、そのためにminlogという証明検証系を使っている。本研究代表者は平成29年度に開始した「クラス理論に基づく自己拡張可能なソフトウェア検証体系の深化」(代表者:佐藤雅彦)という科研費の研究課題の分担者になっていたが、その研究課題では、ラムダ計算を改良・発展させた計算系を開発するためにminlogを使ってその計算系の性質を証明している。さらにその研究課題ではminlogを使ってその計算系と伝統的ラムダ計算の関係を明かにした。伝統的ラムダ計算は古典論理の計算系 lambda-bar-mu に含まれるので、その研究で開発している技術は本研究に応用できるという見込みの下にその分担研究課題に取り組んだ。令和3年度までに伝統的なラムダ計算について様々な性質を証明してきて一段落したと思ったが、令和4年度にα簡約が同値関係になるというよく知られた定理に新しい証明があることに気付き、その証明に取り組むことに注力した。

本研究的目的是研究基于经典逻辑的计算系统的各种性质，并证明该变换具有保持约简的性质。具体来说，经典逻辑计算系统 lambda-bar-mu 及其变体 lambda-bar-mu-tilde-CBN 被转换为 lambda-conj-neg，并且 lambda-conj-neg 被转换为类型化 lambda 演算。通过思考简单的变换来翻译和组合这些变换来获得新的变换。在这项研究中，第一个目标是使用计算机上的证明验证系统来证明与从经典逻辑计算系统到类型化 lambda 演算的转换相关的属性，为此，我们使用称为 minlog 的证明验证系统。。这项研究的主要研究者是 2017 年启动的题为“深化基于类理论的自扩展软件验证系统”的 KAKENHI 研究项目（代表人：佐藤正彦）的合作伙伴。在作业中，为了开发一个改进和发展 lambda 演算的计算系统，我们使用 minlog 来证明该计算系统的属性。此外，在那个研究项目中，我使用 minlog 来阐明该计算系统与传统 lambda 演算之间的关系。由于传统的 lambda 演算包含在经典逻辑的计算系统 lambda-bar-mu 中，因此我参与了这个共享研究项目，期望该研究中开发的技术可以应用于本研究。到 2021 年，我已经证明了传统 lambda 演算的各种性质，并认为它已经稳定下来，但到 2020 年，我发现著名定理 α 约简变成等价关系有了新的证明，他意识到了这一点并集中了他的注意力。努力证明这一点。