Inductive-Data-Type Systems-英文文献.pdf

Theoretical Computer Science 272 (2002) 41–68 /locate/tcs Inductive-data-type systems a ; ∗ a b Frederic Blanqui , Jean-Pierre Jouannaud , Mitsuhiro Okada a ˆ LRI, Bat. 490, Universite Paris-Sud 91405 Orsay, France b Department of Philosophy, Keio University, 108 Minatoku, Tokyo, Japan 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 denitions following a certain format, called the “General Schema”, which generalizes the usual recursor denitions 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 specication language based on abstract data types c and of a strongly typed functional language with strictly positive inductive types. 2002 Elsevier Science B.V. All rights reserved. Keywords: Higher-order rewriting; Strong normalization; Inductive