| 研究課題/領域番号 |
17K00007
|
|---|
| 研究機関 | 電気通信大学 |
|---|
研究代表者 |
中野 圭介 電気通信大学, 大学院情報理工学研究科, 准教授 (30505839)
|
|---|
| 研究期間 (年度) |
2017-04-01 – 2021-03-31
|
| キーワード | 形式木言語理論 / 定理証明支援系 / プログラム変換 / プログラム検証 |
|---|
| 研究実績の概要 |
前年度までの研究代表者の研究成果である木言語理論および木トランスデューサ理論の定式化を整理し，実際の応用に必要な拡張について検討を行うのが本年度の目標であった．ここで具体的に想定されていた応用とは，形式木言語理論を利用した (1)ソフトウェア開発の手法 (プログラム合成やプログラム変換) および (2)プログラム検証の手法 (モデル検査や等価性判定) のことである．本年度は，(1)として属性付き木トランスデューサの表現力の再考，(2)としてはプログラム検証である (2a) 木トランスデューサの型検査や (2b) 等価性判定の実装の準備を進めた．
(1)については研究代表者が平成21年に発表したスタック属性付き木トランスデューサを再考してプログラム変換への応用を発表したが，循環性の考慮が必要なその意味論の複雑さから定理証明支援系において定式化することは難しく，今後の課題であると言える．
(2a) 木トランスデューサの型検査は，与えられた木変換規則と入出力の仕様に対し，「仕様を満たす入力を変換すると必ず仕様を満たす出力が得られる」ということを静的に検査することであり，逆像に基づく計算手法が一般的である．本研究では木オートマトンの表現を工夫することで効率的な実装ができることを確認した．
(2b) 木トランスデューサの等価性判定は，与えられた2つの木変換が同じ入力に対して同じ出力を返すことを静的に判定することであり，降下型木トランスデューサについては様々なアルゴリズムが提案されているものの実装されているものはほとんどない．一部のアルゴリズムについて実装を進めている．
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
初年度である本年度は主として木言語理論および木トランスデューサ理論の定式化を応用するための調査が主な目的であった．一般に，定理証明支援系によって定式化された枠組みから得られる実装は非効率であることが知られているため，Coqなどで提供されているプログラム抽出の機能 (定式化された関数を実行可能なプログラムに変換する機能) をそのまま利用することは現実的ではない．そこで，定理証明支援系とは独立に効率的な実装ができることを確認した上で，それを定式化するという方針で進めている．本年度は，木言語理論において実用化が期待できる枠組みやアルゴリズムのうち，(1)スタック属性付き木トランスデューサの合成によるプログラム変換，(2a)マクロ森トランスデューサの型検査および(2b)降下型木トランスデューサの等価性判定によるプログラム検証を対象にした．
(1)については，スタック属性付き木トランスデューサの合成は，定式化されやすい関数型プログラミングによって実装を行なっているものの，停止性については非自明であり，定理証明支援系における定式化は簡単ではない．そこで，マクロ木トランスデューサと呼ばれる，高い表現力を持ちながら停止性が自明である枠組みを拡張し，スタックマクロ木トランスデューサの考案に至った．
(2a)については，マクロ木トランスデューサを拡張したマクロ森トランスデューサの型検査は逆像を木オートマトンで表現する方法が直観的であり定式化しやすいが，効率のために工夫された実装では交代性木オートマトンが必要であることがわかった．
(2b)については，降下型木トランスデューサの等価性判定の手法として，木トランスデューサの値域を多項式環イデアルに対応できる事実を利用しているため，今後この定式化が必要であることがわかった．ただし，効率的に実装は多項式環に関する特殊な事実を利用する必要がある．
|
| 今後の研究の推進方策 |
当初の計画において，2年めにあたる平成30年度にプログラム変換に必要な木トランスデューサの拡張を検討することを予定していたが，初年度の調査結果を踏まえ，属性付きキトランスデューサに対して(1)文字の抽象化と(2)スタック機構の導入の2点を試みる．(1)の文字の抽象化とは，通常のトランスデューサでは扱えなかった無限の文字集合を扱うための拡張で，記号的トランスデューサとしてマイクロソフトの研究グループを中心に盛んに研究されているものである．このアイデアを属性付きトランスデューサに適用することにより，プログラム変換への応用できる範囲が広がるものと期待される．(2)のスタック機構の導入については研究代表者の過去の研究において提案されていたが，合成アルゴリズムの提案のみにとどまり，その表現力は明らかにされてこなかった．そこで，昨年度検討したスタックマクロ木トランスデューサとの比較や，逆像の性質や型検査の決定可能性などの議論をもとに表現力を特定する．
また，初年度においてはプログラム検証に関する調査も進んでいるため，こちらについても定式化の応用に向けた実用性の高い実装に引き続き取り組む．具体的には，逆像の表現するデータ構造を工夫するのとによる型検査の効率化や，多項式環イデアルを利用した木トランスデューサの等価性判定について現実的な実装やそれに対する定式化を検討する．特に等価性判定のアルゴリズムについては，他の木トランスデューサのクラスに拡張しやすいように多項式環を経由しない定式化の検討も行う．
この他，結合子論理の計算の仕組みの解明のために木言語理論の核となる木オートマトンを利用できることが確認されており，こちらの応用についても併行して研究を進める．
|
| 次年度使用額が生じた理由 |
来年度から実施される実用的アルゴリズムの実装に必要な計算機購入に充てるため．
|
