プログラム基礎理論の総合的研究

1992 Fiscal Year Annual Research Report

• Project/Area Number: 02302009
• Research Institution: Tohoku University
• Principal Investigator: 佐藤 雅彦 東北大学, 電気通信研究所, 教授 (20027387)
• Co-Investigator(Kenkyū-buntansha): 亀山 幸義 東北大学, 電気通信研究所, 助手 (10195000) ; 龍田 真 東北大学, 電気通信研究所, 助手 (80216994)
• Keywords: プログラム理論 / 直観主義論理 / 型理論 / グラフ理論

Research Abstract

計算機は現在、社会のいたるところで使われるようになっているが、その需要の爆発的増加にプログラム作成者の育成が追いつかず、いわゆるプログラムの危機とよばれる状態が予見されている。また、人間が作成したプログラムは必然的に誤りをともなうものであり、そのプログラムが要求仕様を満たすかどうかの保証がない。これらの状況に多処するためには、要求仕様、作成、保守の各段階において、プログラムの基礎的諸理論を統合し、数学的理論に基づいた厳密な方法が必要とされる。また、これらを自動化するめ、数理的に系統化された理論の研究とそれに基づく処理系の開発が不可欠である。こうした見地に立ち、本研究では、各研給分担者は、(1)基礎数理、(2)応用数理、(3)プログラミングの3つの主題について、プログラミングの基礎となる理論の構築、理論に基づくプログラム開発方式の研究、実際の応用プログラムの開発を行った。主要な研究実績として、直観主義論理、証明論、カテゴリー論、型理論、λ計算、項書き替え系、再帰的関数論、様相論理、スコット理論、組み合わせ論、グラフ理論、代数学などの基礎的諸理論について考察し、相互の関連を検討した。特に、直観主義論理に基づく体系RPTを発展させ、プログラムの検証、合成システムを実際に計算機上に実現した。また、論理型プログラム、関数型プログラム、対象指向プログラムなどの処理系について研究を行った。また、前年にひき続き、これらの研究活動の成果を発表する機会として、研究集会を開催し、相互の研究の理解を深めた。

Research Products

• [Publications] M. Sato: "Adding Proof Pbjects and Inductive Definition Mechanisms to Frege Structures" Proceedings of Theoretical Axpects of Computer Softwara. 53-87 (1991)
• [Publications] M. Tatsuta: "Realizability Interpretation of Coinductive Definitions and Program Synthesis with Streams" Theoretical Comrpter Sceince.
• [Publications] M. Tatsuta: "Unequeness of normal proofs of minimal formulas" Journal of Symbolic Logic.
• [Publications] 亀山 幸義: "講成的数学体系RPTに基づく超数学定理の形式化" 情報処理学会第42回全国大会. 1. 47-48 (1991)
• [Publications] 有川 節夫,西野 哲朗: "学習における計算論的アプローチ" 情報処理学会誌. 32-3. 217-225 (1991)
• [Publications] J. Cheng and K. Ushijima: "Analyzing Ada Tasking Deadlocks and Livelocks Using Extended Petri Nets" Lecture Notes in Computer Science. 499. 125-146 (1991)
• [Publications] K.Noshita and Y.Nakatani: "A note on deleting the maximum element in nested s-heaps" Trans. of IECEJ. E73,10. 1725-1726 (1990)
• [Publications] E.Kiriyama and H.Ono: "The contraction rule and decision decision problems for logics without structural rules" Studia Logica. 50. 299-319 (1991)
• [Publications] 萩谷 昌己: "高階単一化と証明の一般化" 人工知能学会誌. 6,3. 388-396 (1991)
• [Publications] M. Hagiya: "Higher-order unefication as atheorem proving Procedure" Eighth International Conference on Logic Programming. 270-284 (1991)
• [Publications] 佐藤 雅彦,桜井 貴文: "プログラムの基礎理論" 岩波書店, 348 (1991)
• [Publications] I.Ito and A.R.Meyer: "Proceedings of Theoretical Aspects of Computar Software" Springer, 770 (1991)
• [Publications] 林 晋,小林 聡: "構成的プログラミングの基礎" 遊星社, 254 (1991)
• [Publications] 龍田 真: "型理論" 近代科学社, 82 (1992)