Abstract data type systems

Jean Pierre Jouannaud, Mitsuhiro Okada

研究成果: Article

41 引用 (Scopus)

抄録

This paper is concerned with the foundations of an extension of pure type systems by abstract data types, hence the name of Abstract Data Type Systems. ADTS generalize inductive types as they are defined in the calculus of constructions, by providing definitions of functions by pattern matching on the one hand, and relations among constructors of the inductive type on the other. It also generalizes the first-order framework of abstract data types by providing function types and higher-order equations. The first half of the paper describes the framework of ADTS, while the second half investigates cases where ADTS are strongly normalizing. This is shown to be the case for the polymorphic lambda calculus (with possibly subtypes) enriched by higher-order algebraic rules obeying a strong generalization of primitive recursion of higher type that we call the general schema. This covers in particular the case of inductive types whose constructors do not have functional arguments. We conjecture that this result holds true for all calculi of the so-called Barendregt's cube. On the other hand, the definition of a schema for the higher-order rules allowing for more general inductive types is left open.

元の言語English
ページ(範囲)349-391
ページ数43
ジャーナルTheoretical Computer Science
173
発行部数2
出版物ステータスPublished - 1997 2 28

Fingerprint

Abstract data types
Abstract Data Types
Type Systems
Schema
Calculus
Higher Order
Generalise
Higher order equation
Lambda Calculus
Pattern matching
Pattern Matching
Recursion
Regular hexahedron
Cover
First-order
Framework

ASJC Scopus subject areas

  • Computational Theory and Mathematics

これを引用

Jouannaud, J. P., & Okada, M. (1997). Abstract data type systems. Theoretical Computer Science, 173(2), 349-391.

Abstract data type systems. / Jouannaud, Jean Pierre; Okada, Mitsuhiro.

:: Theoretical Computer Science, 巻 173, 番号 2, 28.02.1997, p. 349-391.

研究成果: Article

Jouannaud, JP & Okada, M 1997, 'Abstract data type systems', Theoretical Computer Science, 巻. 173, 番号 2, pp. 349-391.
Jouannaud JP, Okada M. Abstract data type systems. Theoretical Computer Science. 1997 2 28;173(2):349-391.
Jouannaud, Jean Pierre ; Okada, Mitsuhiro. / Abstract data type systems. :: Theoretical Computer Science. 1997 ; 巻 173, 番号 2. pp. 349-391.
@article{1075afa999f9437bbc438950c676739f,
title = "Abstract data type systems",
abstract = "This paper is concerned with the foundations of an extension of pure type systems by abstract data types, hence the name of Abstract Data Type Systems. ADTS generalize inductive types as they are defined in the calculus of constructions, by providing definitions of functions by pattern matching on the one hand, and relations among constructors of the inductive type on the other. It also generalizes the first-order framework of abstract data types by providing function types and higher-order equations. The first half of the paper describes the framework of ADTS, while the second half investigates cases where ADTS are strongly normalizing. This is shown to be the case for the polymorphic lambda calculus (with possibly subtypes) enriched by higher-order algebraic rules obeying a strong generalization of primitive recursion of higher type that we call the general schema. This covers in particular the case of inductive types whose constructors do not have functional arguments. We conjecture that this result holds true for all calculi of the so-called Barendregt's cube. On the other hand, the definition of a schema for the higher-order rules allowing for more general inductive types is left open.",
author = "Jouannaud, {Jean Pierre} and Mitsuhiro Okada",
year = "1997",
month = "2",
day = "28",
language = "English",
volume = "173",
pages = "349--391",
journal = "Theoretical Computer Science",
issn = "0304-3975",
publisher = "Elsevier",
number = "2",

}

TY - JOUR

T1 - Abstract data type systems

AU - Jouannaud, Jean Pierre

AU - Okada, Mitsuhiro

PY - 1997/2/28

Y1 - 1997/2/28

N2 - This paper is concerned with the foundations of an extension of pure type systems by abstract data types, hence the name of Abstract Data Type Systems. ADTS generalize inductive types as they are defined in the calculus of constructions, by providing definitions of functions by pattern matching on the one hand, and relations among constructors of the inductive type on the other. It also generalizes the first-order framework of abstract data types by providing function types and higher-order equations. The first half of the paper describes the framework of ADTS, while the second half investigates cases where ADTS are strongly normalizing. This is shown to be the case for the polymorphic lambda calculus (with possibly subtypes) enriched by higher-order algebraic rules obeying a strong generalization of primitive recursion of higher type that we call the general schema. This covers in particular the case of inductive types whose constructors do not have functional arguments. We conjecture that this result holds true for all calculi of the so-called Barendregt's cube. On the other hand, the definition of a schema for the higher-order rules allowing for more general inductive types is left open.

AB - This paper is concerned with the foundations of an extension of pure type systems by abstract data types, hence the name of Abstract Data Type Systems. ADTS generalize inductive types as they are defined in the calculus of constructions, by providing definitions of functions by pattern matching on the one hand, and relations among constructors of the inductive type on the other. It also generalizes the first-order framework of abstract data types by providing function types and higher-order equations. The first half of the paper describes the framework of ADTS, while the second half investigates cases where ADTS are strongly normalizing. This is shown to be the case for the polymorphic lambda calculus (with possibly subtypes) enriched by higher-order algebraic rules obeying a strong generalization of primitive recursion of higher type that we call the general schema. This covers in particular the case of inductive types whose constructors do not have functional arguments. We conjecture that this result holds true for all calculi of the so-called Barendregt's cube. On the other hand, the definition of a schema for the higher-order rules allowing for more general inductive types is left open.

UR - http://www.scopus.com/inward/record.url?scp=0031074199&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=0031074199&partnerID=8YFLogxK

M3 - Article

AN - SCOPUS:0031074199

VL - 173

SP - 349

EP - 391

JO - Theoretical Computer Science

JF - Theoretical Computer Science

SN - 0304-3975

IS - 2

ER -