Inductive-data-type systems

Frédéric Blanqui, Jean Pierre Jouannaud, Mitsuhiro Okada

Research output: Contribution to journalArticle

40 Citations (Scopus)

Abstract

In a previous work ("Abstract Data Type Systems", TCS 173(2), 1997), the last two authors presented a combined language made of a (strongly normalizing) algebraic rewrite system and a typed λ-calculus enriched by pattern-matching definitions following a certain format, called the "General Schema", which generalizes the usual recursor definitions for natural numbers and similar "basic inductive types". This combined language was shown to be strongly normalizing. The purpose of this paper is to reformulate and extend the General Schema in order to make it easily extensible, to capture a more general class of inductive types, called "strictly positive", and to ease the strong normalization proof of the resulting system. This result provides a computation model for the combination of an algebraic specification language based on abstract data types and of a strongly typed functional language with strictly positive inductive types.

Original languageEnglish
Pages (from-to)41-68
Number of pages28
JournalTheoretical Computer Science
Volume272
Issue number1-2
DOIs
Publication statusPublished - 2002 Feb 6

Fingerprint

Abstract data types
Type Systems
Abstract Data Types
Strictly positive
Schema
Specification languages
Pattern matching
Algebraic Specification
Strong Normalization
Specification Languages
Pattern Matching
Natural number
Calculus
Generalise
Language
Model

Keywords

  • Higher-order rewriting
  • Inductive types
  • Recursive definitions
  • Strong normalization
  • Typed lambda-calculus

ASJC Scopus subject areas

  • Computational Theory and Mathematics

Cite this

Inductive-data-type systems. / Blanqui, Frédéric; Jouannaud, Jean Pierre; Okada, Mitsuhiro.

In: Theoretical Computer Science, Vol. 272, No. 1-2, 06.02.2002, p. 41-68.

Research output: Contribution to journalArticle

Blanqui, Frédéric ; Jouannaud, Jean Pierre ; Okada, Mitsuhiro. / Inductive-data-type systems. In: Theoretical Computer Science. 2002 ; Vol. 272, No. 1-2. pp. 41-68.
@article{3b6aae834c264aef96f9938e9f541ab3,
title = "Inductive-data-type systems",
abstract = "In a previous work ({"}Abstract Data Type Systems{"}, TCS 173(2), 1997), the last two authors presented a combined language made of a (strongly normalizing) algebraic rewrite system and a typed λ-calculus enriched by pattern-matching definitions following a certain format, called the {"}General Schema{"}, which generalizes the usual recursor definitions for natural numbers and similar {"}basic inductive types{"}. This combined language was shown to be strongly normalizing. The purpose of this paper is to reformulate and extend the General Schema in order to make it easily extensible, to capture a more general class of inductive types, called {"}strictly positive{"}, and to ease the strong normalization proof of the resulting system. This result provides a computation model for the combination of an algebraic specification language based on abstract data types and of a strongly typed functional language with strictly positive inductive types.",
keywords = "Higher-order rewriting, Inductive types, Recursive definitions, Strong normalization, Typed lambda-calculus",
author = "Fr{\'e}d{\'e}ric Blanqui and Jouannaud, {Jean Pierre} and Mitsuhiro Okada",
year = "2002",
month = "2",
day = "6",
doi = "10.1016/S0304-3975(00)00347-9",
language = "English",
volume = "272",
pages = "41--68",
journal = "Theoretical Computer Science",
issn = "0304-3975",
publisher = "Elsevier",
number = "1-2",

}

TY - JOUR

T1 - Inductive-data-type systems

AU - Blanqui, Frédéric

AU - Jouannaud, Jean Pierre

AU - Okada, Mitsuhiro

PY - 2002/2/6

Y1 - 2002/2/6

N2 - In a previous work ("Abstract Data Type Systems", TCS 173(2), 1997), the last two authors presented a combined language made of a (strongly normalizing) algebraic rewrite system and a typed λ-calculus enriched by pattern-matching definitions following a certain format, called the "General Schema", which generalizes the usual recursor definitions for natural numbers and similar "basic inductive types". This combined language was shown to be strongly normalizing. The purpose of this paper is to reformulate and extend the General Schema in order to make it easily extensible, to capture a more general class of inductive types, called "strictly positive", and to ease the strong normalization proof of the resulting system. This result provides a computation model for the combination of an algebraic specification language based on abstract data types and of a strongly typed functional language with strictly positive inductive types.

AB - In a previous work ("Abstract Data Type Systems", TCS 173(2), 1997), the last two authors presented a combined language made of a (strongly normalizing) algebraic rewrite system and a typed λ-calculus enriched by pattern-matching definitions following a certain format, called the "General Schema", which generalizes the usual recursor definitions for natural numbers and similar "basic inductive types". This combined language was shown to be strongly normalizing. The purpose of this paper is to reformulate and extend the General Schema in order to make it easily extensible, to capture a more general class of inductive types, called "strictly positive", and to ease the strong normalization proof of the resulting system. This result provides a computation model for the combination of an algebraic specification language based on abstract data types and of a strongly typed functional language with strictly positive inductive types.

KW - Higher-order rewriting

KW - Inductive types

KW - Recursive definitions

KW - Strong normalization

KW - Typed lambda-calculus

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

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

U2 - 10.1016/S0304-3975(00)00347-9

DO - 10.1016/S0304-3975(00)00347-9

M3 - Article

AN - SCOPUS:0037028509

VL - 272

SP - 41

EP - 68

JO - Theoretical Computer Science

JF - Theoretical Computer Science

SN - 0304-3975

IS - 1-2

ER -