| 研究課題/領域番号 |
18K11156
|
|---|
| 研究機関 | 東北大学 |
|---|
研究代表者 |
浅田 和之 東北大学, 電気通信研究所, 助教 (00570251)
|
|---|
| 研究期間 (年度) |
2018-04-01 – 2021-03-31
|
| キーワード | 非決定計算 / 確率計算 / 量子計算 / 交差型 / 関数型言語 / ラムダ計算 / 高階文法 / 反復補題 |
|---|
| 研究実績の概要 |
当年度では2つの研究成果を発表することができた．
1つは広い意味での非決定性計算を備えたプログラミング言語の表示的意味論を与えた研究である．非決定性を備えたプログラミング言語は伝統的な領域理論では捉えられない計算の側面があることが古くから知られており，これに対して近年研究が活発に行われている．本研究では通常の非決定計算や，離散的な確率計算，そして量子計算を含む非決定性のある計算機構を備えたプログラミング言語のクラスに対して，その表示的意味論を与える一様かつ一般的なフレームワークを提案した．特にこの手法で与える量子計算の表示的意味論は，Paganiらによる最新の量子計算の表示的意味論と一致しており，それらがどのように一般的な技法により構成されるのかを説明している．またこの提案技法は非常に一般性のある（「自由」な）交差型システムに基づいており，交差型が近年プログラム検証に応用されている背景から，非決定性を備えたプログラムの検証技法の開発に有用なのではないかと期待している．
2つ目の研究は木を計算する単純型付ラムダ計算の項に高階のhomeomorphic embeddingの順序を入れた場合に，well-quasi-orderingになるのではないかという予想を3階の項まで示したというものである．この種の予想を示すことで高階木文法の反復補題が導かれるということを本研究の共同研究者と過去に示しており，この予想の3階までの解決により，3階の木文法の反復補題が得られたことになる．高階木文法は近年高階モデル検査に使われプログラム検証に応用されている．なお0階，1階，2階の語文法はそれぞれ正則文法，文脈自由文法，インデックス文法と同等であり，3階の木文法（の葉の語言語）は4階の語文法に対応するものであり，一般に階数が上がるほど反復補題の複雑さも増していく．
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
離散的確率計算や量子計算のプログラミング言語に対して交差型を用いたモデルを与えることが出来た．この交差型による表示的意味論は再帰型システムについても容易に拡張でき，特に，従来研究と違い本研究では構文的ではなく数学的モデルに基づいた表示的意味論を与えているため，型システムの拡張に対応しやすい．
|
| 今後の研究の推進方策 |
ゲーム意味論あるいは交差型などの技術により連続的な確率計算の表示的意味論を与えることを進めていく．また本年度得られた表示的意味論は交差型変換の圏論的意味論になっていることが明らかになった．交差型変換はプログラミング言語の間の翻訳・変換を，プログラムの操作的性質を交差型に基づいて細かく分析しながら与えるものであり，近年多くの重要な成果を生み出している．その圏論的意味論を与えるということは，交差型変換の技術を一般化し他の表示的意味論の技術と組み合わせることができることを意味している．まずはこれをGirardの提唱した「相互作用の幾何」によるモデルと組み合わせることで，有用なプログラム変換が得られないか研究を進めたい．
多相型のパラメトリシティ原理の圏論的意味論を与えることを並行して行っていく．多相型理論に依存型理論の技術を用いたパラメトリシティ原理の論理関係のアプローチでの研究が近年成功しており，その技術を圏論的意味論のほうにも活用できるのではないかと考えている．近年の型理論の研究とも密接に関係しており，関連分野を調査し技術を習得しつつ研究を進めていく．
|
| 次年度使用額が生じた理由 |
海外の旅費などは事前の想定に対する誤差があるため，若干の予算が残った．
次年度以降旅費に使用する予定である．
|
