定式化された形式木言語理論に基づくソフトウェア基盤技術の開発
| Project/Area Number |
17K00007
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Multi-year Fund |
|---|
| Section | 一般 |
|---|
| Research Field |
Theory of informatics
|
|---|
| Research Institution | Tohoku University (2018-2020)
The University of Electro-Communications (2017) |
|---|
Principal Investigator |
中野 圭介 東北大学, 電気通信研究所, 教授 (30505839)
|
|---|
| Project Period (FY) |
2017-04-01 – 2022-03-31
|
| Project Status |
Granted (Fiscal Year 2020)
|
| Budget Amount *help |
¥4,420,000 (Direct Cost: ¥3,400,000、Indirect Cost: ¥1,020,000)
Fiscal Year 2020: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000)
Fiscal Year 2019: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000)
Fiscal Year 2018: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000)
Fiscal Year 2017: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000)
|
|---|
| Keywords | 形式木言語理論 / 定理証明支援系 / 木トランスデューサ / 木オートマトン / 双方向変換 / プログラム検証 / 等価性判定 / 型検査 / 結合子論理 / プログラム変換 / ソフトウェア検証 |
|---|
| Outline of Annual Research Achievements |
本研究の目的は定式化された形式木言語理論をソフトウェア基盤技術へ応用することであった． 最終年度にあたる令和二年度では，形式木言語理論における木構造データ変換のモデルであるストリーム型の木トランスデューサに着目して研究を進めた．主な成果は，研究代表者がこれまでに研究を進めてきた木トランスデューサの効率的な実装の延長となるものであり，(1)ストリーム型木トランスデューサの表現力の特定と(2)等価性判定が決定可能な木トランスデューサに関する結果である．
(1)のストリーム型木トランスデューサの表現力については，比較的自然な制約の下で既知の木トランスデューサのクラスと一致することを証明した．ストリーム型トランスデューサについては，研究代表者が平成16年に木トランスデューサ理論を構造化文書処理の効率化に応用して以来形式的な表現力が未解決であったが，今回の研究成果によりこの問題に対する部分的な解決が得られたと言える．
(2)の等価性判定が決定可能な木トランスデューサに関する結果についても，ストリーム型木トランスデューサのクラスに対して研究を行った．木トランスデューサの等価性判定に関する従来の結果の多くはストリーム型の変換クラスを対象にしておらず，同様の先行研究においては入力に対して線形な変換のみを扱っていた．今回の研究成果ではより高い表現力をもつストリーム型木トランスデューサのクラスについて透過性判定が決定可能になることを示している．この結果は(1)で示したクラスの表現力同値性を利用したものである．
この他の成果として，研究代表者のテーマの一つであった木構造データに対する双方向変換についての研究も並行して進めた．双方向変換は，二つのデータ間を同期するために必要な二つの変換のことであるが，それらの一貫性が決定可能となる変換のクラスを特徴づける計算モデルを提案した．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
本研究の最終的な目標は，形式木言語理論をソフトウェア基盤技術へ応用することであり，その応用は主に (i)プログラム検証 と (ii)プログラム効率化 の二つであった．本研究課題の実施期間において，(i)については，木トランスデューサで表現することのできる木構造変換プログラムに関する二つの性質について静的検査アルゴリズムを考案した．一つは特定の木トランスデューサのクラスに対する等価性判定アルゴリズムで，二つのプログラムがあらゆる入力に対して出力が同じになることの検査が可能となる．二つめはスタック付きの木トランスデューサに関する停止性判定アルゴリズムで，構文解析などスタックを扱う一部の再帰プログラムについて入力に関係なく停止するかの検査が可能となる．(ii)については，複数の再帰関数の合成について中間データ構造の生成を回避する関数融合に関する新たな成果を得た．木トランスデューサを用いた従来の関数融合アルゴリズムでは，変換対象となる木構造データにおける記号が有限種類に限られていたが，注意深く拡張することにより，無限種類の記号を扱うことのできる木トランスデューサ同士の融合が可能となった．この他にも，木オートマトン理論を応用による組合せ子論理についての未解決問題の部分的解決や，木構造データ間の双方向変換の性質に関する発見など，研究計画の時点では予想できなかった研究成果も得られた．以上のことから，進捗状況として，順調に進めることができたと言える．
|
| Strategy for Future Research Activity |
当初の研究計画においては，研究代表者が定理証明支援系を用いて形式化を進めてきた木オートマトンや木トランスデューサなどの形式木言語理論の枠組みに対して，定理証明支援系に頼った応用を中心に進める予定であった．しかしながら，形式木言語理論に基づく意外な応用の発見もあり，本研究課題の実施期間の途中において研究の方向性の調整を行った．特に，双方向変換技術への応用については，実用的なアプリケーションの開発にも関連する重要な課題である．双方向変換技術は，データベースの分野でビュー更新問題として1980年代から研究が進められてきたが，21世紀に入ってから言語的アプローチによって新たな見方が導入され，近年では盛んに研究されている分野となっている．研究代表者は，形式木言語理論の立場から木構造データ変換に対する双方向変換について研究してきた経験を生かし，双方向変換技術を再訪した結果，これまで知られていなかった双方向変換の一貫性の判定方法についても新たな知見を得た．この点についても，引き続きその可能性について精査を行い，形式木言語理論や関連する枠組みの新たな応用として研究を進める予定である．一方で，形式木言語理論における定理証明支援系の形式化において改善の余地がある部分も発見されたため，こちらも引き続き研究を進める必要がある．なお，最終年度において国内外への移動について強い規制があったため，一部の研究成果の発表を翌年度に延期することとなった．
|
Report
(4 results)
Research Products
(23 results)
