高機能高品質ソフトウェアの基礎理論

高性能、高质量软件的基础理论

• 批准号: 03235102
• 负责人: 伊藤 貴康
• 金额: $ 7.36万
• 依托单位: Tohoku University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research on Priority Areas
• 财政年份: 1991
• 资助国家: 日本
• 起止时间: 1991 至 无数据
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-03235102/
• 关键词: プログラム・モデル; 論理と証明; 型理論ATTT; 並列プログラミング; 並列プロセス計算σー計算; 構成的数学体系RPT; 例による証明; アルゴリズム・アニメ-ション

高機能高品質ソフトウェアの基礎理論に関して,次のような研究を行った。[1]プログラムのモデルと論理に関する研究(担当:伊藤)並列プログラムにおける同時並列性を表現するための理論モデルと論理体系についての研究を行った。結合律を満す並列合成だけでなく,結合律を満さない並列合成をも有する強力な並列プロセス計算σー計算の提案を行った。また,代数的ペトリネットを提案し,プロセスとネットの関係を明らかにした。[2]プログラムの論理と証明に関する研究(担当:佐藤)構成的数学の体系RPTに基づき,構成的プログラミングを実践するための一連のシステムを計算機上に構築し,それを用いて実際に証明を構成することを試みた。[3]プログラミングと証明に関する研究(担当:萩谷)例による証明とプログラミングに関するヒュ-リスティック戦略について研究を深めた。また,構成的体系CCの証明チェッカを開発した。[4]プログラムの証明論と型理論に関する研究(担当:林)論理的仕様からの構成的プログラム抽出のための型理論ATTを改良したATTTという型理論を設計し,その理論的性質について研究を行った。[5]並列プログラミングパラダイムに関する研究(担当:萩原)並列・分散アルゴリズムのためのプログラミングパラダイムを確立する研究の一環として,並列計算モデルのアルゴリズム・アニメ-ション・システムAASをいくつかの計算モデルに対して試作し,改良も行った。また,超立方体状ネットワ-クでの置装ル-ティングに対し決定性アルゴリズムと確率アルゴリズムをシミュレ-ションにより評価した。

High function, high quality software, basic theory, research, etc. [1]Research on the relationship between the logic and the theory of parallel logic system (responsible: Ito) The combination law is parallel to the synthesis law. The combination law is parallel to the synthesis law. The relationship between algebra and life is clear. [2]A mathematical system consisting of a set of logic and proofs is constructed on a computer. [3]For example, if you want to prove that you are interested in the research, please contact us. The proof of CC system is developed. [4]A study on the relationship between the theory of logic and the theory of type (responsibility: Lin) A study on the nature of logic and the theory of type (ATT). [5]The research on the relationship between the parallel and decentralized systems (responsibility: Hagihara) is part of the research on the establishment of the parallel and decentralized systems, and the parallel calculation of the parallel and decentralized systems is part of the calculation and improvement of the system. In addition, the hypercube shape of the product is determined by the accuracy of the product.

项目成果

Masahiko Sato(佐藤 雅彦): "An Abstraction Mechanism for Symbolic Expressions" Artificial Intelligence and Mathematical Theory of Computation(Academic Press). 381-391 (1991)

佐藤正彦：“符号表达的抽象机制”人工智能与数学计算理论（学术出版社）381-391（1991）。

Takayasu Ito(伊藤 貴康): "Lisp and parallelism" Artificial Intelligence and Mathematical Theory of Computation(Academic Press). 187-206 (1991)

伊藤贵康：《Lisp与并行》《人工智能与数学计算理论》（学术出版社）187-206（1991）。

Masahiko Sato(佐藤 雅彦): "Adding Proof Objects and Inductive Definition Mechanisms to Frege Structures" Lecture Notes in Computer Science (SpringerーVerlag). 526. 53-87 (1991)

Masahiko Sato：“向弗雷格结构添加证明对象和归纳定义机制”计算机科学讲义（Springer-Verlag）526. 53-87（1991）。

Masami Hagiya(萩谷 昌己): "From programmingーbyーexample to provingーbyーexample" Lecture Notes in Computer Science (SpringerーVerlag). 526. 387-419 (1991)

Masami Hagiya：“从示例编程到示例证明”计算机科学讲义 (Springer-Verlag) 526. 387-419 (1991)。

萩原 兼一: "分散協調問題解決と分散アルゴリズム" 大阪大学知識科学研究会第6回年次大会資料集. 96-111 (1991)

Kenichi Hagiwara：《分布式协作问题解决与分布式算法》大阪大学知识科学研究组第6届年会资料96-111（1991）。