### 抄録

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

### ASJC Scopus subject areas

- Computational Theory and Mathematics

### これを引用

*Theoretical Computer Science*,

*173*(2), 349-391.

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

研究成果: Article

*Theoretical Computer Science*, 巻. 173, 番号 2, pp. 349-391.

}

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 -