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

1991 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 Objects and Inductive Definition Mechanisms to Frege Structures" Proceedings of Theoretical Aspects of Computer Software. 53-87 (1991)
• [Publications] 龍田 真: "型理論I" コンピュタソフトウェア. 8ー1. 25-33 (1991)
• [Publications] 龍田 真: "型理論II" コンピュ-タソフトェア. 8ー2. 40-46 (1991)
• [Publications] 龍田 真: "型理論III" コンピュ-タソフトェア. 8ー3. 2-8 (1991)
• [Publications] 龍田 真: "型理論IV" コンピュ-タソフトェア. 8ー4. 56-68 (1991)
• [Publications] M.Tatsuta: "Monotone Recursive Delfinition of Predicates and Its Realizability Interpretation" Proceedings of Theoretical Aspects of Computer Software. 38-52 (1991)
• [Publications] M.Tatsuta: "Program Synthesis Using Realizability" Theoretical Computer Science. 90. 309-353 (1991)
• [Publications] 亀山 幸義: "構成的数学体系RPTに基づく超数学定理の形式化" 情報処理学会第42回全国大会. 1. 47-48 (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] J.Cheng,Y.Kasahara,K.Ushijima: "A Tasking Deadlock Detector for Ada Programs" Proc.IEEE 15th Annual COMPSAC. 56-62 (1991)
• [Publications] 有川 節夫,西野 哲朗: "学習における計算論的アプロ-チ" 情報処理学会誌. 32ー3. 217-225 (1991)
• [Publications] 野下 浩平,角田 博保: "長い可変長文字列の挿入操作に関する一考察" 情報処理学会論文誌. 32ー5. 665-672 (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] K.Noshita: "A Program for solving Tsume‐shogi quickly and accurately" Proc.of the Game Playing System Workshop. 56-59 (1991)
• [Publications] Y.Ichisugi and A.Yonezawa: "Exception Handing and Real Time Features in an Object‐Oriented Concurrent Language" Concurrency:Theory,Language,and Architecture‐UK/Japan Workshop,Oxford,September 1989,Proceedings‐Springer Lecture Notes in Computer Science. 491. 92-109 (1991)
• [Publications] T.Watanabe and A.Yonezawa: "An Actor‐Based Metalevel Architectur for Group‐Wide Reflection" Foundations of Object‐Oriented Languages,REX School/Workshop,Noordwijkerhouf,The Netherlands,May/June,1990,Proceedings,Springer Lecture Notes in Computer Science. 489. 405-425 (1991)
• [Publications] S.Matsuoka,T.Watanabe and A.Yonezawa: "Hybrid Group Reflective Architecture for Object‐Oriented Concurrent Reflective Programming" Proceedings of the European Conference on Object‐Oriented Programming(ecoop)'91,Springer Lecture Notes in Computer Science. 512. 231-250 (1991)
• [Publications] S.Matsuoka,S.Furuso,and A.Yonezawa: "A Fast Parallel Conservative Garbage Collector for Concurrent Object‐Oriented Systems" Proceedings of IEEE International Workshop on Object Orientation in Operating Systems,Palo Alto,CA. 87-93 (1991)
• [Publications] S.Matsuoka,T.Watanabe,Y.Ichisugi,and A.Yonezawa: "Object‐Oriented Concurrent Reflective Architectures" Proceedings of Workshop on Object‐Based Concurrent Programming,Geneve,Switzerland,1991,Springer Lecture Notes in Computer Science. (1992)
• [Publications] Y.Ichisugi,S.Matsuoka,T.Watanabe,and A.: "An Object‐Oriented Concurrent Reflective Architecture for Distributed Computing Environments" Proceedings of 29th Annual Allerton Conference on Communication,Control and Computing. (1991)
• [Publications] 杉本 徹,米澤 明憲: "対話理解のための心的状態の多重世界表現形式" 自然言語処理. 83,5. 31-38 (1991)
• [Publications] 渡部 卓雄,松岡 聡,米澤 明憲: "並行オブジェクト指向計算における自己反映計算の一方式" 並列処理シンポジウム論文集. 421-428 (1991)
• [Publications] 古荘 進一,松岡 聡,米澤 明憲: "共有メモリ型並列計算機上のConservative Garbage Collection" 日本ソフトウェア科学会第8会大会論文集. 89-92 (1991)
• [Publications] 八杉 昌宏,米澤 明憲: "N体問題の並列オブジェクト指向アルゴリズム" 日本ソフトウェア科学会第8会大会論文集. 405-408 (1991)
• [Publications] 一杉 裕志,松岡 聡,渡部 卓雄,米澤 明憲: "分散環境のための並列オブジェクト指向言語のリフレクティブア-キテクチャ" 日本ソフトウェア科学会第8会大会論文集. 541-548 (1991)
• [Publications] E.Kiriyama and H.Ono: "The contraction rule and decision problems for logics without structural rules" Studia Logica. 50. 299-319 (1991)
• [Publications] M.Hagiya: "Synthesis of rewrite programs by higher‐order and semantic unification" New Generation Computing. 8,4. 403-420 (1991)
• [Publications] 萩谷 昌己: "高階単一化と証明の一般化" 人工知能学会誌. 6,3. 388-396 (1991)
• [Publications] M.Hagiya: "Higher‐order unification as a theorem proving procedure" Eighth International Conference on Logic Programming. 270-284 (1991)
• [Publications] M.Hagiya(T.Ito and A.R.Meyer eds.): "From programming‐by‐example to proving‐by‐example" Theoretical Aspects of Computer Science,Lecture Notes in Computer Science. 526. 387-419 (1991)
• [Publications] 萩谷 昌己: "視覚的プログラミングと自動プログラミング" コンピュ-タソフトウェア. 8,2. 27-39 (1991)
• [Publications] 大芝 猛: "自動証明における自然な三段論法の導入について" 数理解析研究所講究録. 772. 95-109 (1991)
• [Publications] 佐藤 雅彦,桜井 貴文: "プログラムの基礎理論" 岩波書店, 348 (1991)
• [Publications] I.Ito and A.R.Meyer: "Proceedings of Theoretical Aspects of Computer Software" Springer, 770 (1991)
• [Publications] 榎本 彦衛,加納 幹雄: "グラフの構造" 朝倉書店,
• [Publications] 林 晋,小林 聡: "構成的プログラミングの基礎" 遊星社,
• [Publications] A.Yonezawa and T.Ito: "Concurrency:Theory,Language,and Architecture ‐UK/Japan Workshop,Oxiord,September 1989,Proceedings‐" Springer, 339 (1991)