2019 Fiscal Year Research-status Report
| Project/Area Number |
15K00015
|
|---|
| Research Institution | Kyoto University |
|---|
Principal Investigator |
立木 秀樹 京都大学, 人間・環境学研究科, 教授 (10211377)
|
|---|
| Project Period (FY) |
2015-04-01 – 2021-03-31
|
| Keywords | Fixed Point Logic / Adequacy / Program Extraction / Gray code / Lattice Puzzle |
|---|
| Outline of Annual Research Achievements |
共同研究者とともに，直観主義一階述語論理に述語の再帰的定義を加えた体系 IFP (Intuitionistic Fixed Point Logic) における，証明からプログラムの抽出と，それの応用としての，グレイコードに関するプログラムの抽出についての研究を行った。プログラム抽出における，抽出されたプログラムの正しさを与える定理は，健全性定理と呼ばれている。今まで，IFP の健全性定理は，述語の再帰的定義の利用のされ方に制限を加えた形でしか証明ができていなかった。それに対して，本年度行った研究により完全な証明が得られた。また，抽出の対象となる言語は型なしラムダ計算であるが，そこに，型づけシステムを導入し，さらに，Haskell 言語のプログラムを抽出できるようにした。プログラムの計算結果の正しさは，Adequacy 定理により与えられるが，その証明を，より洗練化することができた。これらの結果を含めた形で，IFP に関する論文を仕上げて，投稿を行うと同時に，Arxiv にあげた。(Ulrich Berger and Hideki Tsuiki, Intuitionistic Fixed Point Logic. arXiv:2002.00188.)また，それと同時に IFP の実装もすすめ，Prawf というシステムを作成した。Prawf を用いて，実数が符号付き2進表現を持っていればグレイコード表現を持つことの証明を行い，それから抽出することにより，この2つの表現の間の変換を行うプログラムを得ることができた。
その一方で，格子状に棒を組み合わせていくパズルである，格子パズルの計算複雑性について調べた。設定を変えることにより，この問題が多項式時間，グラフ同型性完全，NP 完全の3つの異なる計算量クラスの問題になることを示した。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
IFP (Intuitionistic Fixed Point Logic) の論文を完成させることができ，また，その実装である Prawnf システムを完成させ，論文にまとめることができた。
|
| Strategy for Future Research Activity |
共同研究者 とともに，CFP (Concurrent Fixed Point Logic) に関する研究を進め論文をまとめる。IFP, CFP の応用について考える。
|
| Causes of Carryover |
共同研究者と日程の調整が合わなかったり，年度末に参加予定の国際会議がキャンセルになったりした。次年度にこの予算で参加・発表を予定していた会議 (CIE) が virtual 開催になるなど，新型コロナ感染症の影響は次年度も出ている。その状況がいつまで続くかにもよるが，国際共同研究を進展させるため，および，研究発表のための旅費として使用することを計画している。
|
