| 研究課題/領域番号 |
17K00005
|
|---|
| 研究機関 | 千葉大学 |
|---|
研究代表者 |
桜井 貴文 千葉大学, 大学院理学研究院, 教授 (60183373)
|
|---|
| 研究分担者 |
菊池 健太郎 東北大学, 電気通信研究所, 助教 (40396528)
|
|---|
| 研究期間 (年度) |
2017-04-01 – 2021-03-31
|
| キーワード | 古典論理 / 直観主義論理 / ラムダ計算 / 証明検証系 / minlog |
|---|
| 研究実績の概要 |
本研究の目的は古典論理に基づく計算系に関する様々な性質を研究することであるが、本研究代表者は、これまでの研究で古典論理の計算系を型付ラムダ計算に翻訳する新しい変換を考え、その変換が簡約を保存するという性質を持つことを示した。具体的には、古典論理の計算系 lambda-bar-mu やその変種の lambda-bar-mu-tilde-CBN を lambda-conj-neg に翻訳する変換および lambda-conj-neg を型付ラムダ計算に翻訳する簡単な変換を考え、それらの変換を合成することで新しい変換を得ることができた。本研究では、それらの古典論理の計算系から型付ラムダ計算への翻訳に関する性質を計算機上の証明検証系で証明することを最初の目標としており、そのためにminlogという証明検証系を使っている。
本研究代表者は「クラス理論に基づく自己拡張可能なソフトウェア検証体系の深化」(代表者:佐藤雅彦)という科研費の研究課題の分担者になっているが、その研究課題では、ラムダ計算を改良・発展させた計算系を開発するためにminlogを使ってその計算系の性質を証明している。その研究課題でminlogを使って表現しているのはラムダ計算を本質的に含んでいる計算系なので、古典論理の計算系 lambda-bar-mu の表現とも共通部分は多い。したがって、その研究で開発している技術は本研究に応用できるという見込みの下にその分担研究課題に取り組んでいたが、29年度に困難にぶつかった。しかし30年度にその困難を解決できたので、31年度はその成果を本研究へ応用できる状態になった。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
4: 遅れている
理由
証明検証系minlogを用いた検証をまず行う予定であったが、29年度にその基となるであろうと見込んでいた部分の一部(具体的にはeta変換と呼ばれる変換の扱い方)で思いのほか手間取り、30年度に解決できた状態である。したがって、当初の目的であった簡約の性質の検証の段階にまで至ってない。
また、当初の研究計画では明示的代入計算に関する研究はもう少し後で取り組む予定であったが、分担者として行っている研究との関わりが出てきたので、計画を前倒しして、明示的代入計算をminlogを使って表現してその性質を証明することにも取りかかった。そして、上記の困難の解決に関連して、伝統的なラムダ計算の表記を含む体系を考えて体系を構築しつつあるので、それと共通して作業をすることができるようになった。
|
| 今後の研究の推進方策 |
まず、証明検証系minlogを用いて古典論理の計算系から型付ラムダ計算への翻訳に関する性質の検証に引き続き取り組む。minlogによるラムダ計算の表現は一応できているので、その部分は固定してもしくは変更があっても大丈夫な形にして、次の段階つまり翻訳の性質の証明を行う。
次に、30年度に行う予定であった、明示的代入計算に関する研究に取り掛かる。明示的代入計算をminlogを使って表現しておくと簡約過程を計算機上で実行することができるので、確認しながら設計や証明を進めやすくなることがこれまでの経験で判明した。そしてその性質を証明することにも取りかかり、簡約過程を抽象機械上実行とみなすことを考える。抽象機械もminlogで表現することにより、この対応をうまく表現できることが期待できる。
また可能ならば、将来証明系を作るための準備として、関数型言語HaskellによるGUIの作成方法について予備的な実験を開始する。
|
| 次年度使用額が生じた理由 |
29年度に直面した困難を解決するのに30年度一杯かかってしまったため、ハードウェアは必要としなかった。
使用計画としては、30年度に購入する予定であった計算機を購入するつもりである。
|
