2020 Fiscal Year Research-status Report
| Project/Area Number |
15K00015
|
|---|
| Research Institution | Kyoto University |
|---|
Principal Investigator |
立木 秀樹 京都大学, 人間・環境学研究科, 教授 (10211377)
|
|---|
| Project Period (FY) |
2015-04-01 – 2022-03-31
|
| Keywords | Amb / Program Extraction / IFP / nondeterminism / totality |
|---|
| Outline of Annual Research Achievements |
共同研究者とともに，IFP (Intuitionistic Fixed Point Logic) のシステムに細かな修正を行い，論文を最終的なものにした。また，IFP を拡張して，非決定的な並列実行を行うプログラムを抽出できる論理である CFP を考えた。部分プログラム（すなわち，引数によっては止まらないプログラム） M, N に対し，M と N の並列実行を行い最初に返ってきた値を返すプログラムを Amb(M, N) とする。CFP は，IFP に || (restriction) と S (concurrency) という2つの論理演算子を加えた体系である。CFP において，論理式S(A)を証明すると，その証明から，Amb(M, N) という形のプログラムで，どの引数に対しても必ず終了し，A を満たす結果を出すものが得られる。CFP で抽出されるプログラムの正しさは，RCFP というプログラムに関する論理における証明として与えられる。また，表示的意味論と操作的意味論をくみあわせることにより，その証明が実行結果を保証するものであることが示されている。CFP を用いて，実数 x がグレイコードという不定元を含む実数の表現を持つという述語 G(x), 符号付き2進表現を並列的に計算できるという述語 C(x) に対し，all x G(x) -> C(x) を CFP で証明し，その証明から，二つのコード間の変換を行うプログラムを抽出した。 並列実行の全域性を示すのに，concurrency だけではなく restriction の論理演算子も必要であるという知見は，並列実行の根源的な理解の一助になるのではないかと考えている。
|
| 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 の論文を完成させることができた。また，CFP に関する研究も，順調に進んでいる。
|
| Strategy for Future Research Activity |
今後の研究として，CFP に関する研究を完成させる，IFP の実装方法を工夫する，IFP の計算可能性解析学への応用といったことを考えている。
|
| Causes of Carryover |
海外の研究集会での発表を予定していたが，Zoom での開催となり，旅費を使用せずに参加することができた。今年度も，海外での発表や内外の研究者との共同研究を予定している。また，システムを実装するために，コンピュータを購入したい。
|
