プログラム言語における型の論理

点击翻译按钮获取中文摘要

型と論理式、プログラムと証明の対応によるプログラムの形式的開発において、プログラムが満足できる程度の自然なプログラムの開発ができる型理論の研究の一環として、従来の型理論や、林の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に基づく型理論に変更した。