Inductive-data-type Systems. F. Blanqui, J.-P. Jouannaud and M. Okada. TCS 272, 30 pages, 2002.

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 lambda-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.

Erratum:

• Definition 3 (strictly positive types and basic types). Instead of "An inductive type s is said to be strictly positive if it does not occur or occurs strictly positively in the types of the arguments of its constructors, and no type I-equivalent to s occurs at a negative position in the types of the arguments of the constructors of s. A strictly positive type is basic if its constructors have no functional arguments.", read: "An inductive type s is said to be strictly positive if, for every constructor C:s₁→...→s_n→s and every i ∈ {1,...,n}, s_i is of the form t₁→...→t_k→t and, for every j ∈ {1,...,k}, no inductive type equivalent to s occurs in t_j. It is basic if, for every constructor C:s₁→...→s_n→s and every i in {1,...,n}, either s_i is equivalent to s, or s_i is a basic type smaller than s."
• Definition 15 is missing. After the proof of Lemma 14, add:

  "We showed that each 〚s〛 is the least fixpoint of the monotone functional F_s. This least fixpoint can be reached by transfinite iteration. Let F_s^a be the a-th iterate of F_s over the empty set. Note that we need to go further than ω as it is shown by the following example. Consider the function i:nat→ord defined in Section 2.1.3. For all n, i(n) ∈ F_ordⁿ⁺¹-F_ordⁿ. Thus, lim(λx.i(x)) ∈ F_ord^ω+1-F_ord^ω.

  This provides us with a well-founded ordering on the computable terms of type s:

  Definition 15 (Ordering on the arguments of a function symbol) The order of a term t ∈ 〚s〛 is the smallest ordinal a such that t ∈ F_s^a. We say that t ∈ 〚s〛 is greater than u ∈ 〚s〛, t > u, if:

  • either s ∈ I and the order of t is greater than the order of u,
  • or s = s 1 → s 2 and t → ∪ ▷ u.

  This is this ordering which allows us to treat the definitions on strictly positive types. This idea is already used by Mendler for proving the strong normalization of System F with recursors for positive inductive types [36] and by Werner for proving the strong normalization of the Calculus of Inductive Constructions with recursors for strictly positive types [51]. We apply this technique to a larger class of higher-order rewrite rules.

  Let us see the example of the addition on Brouwer’s ordinals. If lim(f) is computable then, by definition of 〚ord〛, f is computable. This means that, for any n ∈ 〚nat〛, (f n) is computable. Therefore, lim(f) > (f n)."