2018 Fiscal Year Research-status Report
定式化された形式木言語理論に基づくソフトウェア基盤技術の開発
| Project/Area Number |
17K00007
|
|---|
| Research Institution | Tohoku University |
|---|
Principal Investigator |
中野 圭介 東北大学, 電気通信研究所, 教授 (30505839)
|
|---|
| Project Period (FY) |
2017-04-01 – 2021-03-31
|
| Keywords | 形式木言語理論 / 木オートマトン / 木トランスデューサ / 結合子論理 |
|---|
| Outline of Annual Research Achievements |
本研究の目的は定式化された形式木言語理論をソフトウェア基盤技術へ応用することであるが，2年目にあたる平成30年度では，形式木言語理論の中心となる木トランスデューサ（木変換の形式的表現）と木オートマトン（木集合の形式的表現）の双方について応用やそのための拡張について研究を進めた．本年度の成果は，主に(1)木トランスデューサの記号的拡張，(2)木トランスデューサの等価性判定，(3)結合子論理の性質の部分的解明である．
(1)の記号的拡張は既存の木オートマトンや木トランスデューサを拡張する手法の一つであり，記号の有限性制約を外すことを目的としている．この拡張は，有限性を満たす場合の望ましい性質を維持しながら注意深く行う必要があるが，本研究では，マクロ木トランスデューサとよばれる比較的表現力の高いものについて拡張に成功した．
(2)の等価性判定はプログラム検証の手法に応用可能な「同じ入力に対し必ず同じ出力が得られる」という問題を解くことであり，一般的には決定不能問題であるが，特定の木トランスデューサについては決定可能であることが知られている．本研究では，ストリーム木トランスデューサの特殊な場合について等価性が決定可能になると予想し，部分的に解決した．
(3)の結合子論理の中で関数合成を表す結合子について，研究代表者が平成20年に予想した性質を部分的に証明した．この証明においては，無限個の要素を含む木集合を有限で表せる木オートマトンを利用している．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
当初の計画において本年度は，昨年度までに検討した形式木言語理論のソフトウェアへの応用に対し，それに即した拡張を行う予定であった．ここでは，本年度までの進捗状況について，研究代表者が計画において掲げている形式木言語理論の二つの応用，(1)プログラム検証，および，(2)プログラム効率化について述べる．
(1)のソフトウェア検証に利用可能な等価性判定アルゴリズムについては，共同研究者との研究において，等価性判定が決定可能であることが知られている既存の木トランスデューサに帰着することで，異なるクラスの木トランスデューサの等価性判定を実現できることを発見した．この木トランスデューサのクラスはストリーム木変換とよばれる時間効率性と空間効率性の双方を兼ね備えたプログラムをモデル化したものであり，実用的なソフトウェアへの応用する重要な第一歩といえる．
(2)のプログラム効率化に利用可能な木トランスデューサの合成については，記号の有限性にとらわれない記号的アプローチに着目し，既存のさまざまな木トランスデューサのクラスに対して記号的拡張を提案し，それに対応する合成アルゴリズムを開発した．この手法により，多くの再帰的な木変換プログラムの効率化が可能になることが期待される．
一方，当初の予定ではこの拡張を定理証明支援系によって定式化することも視野に入れていたが，結合子論理の性質など想定していない応用も同時に進めていたため，定式化はあまり進んでいない．これは来年度以降の課題である．
|
| Strategy for Future Research Activity |
当初の計画においては，3年めにあたる令和元年度からプログラム合成やモデル検査に必要な木トランスデューサおよび木オートマトンの拡張も進めていく予定であった．プログラム合成は仕様からプログラムを自動生成する手法で， 形式木言語理論においては，入出力に対応する木オートマトンなどで与えられる仕様から木トランスデューサの規則集合を推測することに相当する．また，モデル検査はソフトウェアが仕様を満たしているかを静的に検査する手法で，形式木言語理論においては，「木トランスデューサと入出力に対応する木オートマトンに対し，入力木が入力仕様を満たす限りその変換による出力木は必ず出力の仕様を満たす」という型検査に相当する．
本年度においては，特に型検査に重点を置き，既存の木トランスデューサより広いクラスの木変換に対して型検査を試みる．具体的には，逆像の正規保存性を満たさないクラスの木変換を定義し，従来の手法では実現できなかった型検査アルゴリズムを提案する．また，前年度までに行ってきた等価性判定アルゴリズムについても精査し，木トランスデューサの融合手法についても研究を進め，可能な限り定理証明支援系による定式化を行う．
|
| Causes of Carryover |
研究成果に関する論文が年度をまたいで査読中であり，発表が次年度に持ち越されるため．
|
