1990 Fiscal Year Annual Research Report
| Project/Area Number |
02249102
|
|---|
| Research Institution | Tohoku University |
|---|
Principal Investigator |
伊藤 貴康 東北大学, 工学部, 教授 (80124551)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
萩原 兼一 大阪大学, 基礎工学部, 助教授 (00133140)
萩谷 昌己 京都大学, 数理解析研究所, 助教授 (30156252)
佐藤 雅彦 東北大学, 電気通信研究所, 教授 (20027387)
|
|---|
| Keywords | プログラムの論理と証明 / 実行の論理 / 構成的数学体系 / 例によるプログラミング / 例による証明 / 高階ユニフィケ-ション / 並列アルゴリズム / 分散アルゴリズム |
|---|
| Research Abstract |
本研究では,ソフトウエアの基礎理論に関する研究課題のうち,プログラムのモデル・論理・証明・型理論,プログラミングと証明,および並列・分散プログラミングに関する研究を行うことを目的としている。
伊藤は,実行モデルに基づくプログラムの論理を構築するという立場から,実行の論理を提案した。実行の論理をもとに,並行プラセスの理論・制御の論理の試みも行っている。
佐藤は,RPTと言う構成的数学体系を提案し,その数学的な性質について理論的に明らかにすると共に,Λ(ラムダ)と言う言語をRPTを基に設計し,その処理系をLISPを用いて実現した。
萩谷は,例によるプログラミングと例による証明の両者を,関数方程式の形で統一的に定式化し,高階ユニフィケ-ションを用いて関数方程式を解くことにより両者を実現する研究を行い,興味深い結果を得ている。特に,型理論,項書き換え系,LFCLogical Framework)を対象に研究を進め処理系の試作も進めている。
萩原は,複数プロセスでの協調的問題解決の仕方を,並列アルゴリズム法と分散アルゴリズム法に分け,それらによるアルゴリズムの解析・設計・改良のソフトウエア・ツ-ルを設計し,試作している。特に,アルゴリズムの動きを可視化するアニメ-ション・システムを開発している。
なお,公募研究の林晋氏は,ATTと言う新しい構成的タイプ理論を構築し,構成的プログラミングに応用している。また,榎本肇氏は,ソフトウエア記述プロセスとしての情報構造とその操作をオブジェクト指向の形で詳細化し,手続きを得る方法について研究を行った。
|
Research Products
(6 results)
-
[Publications] Ito,Takayasu: "Logic of execution:An outline" Lecture Notes in Computer Science. 491. 79-91 (1991)
-
[Publications] Sato,Masahiko: "Constructive programming in SST" Proceedings of JapaneseーCzechoslovak Seminar on Theoretical Foundations of Konwledge Information Processing. 20-30 (1990)
-
[Publications] Hagiya,Masami: "Programming by example and proving by example using higherーorder unification" Lecture Notes in Computer Science. 448. 588-602 (1990)
-
[Publications] Hagiya,Masami: "Synthesis of rewrite programs by higherーorder and semantic unification" Proceedings of the First International Workshop on Algorithmic Learning Theory. 396-410 (1990)
-
[Publications] 萩原 兼一: "分散アルゴリズム" 情報処理. 31. 1245-1256 (1990)
-
[Publications] 萩原 兼一: "分散アルゴリズム" 人工知能学会誌. 5. 42-52 (1990)
