TOP > 研究活動 > 研究者総覧「情報知」 > 情報システム学専攻 > ソフトウェア論講座 > 西田 直樹

研究者総覧「情報知」

情報システム学専攻

氏　名
西田 直樹（にしだ なおき）
講座等
ソフトウェア論講座
職　名
准教授
学　位
博士(工学)
研究分野
項書換え系，プログラム変換，定理自動証明
西田 直樹

研究内容

関数型言語における逆計算プログラムの自動生成とソフトウェア検証
研究の背景--逆計算とは
あるプログラムの逆計算とは、既知の出力データから元の入力データを求めることである。そのような計算を行うプログラムを生成するツールは逆計算コンパイラと呼ばれ、生成されたプログラムは元のプログラムの逆計算プログラムと呼ばれる。また、元のプログラムの計算は順計算と呼ばれる。順/逆計算プログラムの実用例としては、圧縮/解凍ソフトウェアが挙げられる。実用例からもわかるように、逆計算プログラムにバグが存在することは大きな問題である。よって、逆計算プログラムには高い信頼性が要求される。そのために、与えられたプログラムから自動的にその逆計算プログラムを生成する逆計算コンパイラにはバグのないプログラム生成を求められ、それが満たされているとき非常に有益なツールとなる。

研究の概要--逆計算コンパイラの構築
本研究では、関数型言語の代表的な計算モデルである項書換え系を対象とした逆計算コンパイラの構築を行っている。

本研究のコンパイラの最大の特長は、生成するプログラムにバグがないことである。これは、変換方法の正しさを証明することによって実現している。関数型言語の分野では、すでに様々な逆計算コンパイラが提案されてきた。しかし、それらのすべてにおいて生成方法の正当性は議論されていない。たとえ、変換が直感的に正しいように見えても、本当に正しいかは保証できない。それは順計算の評価方法に関係している。Call-by-Valueで評価していない順計算については逆計算が可能かどうかは現在のところわかっていない。この問題点は、本コンパイラの正しさを証明する過程で明らかにされたことであり、本研究の成果といえる。また、項書換え系は計算の規則を“左辺項→右辺項”の形式で表現する単純な計算モデルであるので、他の関数型言語との対応関係がわかりやすい。よって、本コンパイラの正当性から他手法の正当性の保証に利用できると期待される。

多対一関数の逆計算では解が複数個存在する場合がある。項書換え系は非決定的な計算も自然に表現できるので、すべての解への書換えが存在する。この場合、全解探索によりすべての解を得られるが、単純に全解探索を行っては効率が悪い。そこで、本研究では非決定的な計算における全解探索の効率化を実現する計算戦略も研究している。成果の一つは、生成したプログラムが計算の停止性と２つのある構文的性質を持つ場合に再内計算（Call-by-Valueに相当する戦略）によりすべての解が得られることである。また、本研究では、生成プログラムに要求される構文的性質をもたらす元のプログラムの構文的性質についても調べている。これは、項書換え系のこれまでの多くの成果を利用することに役立つ。

研究の拡張--部分逆計算へ
逆計算の拡張として、部分逆計算がある。これは元のプログラムの引数の値の一部は既知と考え、それらの値と既知の出力値から、残りの引数の値を求めることである。例えば、加算と減算、乗算と除算などが身近な例である。また、セキュリティプロトコルの分野における暗号化/復号化ツールもよい例である。暗号化/復号化には共通鍵などが既知の値として使われる。逆計算は部分逆計算の特別な場合であるので、部分逆計算はより複雑なテーマである。一方で、より実用性が強いので、非常におもしろいテーマでもある。

今後の展望--ソフトウェア検証への応用
逆計算を利用する例として、ソフトウェア検証が挙げられる。これは、本研究の応用分野の一つであり、今後の研究テーマでもある。元のプログラムの引数すべてが既知である状況では、部分逆計算は何を意味するのだろうか？ これは順計算と逆計算を同時に行うことによる計算の整合性の検証になっていると考えられる。このように逆計算が順計算をさかのぼる計算であることを利用した検証もおもしろいテーマである。

前述したように、これまでの逆計算コンパイラの研究では、変換の正当性などは議論されていなかった。しかし、本コンパイラの正当性の証明の際には、逆計算ができる順計算の条件などが明らかになり、さらに順計算の性質の解析や、それに関係した元のプログラムの性質の有用性も示された。ソフトウェア検証が部分逆計算の応用例の一つであることからも、逆計算におけるさまざまな性質の解析は非常に有益な結果をもたらす可能性がある。逆計算に関する研究はまだまだおもしろくなっていきそうである。
順計算／逆計算の概要

