1990 Fiscal Year Annual Research Report
| Project/Area Number |
02249209
|
|---|
| Research Institution | Ryukoku University |
|---|
Principal Investigator |
林 晋 龍谷大学, 理工学部・数理情報学科, 助教授 (40156443)
|
|---|
| Keywords | プログラム言語における型理論 / プログラム検証 |
|---|
| Research Abstract |
型と論理式、プログラムと証明の対応によるプログラムの形式的開発において、プログラムが満足できる程度の自然なプログラムの開発ができる型理論の研究の一環として、従来の型理論や、林のPXシステムにおける仕様記述の方法を拡張した型理論ATT(A Type Theory)の設計と、その基本的性質の解明を行った。
ATTの特徴は、従来の型理論の最大の特徴とされていたふたつの型πxeA.B(依存積)とΣxeA.B(依存和)を廃し、simpley typed lambda calculusの型であるA→B,A×B,型の族のunionとintersection、および、singleton type {M}_Aを導入したことである。この結果、ATTでは、依存和、依存積は、基本的型構成子ではなく、ユ-ザ-によって定義させた派生的型構成子となった。従来の型理論では、依存和、依存積を、あまりに多義的に用いていたため、不自然な使い方を余儀なくされていた。例えば、プログラムの実行に関連のない証明のコ-ドを、プログラムの一部として取り込まざるをえない等の欠点は、このことに起因する。ATTでは、依存和,依存積を、より基本的を型に分解したため、プログラムの自然な意味にあった詳細な仕様記述がおこなえるようになったばかりでなく、従来の方法では不可能な仕様記述も行なえるようになった。
ATTは、当初,MartinーLo^^°fの型理論に基づいていたが、本年度の後半の研究により、Calculus of Contructionに基づく型理論に変更した。
|
-
[Publications] 高山 幸秀・林 晋: "Extended projection method with KreiselーTroelstra realizability" Information and Computation.
-
[Publications] 八杉 満利子・林 晋: "A functional system with transfinitely defined types" 日本数学会1991年春季総合分利会.
-
[Publications] 井田 哲雄編: "続 新しいプログラミング・パラダイム" 共立出版, (1990)
-
[Publications] 林 晋・小林 聡: "構成的プログラミングの基礎" 遊星社, (1991)
