| 研究課題/領域番号 |
17K00005
|
|---|
| 研究機関 | 千葉大学 |
|---|
研究代表者 |
桜井 貴文 千葉大学, 大学院理学研究院, 教授 (60183373)
|
|---|
| 研究分担者 |
菊池 健太郎 東北大学, 電気通信研究所, 助教 (40396528)
|
|---|
| 研究期間 (年度) |
2017-04-01 – 2024-03-31
|
| キーワード | 古典論理 / ラムダ計算 / α同値 / 証明検証系 / minlog |
|---|
| 研究実績の概要 |
本研究の目的は古典論理に基づくの計算系に関する様々な性質を研究することであるが、本研究代表者は、これまでの研究で古典論理の計算系を型付ラムダ計算に翻訳する新しい変換を考え、その変換が簡約を保存するという性質を持つことを示した。具体的には、古典論理の計算系 lambda-bar-mu やその変種の lambda-bar-mu-tilde-CBN を lambda-conj-neg に翻訳する変換および lambda-conj-neg を型付ラムダ計算に翻訳する簡単な変換を考え、それらの変換を合成することで新しい変換を得ることができた。本研究では、それらの古典論理の計算系から型付ラムダ計算への翻訳に関する性質を計算機上の証明検証系で証明することを最初の目標としており、そのためにminlogという証明検証系を使っている。
本研究代表者は平成29年度に開始した「クラス理論に基づく自己拡張可能なソフトウェア検証体系の深化」(代表者:佐藤雅彦)という科研費の研究課題の分担者になっていたが、その研究課題では、ラムダ計算を改良・発展させた計算系を開発するためにminlogを使ってその計算系の性質を証明している。さらにその研究課題ではminlogを使ってその計算系と伝統的ラムダ計算の関係を明かにした。伝統的ラムダ計算は古典論理の計算系 lambda-bar-mu に含まれるので、その研究で開発している技術は本研究に応用できるという見込みの下にその分担研究課題に取り組んだ。令和3年度までに伝統的なラムダ計算について様々な性質を証明してきて一段落したと思ったが、令和4年度にα簡約が同値関係になるというよく知られた定理に新しい証明があることに気付き、その証明に取り組むことに注力した。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
4: 遅れている
理由
古典論理の計算系について、証明検証系minlogを用いた検証をまず行う予定であったが、令和元年度から2年度にかけては先に伝統的ラムダ計算について集中して検証を行なったが、これは概要で述べた分担者としての研究との関連でさらに研究を深める必要が生じ3年度から4年度にかけてそれに取りかかった。しかし、変数の扱いに関して決定的な方法がまだ見つからず研究が進まなかったので、当初の目的であった古典論理の計算系の簡約の性質の検証の段階にまで至ってない。
実際に進捗した部分としては、伝統的なラムダ計算の性質についての研究を続け、α簡約が同値関係になるというよく知られた定理に新しい証明があることに気付き、その証明に取り組んだ。証明のアイデアは、α簡約時に起き得る変数の衝突を回避するために、そのようなα簡約を変数の衝突が起きないようなα簡約に分解するというものであるが、その過程で、伝統的なラムダ計算における代入操作は再帰的に定義されるが、これまで見逃していた振舞いに気付き、それが証明において重要であることが判明した。その証明は証明検証系minlogを使って形式化しており、大筋は完成した状態になっている。
このように、当初の課題に取り組む準備として行っていた研究に予想よりも興味深い点を見付けたので、そちらのほうに力を注いでしまったので、当初の目標である古典論理の計算系の研究については遅れている。
|
| 今後の研究の推進方策 |
昨年度から引き続いての延長であるが、これまでにできなかった部分を遂行するより、伝統的ラムダ計算に関してもう少し研究を続けたい。具体的には、進捗状況の所で述べたα簡約が同値関係になるという証明を証明検証系minlogを使って細部に至るまで完全に完成する。しかし、minlogによる形式的証明の表現はプログラムのようなものなので、それだけを読んでも理解するのは容易ではない。そこでアイデアと技術的詳細を自然言語で説明し、最終的に論文の形にしたい。
その後(もしくは並行して)、証明検証系minlogを用いて古典論理の計算系から型付ラムダ計算への翻訳に関する性質の検証に引き続き取り組む。まずminlogによる古典論理の計算系の形式化を完成する；型付ラムダ計算の形式化については、伝統的ラムダ計算の形式化はできているので容易である。そして次の段階つまり翻訳の性質の証明を行う。伝統的ラムダ計算のα簡約中に出てくる代入操作は古典論理の計算系においても基本的な操作であり、令和4年度の研究で得られた知見が役に立つと思われる。
また時間があれば、古典論理の計算系を動かす抽象機械について考察したいが、それには明示的代入計算を利用するのが良さそうである。なぜなら、明示的代入計算は代入操作を分解したものなので、明示的代入計算と古典論理の計算系の簡約過程の対応をうまく表現できることが期待できるからである。そして、明示的代入計算および抽象機械をminlogで表現することにより簡約の性質についてもminlog上で証明できるようになるので、抽象機械の実装だけでなく性質を証明するための枠組も整うので都合がよいのである。
|
| 次年度使用額が生じた理由 |
令和2年度から続く病気により、令和4年度も研究に十分な時間が取れず、遅れを取り戻すことができなかったため、次年度使用が生じた。
使用計画としては、令和4年度に購入する予定であった計算機および周辺機器を購入する予定である。
|
