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

1991 年度 実績報告書

• 研究課題/領域番号: 02302009
• 研究機関: 東北大学
• 研究代表者: 佐藤 雅彦 東北大学, 電気通信研究所, 教授 (20027387)
• 研究分担者: 亀山 幸義 東北大学, 電気通信研究所, 助手 (10195000) ; 龍田 真 東北大学, 電気通信研究所, 助手 (80216994)
• キーワード: プログラム理論 / 直観主義論理 / 型理論 / グラフ理論

研究概要

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

研究成果

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