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

1995 年度 実績報告書

• 研究課題/領域番号: 05302011
• 研究機関: 千葉大学
• 研究代表者: 辻 尚史 千葉大学, 理学部, 教授 (70016666)
• 研究分担者: 一松 信 東京電機大学, 理工学部, 教授 (10027378) ; 小野 寛晰 北陸先端科学技術大学院大学, 情報科学研究科, 教授 (90055319) ; 難波 完爾 東京大学, 大学院・数理科学研究所, 教授 (40015524) ; 米田 信夫 東京電機大学, 理工学部, 教授 (50080487) ; 五十嵐 滋 筑波大学, 電子情報工学系, 教授 (80027367)
• キーワード: NU / envelope system / 音楽情報処理 / PSYCHE / オブジェクト指向

研究概要

各研究分担者は、解析的意味論に基づく述語論理的プログラム言語NUの理論の構築及び処理系の作成等を行なった。NUは、論理的プログラム言語であるうえに手続き的な表現ができ、さらにプログラムの要求仕様と相互に変換が容易であるという特徴をもつ。主な研究業績は、以下の2項目である。
1.解析的意味論の研究として、以下の2点について一定の成果が得られ、それらを公表した。
(1)実時間並行プロセスに関する諸問題を表現・解析する時制算術に位相空間の概念を導入したenvelope systemと呼ぶ検証システムについて、実時間を陽に表現できるように研究・改良した。また具体的な並行プログラム系の検証に適用した。
(2)envelope systemで導入されたプロセスのスケジューラを一般化した概念である拍車に着目したプログラム検証法を発案し、具体的な並行プログラム系の検証を行なった。
2.高度に知的な人工知能的課題である音楽情報処理について、PSYCHEと呼ぶピアノなどのアコースティック楽器による表情豊かな美しい演奏を目指した研究を進めた。そこで以下の3点の研究について一定の成果が得られ、それらを公表した。
(1)演奏家の演奏の特徴を定量的に抽出し解析するとともに、それらを2次曲線や図形を用いて表現し、音楽の構造について研究を行なった。
(2)生ピアノ等の制御に遅延を伴う楽器を用いて自動伴奏を行う実時間制御システムについて研究・開発を行なった。この中には、演奏家の演奏を模倣するシステムを含んでいる。
(3)音楽ソフトウェアの統合的環境についてオブジェクト指向に基づく研究・開発を行なった。
また12月に研究集会を開催し、基礎的意見交換、研究発表、及び総括的討論を行なった。なお東京電機大学米田信夫教授の研究費は研究の都合で代表者経理にした。

研究成果

• [文献書誌] Shigeru Igarashi, Tetsuya Mizutani, Takashi Tsuji and Chiharu Hosono: "On locomorphism in analytical equivalence theory" Lecture Notes in Computer Science. 792. 173-187 (1994)
• [文献書誌] Kohji Tomita, Takashi Tsuji and Shigeru Igarashi: "Analysis of a Software/Hardware System by Tense Arythmetic" Lecture Notes in Computer Science. 792. 188-205 (1994)
• [文献書誌] Chiharu Hosono and Yasuo Ikeda: "A formal derivation of the decidability of the theory SA" Theoretical Computer Science. 127. 1-23 (1994)
• [文献書誌] 池田靖雄,細野千春,辻尚史: "プログラム言語BQLとその処理系" 情報処理学会論文誌. 37. 印刷中 (1996)
• [文献書誌] 富田康治,辻尚史,五十嵐滋: "プログラムにおける実時間問題のv-転換による解析と動作条件" 情報処理学会論文誌. 34. 1099-1106 (1993)
• [文献書誌] Yasuhito Mukouchi and Setsuo Arikawa: "Towards a mathematical theory of machine discovery from facts" Theoretical Computer Science. 137. 53-84 (1995)
• [文献書誌] Jianjun Zhao, Jingde Cheng and Kazuo Ushijima: "Literal dependence net and its use in concurrent logic programming environment" Proceeding of the Workshop on Parallel Logic Programming attached to FGCS′94. 127-141 (1994)
• [文献書誌] Jianjun Zhao, Jingde Cheng and Kazuo Ushijima: "Theoretical and experimental study of dependence-based complexity metrics for distributed programs" Proceedings of the Fourth International Conference for Young Computer Scientiste. 345-352 (1995)
• [文献書誌] R. Hori, H. Ono and H. Schellinx: "Extending intuitionistic linear with knotted structural rules" Notre Dame Journal of Formal Logic. 35. 219-242 (1994)
• [文献書誌] Robert K. Meyer and Hiroakira Ono: "The finite model property for BCK and BCIW" Studia Logica. 53. 107-118 (1994)
• [文献書誌] Hiroakira Ono: "Algebraic semantics for predicate logics and their completeness" Logic at work. (co appear).
• [文献書誌] Hiroakira Ono: "Decidability and finite model property of substructural logics" Proceedings of the Tbilisi Symposium of Language, Logic and Computation. (co appear).
• [文献書誌] Masami Hagiya: "A Typed λ-Calculus for Proving-by-Example and Bottom-Up Generalization Procedure" Theoretical Computer Science. 137. 3-23 (1995)
• [文献書誌] Wei-Ngan Chin and Masami Hagiya: "A Transformation Method for Dynamic-Sized Tabulation" Acta Informatica. 32. 93-115 (1995)
• [文献書誌] Masami Hagiya and Tomoki Shiratori: "Programming by Example in Computing-as-Editing Paradigm" Proceedings of the 11th International IEEE Symposium. 275-283 (1995)
• [文献書誌] Masami Hagiya and Kouhei Iino: "Binding Time Analysis for Data Type Specialization" Fuji International Workshop on Functional and Logic Programming. 254-269 (1995)
• [文献書誌] Mituharu Yamanoto, Shin-ya Nishizaki Masami Hagiya and Yozo Toda: "Formalization of Planar Graphs" Lecture Notes in Computer Science.971. 369-384 (1995)
• [文献書誌] Susumu Hayasji and Satoshi Kobayashi: "A new formalization of Feferman′s system of functions and classes and its relation to Frege structure" International Journal of Foundations of Computer Science. 6. 187-202 (1995)
• [文献書誌] 大芝猛: "自動証明における自然な証明生成への一つの近接" 情報処理学会論文誌. 35. 222-281 (1995)
• [文献書誌] 大芝猛,小橋一秀: "知識命題の標準系を用いる妥当性検証" 数理解析研究所講究録. 906. 132-135 (1995)
• [文献書誌] 前野年紀,太田昌孝: "パイプラインとキャッシュを活用するためのプログラミグ技法" 第35回プログラミングシンポジウム報告集. 31-42 (1994)
• [文献書誌] Kenji Yoshida, Kunihiko Hayashi and Kazunori Miyoshi: "Programming music system "Z-MUSIC" as an texteded instrument" Proceedings of MCHA95. 1-4 (1995)
• [文献書誌] 木下孝,牧野潔夫,三好和徳: "Fraction-freeによる行列式の計算効率" 数理科学講究録. 920. 62-73 (1995)
• [文献書誌] 一松信: "基礎微分積分学入門" 近代科学社, (1995)