| 研究課題/領域番号 |
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 の表現とも共通部分は多い。このように、その研究で開発している技術は本研究に応用できるという見込みの下に取り組み一定の知見は得たが、予想していなかった困難にぶつかり本研究への応用にまでは手が回らなかった。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
4: 遅れている
理由
証明検証系minlogを用いた検証をまず行う予定であったが、その基となるであろうと見込んでいた部分の一部(具体的にはeta変換と呼ばれる変換の扱い方)で思いのほか手間取り、簡約の性質の検証の段階にまで至ってない。しかし、研究実績の概要の所で述べた別課題の分担者としての研究の経験から、どのように進めればよいかは判明している。
また、当初の研究計画では明示的代入計算に関する研究はもう少し後で取り組む予定であったが、分担者として行っている研究との関わりが出てきたので、計画を前倒しして、明示的代入計算をminlogを使って表現してその性質を証明することにも取りかかった。まだ完成には至っていない状態であるが、方針を立てることはできた。
|
| 今後の研究の推進方策 |
まず、証明検証系minlogを用いて古典論理の計算系から型付ラムダ計算への翻訳に関する性質の検証に引き続き取り組む。minlogによるラムダ計算の表現は一応できているので、その部分は固定してもしくは変更があっても大丈夫な形にして、次の段階つまり翻訳の性質の証明を行う。
次に、当初の研究計画での順序を変更して、明示的代入計算に関する研究を先行させる。明示的代入計算をminlogを使って表現しておくと簡約過程を計算機上で実行することができるので、確認しながら設計や証明を進めやすくなることがこれまでの経験で判明した。そしてその性質を証明することにも取りかかり、簡約過程を抽象機械上実行とみなすことを考える。抽象機械もminlogで表現することにより、この対応をうまく表現できることが期待できる。
|
| 次年度使用額が生じた理由 |
29年度の秋に計3週間の入院をし、その後に体調不良が続いたため、十分に研究時間が取れず、次年度使用が生じた。
使用計画としては、29年度に購入する予定であった計算機を購入するつもりである。
|
