| 研究課題/領域番号 |
18K11156
|
|---|
| 研究機関 | 東北大学 |
|---|
研究代表者 |
浅田 和之 東北大学, 電気通信研究所, 助教 (00570251)
|
|---|
| 研究期間 (年度) |
2018-04-01 – 2021-03-31
|
| キーワード | 非決定計算 / 交差型 / 関数型言語 / ラムダ計算 / 高階文法 / 高階プログラム検証 |
|---|
| 研究実績の概要 |
2019年度では高階プログラム検証に用いられる高階木文法（非決定性のあるラムダ計算）に関して2本の論文を投稿した（採録は2020年度）．
2018年度の論文において，Kruskalの木定理の高階木文法への拡張の部分的結果を与えるために，変数の使用分析を基底型の変数にのみ着目して行う（交差型を用いない）手法を導入していたが，これは3階の型の項までに制限されていた．2019年度に投稿した当論文ではこの技術を一般の階の項に拡張することで，2016年に与えた「n+1階の高階語文法の成す語言語とn階の高階木文法の生成する木の葉からなる語言語は等しい言語クラスを成す」という（交差型を用いた）結果を計算量の面で改良した．これにより，変換における文法の理論的サイズの増大および計算時間がそれまで超指数的だった計算量を，多項式計算量へと改善させた．これにより，一般に，高階木言語の計算量を伴う結果から高階語言語の結果を系として導出することが容易にできるようになった．
別の論文では高階モデル検査の定量的計算量を分析する研究を行った．この研究では交差型を用いて使用分析の精緻な技術を構築し，それを活用して，2018年度に発表した無限の猿の定理の技術を併用して高階モデル検査の定量的計算量の結果を与えた．高階モデル検査は最悪計算量についてはよく研究されているが，より現実的な計算量である平均計算量の研究はまだなされておらず，本研究はその第一歩を踏み出したものである．またこの使用分析の技術はラムダ計算や高階文法の他の問題へも応用が期待できる．
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
今年度行った研究は昨年までの研究成果で用いられた技術の延長上にあるものであるが，計算量や平均計算量というより応用に近い結果を出すことができ，研究技術の有用性を示している．
|
| 今後の研究の推進方策 |
2019・2020年度の論文において，基底型の変数にのみ着目した使用分析を行う（交差型を用いない）手法を導入することでより良い計算量の結果を出すことに成功したが，これを既存の交差型の枠組みとどう結び付けられるのかについて明らかにしたい．これにより，一定のケースの既存の交差型を用いた研究についても同様に計算量の改善が見込めるのではないかと期待できるため，研究を進めていきたい．
2019年度の研究において，既存の値呼び評価の意味論との関係が不明であったが，
その後の研究で別の視点から交差型と値呼び評価の研究が行われており，
それを手がかりに我々の研究の意味論の値呼び評価の側面を研究したい．
|
| 次年度使用額が生じた理由 |
コロナウイルスの感染拡大のため参加を予定していた学会が現地開催を中止したため．
|
