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

编程语言中的类型逻辑

基本信息

批准号：
02249209
负责人：
林晋
金额：
$ 0.45万
依托单位：
Ryukoku University
依托单位国家：
日本
项目类别：
Grant-in-Aid for Scientific Research on Priority Areas
财政年份：
1990
资助国家：
日本
起止时间：
1990 至无数据
项目状态：
已结题

来源：
https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-02249209/
关键词：
プログラム言語における型理論プログラム検証

项目摘要

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

作为类型理论的研究的一部分，该研究允许使用类型，逻辑公式，程序和证据的对应关系形式地制定自然程序，以正式开发程序的形式满足程序，我们设计和阐明了类型理论（ATT）的基本属性（ATT）的基本属性，该属性扩展了传统类型理论和规格在Hayashi的PX系统中描述方法。 The feature of ATT is that it abolishes the two types πxeA.B (dependent product) and ΣxeA.B (dependent sum), which were considered to be the biggest features of conventional type theory, and introduces the types A→B, A×B, and union and intersection of the type family, as well as the singleton type {M}_A, which are the types of simple typed lambda calculus.结果，在ATT中，依赖性和依赖性产品是由用户定义的类型构造而不是基本类型构造的。在传统类型的理论中，依赖总和和依赖性产品的使用非常模棱两可，以至于它们被迫以不自然的方式使用它们。这是由于缺点，例如，必须将与程序执行无关的证明代码必须作为程序的一部分合并。在ATT中，依赖性总和和依赖性产品被分解为更基本的类型，从而可以创建适合该程序自然含义的详细规范，并可以使常规方法不可能进行规范描述。该ATT最初是基于Martin-Lo ^^°F的类型理论，但在今年晚些时候，我们将其改为基于构造的计算的类型理论。