1988 Fiscal Year Annual Research Report
| Project/Area Number |
62460220
|
|---|
| Research Institution | Tohoku University |
|---|
Principal Investigator |
佐藤 雅彦 東北大学, 電気通信研究所, 教授 (20027387)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
亀山 幸義 東北大学, 電気通信研究所, 助手 (10195000)
|
|---|
| Keywords | 構成的数学 / 関数型プログラム言語 / 直観主義論理 / 証明プログラムの検証 / プログラムの合成 |
|---|
| Research Abstract |
本年度の研究では、(1)前年度にひき続き、構成的数字を形式化した論理体系SST(Symbolic Set Theory)を設計し、SSTの表現力と倫理体系としての性質に関する考察、SSTに含まれるプログラム言語Λの形式的意味の記述、ΛによるSST証明係の実現の手法の検討などの理論的研究、(2)Λの計算機上への実現、ΛによるSST証明系の実現、そのフィードバックによってSSTをより洗練する研究を行った。
SSTの特徴は、(1)項や論理式がS式に基づいた記号表現のなので、計算機による処理に適している、(2)項を構成する際に型の制約がないので一般の再帰的関数を定義できる(SSTの閉項によるプログラム言語をΛとよぶ)、(3)計算の止まらない項を扱う部分項の論理を基礎とするので、プログラムの性質を直接取り扱うことができる、(4)ある論理式を満たす項の集まりを集合として取りこむ規制を持つので、空集合、全体集合、直積、直和、関数空間、集合の集合などの集合を定義することができる。(特に集合の集合の存在は、他の理論には見られない)、(5)帰納的に術語を定義する規則を含んでいるため、自然数やリスト、木などのデータ型も集合として表現することができる、などである。これらの長所により、SSTによって、Λのプログラムの仕様の記述およびその性質の推論をすることが容易になった。また、Λはプログラム言語として十分な能力を持つため、SST自身の証明系をΛで実現することが可能である。今年度は、Λの本格的な処理系を計算機上に実現し、自己評価系やSSTの証明系の基本部分をΛで実現した。これらの過程を通じて、Λにパターン照合の機能が不可欠であること、などが証明し、SST自身の改良をくり返した。前年度の理論的成果である、SSTの無矛盾性、項の存在性の定理等を改良したSSTに対して再び証明した。
|
