発展的ソフトウェアの理論に関する研究

1997 年度 実績報告書

• 研究課題/領域番号: 09245102
• 研究種目: 重点領域研究
• 研究機関: 東北大学
• 研究代表者: 伊藤 貴康 東北大学, 大学院・情報科学研究科, 教授 (80124551)
• 研究分担者: 萩谷 昌己 東京大学, 大学院・理学研究科, 教授 (30156252) ; 米崎 直樹 東京工業大学, 大学院・情報理工学研究科, 教授 (00126286) ; 坂部 俊樹 名古屋大学, 工学部, 教授 (60111829) ; 井田 哲雄 筑波大学, 電子情報工学系, 教授 (70100047)
• キーワード: 発展的ソフトウェア / 発展的計算モデル / ソフトウェア仕様記述 / 論理・関数型プログラミング / 書換え型メタ計算モデル / リアクティブシステム / 検証 / 適応的発展機構

研究概要

発展的ソフトウェアの理論に関して次のような研究を行い、所期の研究成果を得た。
1.ソフトウェア仕様作成プロセス理論の研究(担当:井田哲雄)発展機能を取り入れた論理型・関数型パラダイム、並列分散環境における進化的プログラミング方法論やマルチパラダイム複合処理系の研究を行い、関数・論理型プログラミングと項書換え系に基づく計算モデルの拡張を与え、拡張されたモデルの求解完全性などの結果を得た。
2.書換え型計算に発展的ソフトウェアの基礎研究(担当:坂部俊樹)書き換え規則や項書換え系をFirst Class Objectとして扱え、また、書換え過程の制御を同期演算により記述できる計算モデルについて合流性の十分条件を与えた。また、通信プロセスに関して、実時間通信プロセスの検証技法に関する成果を得た。
3.実時間環境のための発展的ソフトウェアの理論の研究(担当:米崎直樹)リアクティブシステムの発展的構成を目的として、仕様記述の発展的精密化(時間領域の精密化、段階的検証法、差分的検証法等)の研究を行い、1)弱い離散構造を持つ様相論理の結合法による自動証明法、2)システムの実現可能性の分類と判定アルゴリズム、3)様相オペレータを含む命題線形論理CLLeの新しい意味論ついて成果を得た。
4.検証系の検証と検証情報の発展(担当:萩谷昌己)プログラミング及び問題解決機構の研究に関し、正当性検証を行う検証系自身の検証と、検証情報の発展的支援を行う研究を行い、各種検証系の基礎となるグラフ探索アルゴリズムの形式的検証,Javaバイトコ-検証系のための型体系,証明支援系のユーザ・インタフェースなどについて成果を得た。
5.言語処理系の適応的発展機構とプロセスの視覚化の研究(担当:伊藤貴康)関数型並列プログラムを対象として実行効率のよい処理機構を与え、プログラムの実行コストを考慮した処理系の適応的改良法の研究を行い、そのための視覚的ツールを試作した。

研究成果

• [文献書誌] T.Ida and K.Nakahara: "Leftmost Outside-in Narrowing Calculi" Journal of Functional Programming. Vol.7,No.2. 129--161 (1997)
• [文献書誌] Q.Li, Y.Guo, T.Ida and J.Darlington: "The Minimised Geometric Buchberger Algorithm:An Optimal Algebraic Algorithm for Integer Programming" Proceedings of the 1997 International Symposium on Symbolic and Algebraic Computation. 331--338 (1997)
• [文献書誌] T.Suzuki, K.Nakagawa and T.Ida: "Higher-Order Lazy Narrowing Calculus:A Computation Model for a Higher-order Functional Logic Language" Lecture Notes in Computer Science (Spronger-Verlag)(Proceedings of Sixth International Joint Conference,ALP'97-HOA'97,Southampton). 1298. 99--113 (1997)
• [文献書誌] M.Hamada and T.Ida: "Deterministic and non-deterministic Lazy Conditional Narrowing and their implementations" Journal of Information Processing Society of Japan. Vol.79,No.3. (1998)
• [文献書誌] S.Feng, T.Sakabe, Y.Inagaki: "Confluence Property of Simple Frames in Dynamic Term Rewriting Calculus" IEICE Transactions on Information and Systems. vol.E80-D,no.6. 625--645 (1997)
• [文献書誌] 結縁祥治, 坂部俊樹, 稲垣康善: "正則な実時間通信プロセスに対するテスト擬順序の記号的特性化" 電子情報通信学会 論文誌. vol.J80-D-I,no.6. 474--485 (1997)
• [文献書誌] Yoshiaki Minamisawa, Masahiko Tomoishi and Naoki Yonezaki: "A New semantics for Linear Logic and its Completeness" Information modeling and knowledge bases. Vol.VIII. 155--166 (1997)
• [文献書誌] Shigeki Hagihara and Naoki Yonezaki: "A Connection based proof method for Modal logic restricted to Discrete frames" Poster Session Abstracts,Fifteenth International Conference on Artificial Intelligence. 43 (1997)
• [文献書誌] 森亮靖、友石正彦、米崎直樹: "時相論理によるリアクティブシステム仕様の実現可能性に関する分類" 日本ソフトウェア科学会論文誌. (1998)
• [文献書誌] 萩谷昌己, 高橋孝一: "「計算=編集」パラダイムに従うHOLタクティクのためのEmacsインタフェース" インタラクティブシステムとソフトウェアV,レクチャーノート/ソフトウェア学(近代科学社). Vol.18. 123--128 (1997)
• [文献書誌] Yasuaki Takebe and Masami Hagiya: "A User Interface for Controlling Term Rewriting Based on Computing-as-Editing Paradigm" User Interfaces for Theorem Provers UITP'97,INRIA Sophia-Antipolis. 93--100 (1997)
• [文献書誌] Wei-Ngun CHIN, Masami HAGIYA: "A Bounds Inference Method for Vector-Based Memoization" International Conference on Functional Programming'97. 176--187 (1997)
• [文献書誌] Takayasu Ito, Toshihiro Asai: "Timed-GC for a Real-Time Lisp System" Proceedings of ACM SIGPLAN Workshop on Languages,Compilers and Tools for Real-Time Systems. 56--67 (1997)
• [文献書誌] Max Kanovich, Takayasu Ito: "Temporal Linear Logic Specifications for Concurrent Processes" Proceedings of IEEE Symposium on Logic in Computer Science. 48--57 (1997)
• [文献書誌] 伊藤貴康: "LISP言語国際標準化と日本の貢献" 情報処理. 第38巻10号. 932--937 (1997)
• [文献書誌] 川本真一、伊藤貴康: "スティール評価法を備えたPaiLispシステムの実現とその評価" 情報処理学会論文誌. 第39巻3号. (1998)
• [文献書誌] Takayasu Ito: "An Efficient Evaluation Strategy for Concurrency Constructs in Parallel Scheme Systems" Advanced Lisp Technology in Japan,Information Processing Society of Japan(Gordon and Breach)<to be published>. (1998)
• [文献書誌] Takayasu Ito, Shin-ichi Kawamoto, and Masayoshi Umehara: "A Multi-Threaded Implementation of PaiLisp Interpreter and Compiler Using the Steal-Help Evaluation Strategy" Advanced Lisp Technology in Japan,Information Processing Society of Japan(Gordon and Breach)<to be publishied>. (1998)
• [文献書誌] 米崎直樹: "計算論入門" 日本評論社, 211 (1998)
• [文献書誌] 萩谷昌己: "関数プログラミング" 日本評論社, 242 (1998)