順計算／逆計算の概要

経歴

  • 2004年３月 名古屋大学大学院工学研究科情報工学専攻博士後期課程修了．博士（工学）．
  • 2004年４月 同大学大学院情報科学研究科情報システム学専攻助手．
  • 2007年4月〜2013年3月 同大学同研究科同専攻助教．
  • 2010年7月〜12月バレンシア工科大学客員研究員．
  • 2013年4月 同大同研究科同専攻准教授．現在に至る．

所属学会

  • 電子情報通信学会
  • 日本ソフトウェア科学会
  • 情報処理学会

主要論文・著書

  1. 西田直樹，酒井正彦，坂部俊樹，構成子項書換え系の逆計算プログラムの生成，電子情報通信学会論文誌，J88-D-I(8)，1171-1183，2005．
  2. 西田直樹，酒井正彦，坂部俊樹，右辺のみに現れる変数を持つ項書換え系の計算モデル，コンピュータソフトウェア，20巻，５号，85-89，2003．
  3. 西田直樹，酒井正彦，坂部俊樹，PT関数の逆関数を定義するTRSの生成，コンピュータソフトウェア，19巻，１号，29-33，2002．
  4. Nishida, N., Sakai, M., and Sakabe,T., “Partial Inversion of Constructor Term Rewriting Systems", Proceedings of RTA 2005, LNCS 3467, pp. 264-278. 2005.
  5. 古市祐樹, 西田直樹, 酒井正彦, 草刈圭一朗, 坂部俊樹， 制約付き項書換え系の潜在帰納法を利用した手続き型プログラム検証の試み， 情報処理学会論文誌プログラミング，Vol. 1，No. 2，pp. 100-121, 2008．
  6. 坂田翼, 西田直樹, 坂部俊樹, 酒井正彦, 草刈圭一朗， 制約付き項書換え系における書換え帰納法， 情報処理学会論文誌プログラミング，Vol. 2，No. 2，pp. 80-96，2009．
  7. Nishida, N. and Vidal, G., “Termination of Narrowing via Termination of Rewriting “, Applicable Algebra in Engineering, Communication and Computing, Vol. 21, No. 3, pp. 177-225, 2010.
  8. Nishida, N., Sakai, M., and Sakabe, T., "Soundness of Unravelings for Deterministic Conditional Term Rewriting Systems via Ultra-Properties Related to Linearity", In Proc. of RTA 2011, Vol. 10 of LIPIcs, pp. 267-282, 2011.
  9. Nishida, N. and Vidal, G., "Program Inversion for Tail Recursive Functions", In Proc. of RTA 2011, Vol. 10 of LIPIcs, pp. 283-298, 2011.
  10. Sakata, T., Nishida, N., and Sakabe, T., "On Proving Termination of Constrained Term Rewriting Systems by Eliminating Edges from Dependency Graphs", In Proc. of WFLP 2011, Vol. 6816 of LNCS, pp. 138-155, 2011.
  11. Nishida , N. and Vidal, G., "More Specific Term Rewriting Systems", In Proc. of WFLP 2012, 15 pages, 2012.
  12. Nishida, N., Nomura, F., Kurahashi, K., and Sakai, M.. "Constrained Tree Automata and their Closure Properties", In Proc. of TTATT 2012, pp. 24-34, 2012.
  13. Nishida, N. and Vidal, G., "Computing More Specific Versions of Conditional Rewriting Systems", In Proc. of LOPSTR 2012, pp. 115-129, 2012.
  14. Niwa, M., Nishida, N., and Sakai, M., "Extending Matching Operation in Grammar Program for Program Inversion", In Proc of LOPSTR 2012, pp. 130-139, 2012.
  15. Nishida, N., Sakai, M., and Sakabe, T., "Soundness of Unravelings for Conditional Term Rewriting Systems via Ultra-Properties Related to Linearity", LMCS, Vol. 8, No. 3, pp. 1-49, 2012.
  16. Nishida, N. and Vidal, G., "Conversion to tail recursion in term rewriting," The Journal of Logic and Algebraic Programming, Vol. 83, Issu 1, pp. 53-63, Jan 2014.

BACK

このページのトップへ