Top > Search Research paper > (In Japanese)効率的で正しいプログラムの自動生成

(In Japanese)効率的で正しいプログラムの自動生成

Research report code R040000101
Posted date May 18, 2007
  • (In Japanese)小川 瑞史
  • (In Japanese)北陸先端科学技術大学院大学情報科学研究科
Research organization
  • (In Japanese)北陸先端科学技術大学院大学
Report name (In Japanese)効率的で正しいプログラムの自動生成
Technology summary (In Japanese)効率的で正しいプログラムを得るために、計算機が可能なサポートには(1)人間の書いたコードの解析に基づく最適化とエラー検出、および(2)仕様に基づく自動生成の二つがある。後者ではプログラムの正しさは仕様と自動生成系が正しければ自動的に保証される。本研究では、後者の立場をとり、「効率的で正しいプログラムの自動生成」というテーマを設定した。しかし、一般的なプログラムを対象に自動生成を試みれば、構成的証明からのプログラム抽出の研究でも広く知られるように簡単に決定不能性に陥る。したがって、有用な応用領域への適切な制限が必要になる。また、理論計算機科学では論理の枠組みを用いることが多いが、その中にもるべき内容を数学(特に組み合わせ理論)から借りてくることで、対象とする領域では人間のコーディングを凌駕する自動生成を狙いとした。具体的なアプローチは、応用領域の制限として、(1)関係データベースやデータマイニング、(2)プログラムのフロー解析を、また組み合わせ理論としてそれぞれ(1)順序の理論(Well-Quasi-OrderやKruskal型定理の構成的証明)(2)グラフの代数的構成法(グラフの木分割や木幅)を用いた(図)。これらの組み合わせ理論は、線形時間プログラムの生成、および生成されたプログラムの定数の削減において用いられる。
Research field
  • Theory of computation
  • Computer software in general
Published papers related (In Japanese)(1) Ken Mano, Mizuhito Ogawa, Unique Normal Form Property of Compatible Term Rewriting Systems-A New Proof of Chew's Theorem-, Theoretical Computer Science, 258(1-2), pp.169-208, 2001.
(2) Zurab Khasidashvili, Mizuhito Ogawa, Vincent van Oostrom. Perpetuality and Uniform Normalization in Orthogonal Rewrite Systems. Information and Computation, 164(1), pp.118-151, 2001.
(3) Mizuhito Ogawa. A Linear Time Algorithm for Monadic Querying of Indefinite Data over Linearly Ordered Domains. Information and Computation, 186(2), pp.236-259, 2003, Fourth International Symposium on Theoretical Aspects of Computer Science special issue.
(4) Mizuhito Ogawa. Well-Quasi-Orders and Regular ω-languages. Theoretical Computer Science 掲載予定, Third International Colloquium on Words, Languages and Combinatorics special issue.
(5) 篠埜功,胡振江,武市正人,小川瑞史.ナップサック問題およびその発展問題の統一的解法,コンピュータソフトウェア18(2), pp.59-63, 2001.
(6) 篠埜功,胡振江,武市正人,小川瑞史.最大重み和問題の線形時間アルゴリズムの導出.コンピュータソフトウェア18(5), pp.1-17, 2001.
(7) Isao Sasano, Zhenjiang Hu, Masato Takeichi, Mizuhito Ogawa. Derivation of Linear Algorithm for Mining Optimized Gain Association Rules. コンピュータソフトウェア 19(4), pp.39-44, 2002.
(8) 山岡裕司,胡振江,武市正人,小川瑞史.モデル検査技術を利用,したプログラム解析器の生成ツール.情報処理学会論文誌:プログラミング掲載予定.
(9) Zurab Khasidashvili, Mizuhito Ogawa, Vincent van Oostrom. Uniform Normalization beyond Orthogonality. Proceedings of the 12th International Conference on Rewriting Techniques and Applications (RTA01), Lecture Notes in Computer Science 2051, pp.122-136, May 2001, Springer-Verlag.
(10) Mizuhito Ogawa. Generation of a Linear Time Query Processing Algorithm Based on Well-Quasi-Orders. Proceedings of the Fourth International Symposium on Theoretical Aspects of Computer Software (TACS2001), Lecture Notes in Computer Science 2215, pp.283-297, October 2001, Springer-Verlag.
(11) Mizuhito Ogawa. Call-by-Need Reductions for Membership Conditional Term Rewriting Systems. The 3rd International Workshop on Rewriting Strategies in Rewriting and Programming (WRS03), June 2003, Electronic Notes in Theoretical Computer Science 86(4) 掲載予定, Elsevier.
(12) Mizuhito Ogawa, Zhenjiang Hu, Isao Sasano. Iterative-Free Program Analysis, Proceedings of the 8th ACM SIGPLAN International Conference on Functional Programming (ICFP03), pp.111-123. August 2003, ACM Press.
Research project
  • Precursory Research for Embryonic Science and Technology.;Information and Systems
Information research report
  • (In Japanese)小川 瑞史. 効率的で正しいプログラムの自動生成. 「さきがけタイプ」「機能と構成」領域 研究報告会講演要旨集(研究期間2000-2003),2003. p.9 - 17.