| 研究分担者 |
水谷 哲也 筑波大学, 電子・情報工学系, 講師 (70209758)
坂井 公 筑波大学, 数学系, 助教授 (20241797)
細野 千春 筑波大学, 電子・情報工学系, 助教授 (20108294)
塩 雅之 筑波大学, 電子・情報工学系, 助手 (60302395)
富田 康治 通商産業省, 工業技術院・機械技術研究所, 研究員 (80357574)
|
|---|
| 研究概要 |
諭理的プログラムに関する研究は,現代のプログラム理論において重要な問題の1つである.本研究では,解析的意味論を基にした解析的同値理論及び実時間プログラム検証体系SOFA,エンヴェロープ理論tense arithmetic等により,論理的プログラム・システム及びその検証系を構築した.解析的意味論で用いられるν-定義可能行為はプログラムを高階の数学理論の言語で表現するものであり,数学的,論理的に厳密な理論を展開することができる.またSOFA,tense arithmetic等の実時間プログラム検証体系はビークルの制御系や生ピアノの自動重奏システムなどの連続的に変化する外部の物理系を離散的に制御するプログラム系を検証するシステムである.
本年度は昨年度までに引続き連続変化外部系を離散的に制御するプログラム系のtense arithmeticによる検証・解析システムの研究を行なうとともに,実時間システムの例題のひとつである音楽情報処理分野においては,楽曲構造に着目することにより,
・実時間重奏システムの形式的理論的表現＼＼
・演奏ルールの形式的理論的表現＼＼
・それらの成果に基づいた楽曲分析システム,実時間重奏システムの実装
を研究し,成果を得た.
|
