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

点击翻译按钮获取中文摘要

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