2020 Fiscal Year Research-status Report
| Project/Area Number |
17K00005
|
|---|
| Research Institution | Chiba University |
|---|
Principal Investigator |
桜井 貴文 千葉大学, 大学院理学研究院, 教授 (60183373)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
菊池 健太郎 東北大学, 電気通信研究所, 助教 (40396528)
|
|---|
| Project Period (FY) |
2017-04-01 – 2022-03-31
|
| Keywords | 古典論理 / 直観主義論理 / ラムダ計算 / 証明検証系 / minlog |
|---|
| Outline of Annual Research Achievements |
本研究の目的は古典論理に基づくの計算系に関する様々な性質を研究することであるが、本研究代表者は、これまでの研究で古典論理の計算系を型付ラムダ計算に翻訳する新しい変換を考え、その変換が簡約を保存するという性質を持つことを示した。具体的には、古典論理の計算系 lambda-bar-mu やその変種の lambda-bar-mu-tilde-CBN を lambda-conj-neg に翻訳する変換および lambda-conj-neg を型付ラムダ計算に翻訳する簡単な変換を考え、それらの変換を合成することで新しい変換を得ることができた。本研究では、それらの古典論理の計算系から型付ラムダ計算への翻訳に関する性質を計算機上の証明検証系で証明することを最初の目標としており、そのためにminlogという証明検証系を使っている。
本研究代表者は「クラス理論に基づく自己拡張可能なソフトウェア検証体系の深化」(代表者:佐藤雅彦)という科研費の研究課題の分担者になっているが、その研究課題では、ラムダ計算を改良・発展させた計算系を開発するためにminlogを使ってその計算系の性質を証明している。さらにその研究課題ではminlogを使ってその計算系と伝統的ラムダ計算の関係を明かにした。伝統的ラムダ計算は古典論理の計算系 lambda-bar-mu に含まれるので、その研究で開発している技術は本研究に応用できるという見込みの下にその分担研究課題に取り組んでいる。令和2年度までに伝統的なラムダ計算について様々な性質を証明することができたので、3年度はその成果を本研究へ応用できる状態になった。
|
| Current Status of Research Progress |
Current Status of Research Progress
4: Progress in research has been delayed.
Reason
古典論理の計算系について、証明検証系minlogを用いた検証をまず行う予定であったが、令和元年度は先に伝統的ラムダ計算について集中して検証を行ったが、さらに2年度にその研究を深める必要が生じた。したがって、当初の目的であった古典論理の計算系の簡約の性質の検証の段階にまで至ってない。
また、当初の研究計画では明示的代入計算に関する研究はもう少し後で取り組む予定であったが、分担者として行っている研究との関わりが出てきたので、一昨年度から計画を前倒しして、明示的代入計算をminlogを使って表現してその性質を証明することにも取りかかった。具体的には、伝統的ラムダ計算におけるβ簡約の過程を細いステップに分割して規則にするのが明示的代入計算であるが、minlogにおいてβ簡約を計算する関数の代わりに明示的代入計算の規則による導出をデータの形で表現することにより、両者を同じ枠組の中で表現して、それらの関係について述べることができるのである。概要で述べた分担者としての課題においては、伝統的なラムダ計算を含む体系を考えて体系を構築したので、そこで使った技法を応用して体系を表現することができるようになった。
|
| Strategy for Future Research Activity |
基本的は、令和2年度にできなかった部分を遂行する方針である。
まず、証明検証系minlogを用いて古典論理の計算系から型付ラムダ計算への翻訳に関する性質の検証に引き続き取り組む。minlogによる伝統的ラムダ計算の実現はできているので、その部分は固定してもしくは変更があっても大丈夫な形にして、次の段階つまり翻訳の性質の証明を行う。
次に、令和2年度に行う予定であった、明示的代入計算に関する研究に取り掛かる。明示的代入計算をminlogを使って表現しておくと簡約過程を計算機上で実行することができるので、確認しながら設計や証明を進めやすくなることがこれまでの経験で判明した。そしてその性質を証明することにも取りかかり、簡約過程を抽象機械上実行とみなすことを考える。抽象機械もminlogで表現することにより、この対応をうまく表現できることが期待できる。そしてこの抽象機械を使って古典論理の計算系における計算を表現することを考える。
また可能ならば、将来証明系を作るための準備として、関数型言語HaskellによるGUIの作成方法について予備的な実験を開始する。
|
| Causes of Carryover |
令和2年度は、コロナに対応するためにオンライン講義の準備に忙殺されたのに加え、病気が再発し充分に研究時間が取れなかった。
使用計画としては、2年度に購入する予定であった計算機を購入するつもりである。
|
