2017 Fiscal Year Research-status Report
文脈移動変換と高階書き換え理論に基づくプログラム検証法の研究
| Project/Area Number |
16K00091
|
|---|
| Research Institution | Tohoku University |
|---|
Principal Investigator |
菊池 健太郎 東北大学, 電気通信研究所, 助教 (40396528)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
青戸 等人 新潟大学, 自然科学系, 教授 (00293390)
|
|---|
| Project Period (FY) |
2016-04-01 – 2019-03-31
|
| Keywords | 書き換えシステム / プログラム検証 |
|---|
| Outline of Annual Research Achievements |
書き換えシステムに基づく新しいプログラム検証手法を開発することを目的として研究を進めている。本年度の研究では、以下のような成果・知見が得られた。
(1) 左線形項書き換えシステムに対する並列閉包定理とその一般化による合流条件を、左線形名目書き換えシステムに対する合流条件に拡張した。この条件は、α安定性をもたない名目書き換えシステムに対しても有効であるため、従来の束縛変数を伴う高階書き換えの枠組みでは取り扱えない例に対しても適用可能である。一方、名目書き換えシステムのようにα同値性を明示的に扱うことはせず、α同値な項を同一視するような書き換えシステムの枠組みとその記述形式を提案し、分離並列簡約との強可換性を用いた合流条件を与えることを試みた。しかしながら、そのような枠組みにおいては書き換えシステムのクラスの条件を書き下すことが困難であることが分かり、合流条件の厳密な議論のためには名目書き換えシステムの枠組みのほうが優れているという知見が得られた。
(2) プログラムを表す書き換えシステムの変換の一つである文脈移動変換においては、変換の正当性を保証するために文脈交換律などの等式が元の書き換えシステムの帰納的定理であることを証明する必要がある。研究代表者らの先行研究では、停止性や十分完全性をもたない書き換えシステムの変換の例について正当性を示しているが、その考え方を一般的な等式の帰納的定理の証明においても適用できないか検討した。帰納的定理の証明手法である潜在帰納法では、合流性と十分完全性が条件として必要であると考えられているが、本研究の検討の結果、十分完全性については全ての項に対してではなく証明すべき等式の両辺の項に対してのみ要求すればよいということが明らかになった。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
束縛変数を伴う書き換えシステムに対しては、名目書き換えシステムと関連する体系の合流条件についての成果・知見が、また、文脈移動変換に対しては、新しい帰納的定理の証明手法についての知見がそれぞれ得られ、おおむね計画通りに研究を進めることができたため。
|
| Strategy for Future Research Activity |
これまでに得られた成果・知見を利用して、書き換えシステムに基づく新しいプログラム検証手法を開発する。また、開発した検証手法を実際のプログラムの例に適用することにより、その有効性を明らかにする。
|
