I'm wondering if someone can give me the intuition behind why strict positivity of inductive data types guarantees strong normalization.

To be clear, I see how having negative occurrences leads to divergence, i.e. by defining:

data X where Intro : (X->X) -> X

we can write a divergent function.

But I'm wondering, how can we prove that strictly positive inductive types don't allow for divergence? i.e. is there some induction measure that lets us construct a proof of strong-normalization (using logical relations or similar)? And where does such a proof break down for negative occurrences? Are there any good references that show strong normalization for a language with inductive types?

  • $\begingroup$ I think the idea is strictly positive types can convert to W types, conceptually. Also non-strict-positive type is inconsistent with Coq vilhelms.github.io/posts/… . It is commented that positive type is consistent with Agda, but I'd like to see a conceptual explanation also... $\endgroup$ – molikto Apr 2 '19 at 1:08
  • $\begingroup$ @molikto Thanks, that's helpful. But I thought that W-types didn't give the desired induction principles in an intensional theory? How can we prove strong normalization for strictly-positive inductives in an intensional theory? $\endgroup$ – jmite Apr 2 '19 at 3:19

It sounds like you want an overview of normalization arguments for type systems with positive datatypes. I'd recommend Nax Mendler's PhD dissertation: http://www.nuprl.org/documents/Mendler/InductiveDefinition.html.

As the date suggests, this is pretty classic work. The basic intuition is that an ordinal $\lambda$ can be associated to any element of a positive inductive type, e.g. for the data type

Inductive Ord = Zero : Ord | Suc : Ord -> Ord | Lim : (Nat -> Ord) -> Ord

We would get:

$$ \lambda(t) = 0$$ if $t$ is a normal form which is not a constructor $$ \lambda(\mathrm{Zero}) = 0$$ $$ \lambda(\mathrm{Suc}(o)) = \lambda(o)+1$$ and $$ \lambda(\mathrm{Lim}(f)) = \sup_n \lambda(f\ n)$$

where $n$ ranges over terms with normal forms. The caveat is that this interpretation is only defined in the 3rd case when $f\ n$ has a normal form as well, which requires some care in the definitions.

One can then define recursive functions by induction over this ordinal.

Note that these data types can be defined already in classical set theory, as indicated in the excellent Inductive Families paper by Dybjer (http://www.cse.chalmers.se/~peterd/papers/Inductive_Families.pdf). However, because the function spaces are so huge, types like Ord require really large ordinals to interpret.

| cite | improve this answer | |
  • $\begingroup$ Thanks, this is very helpful! Do you know if such ordinals can be defined in type theory itself? i.e. if I was trying to use Agda to with induction-recursion to model a type theory with inductives (but no induction-recursion), could I use something like Ord to model the ordinals needed for showing well-foundedness? $\endgroup$ – jmite Apr 2 '19 at 16:24
  • 1
    $\begingroup$ @cody Isn't the example Ord that you give a strictly positive type? $\endgroup$ – Henning Basold Apr 3 '19 at 6:26
  • 1
    $\begingroup$ @HenningBasold yes it is (that's why I used it as illustration!). But it doesn't behave exactly like ordinals in a (classical) set theory, and certainly not like the set of all ordinals. In particular, it's a bit hard to define an order on these. $\endgroup$ – cody Apr 3 '19 at 11:51
  • 1
    $\begingroup$ @HenningBasold also I should note that jmite's question was about strictly positive types specifically, though information on the more general setting is interesting as well! $\endgroup$ – cody Apr 3 '19 at 11:53
  • 1
    $\begingroup$ Just for the reference of others: The definition of ordinals cody gave is indeed quite different from the classical ordinals and don't exhaust all of them (this now really a matter of what you define to be an ordinal, similar to different notions of real numbers in constructive mathematics). The type cody gave is essentially Kleene's O, which is discussed, for example, here $\endgroup$ – Henning Basold Apr 6 '19 at 10:16

Another good source for going beyond strictly positive types is the PhD thesis of Ralph Matthes: http://d-nb.info/956895891

He discusses extensions of System F with (strictly) positive types in chapter 3 and proves many strong normalisation results in chapter 9. There are a few interesting ideas discussed in chapter 3.

  1. We can add least fixed points for any type $\rho$ with free variable $\alpha$ , as long as we can provide a monotonicity witness $\forall \alpha \forall \beta.\, (\alpha \to \beta) \to \rho \to \rho[\beta/\alpha]$. This idea is already present in Mendler's work that cody mentioned. Such witnesses exist canonically for any positive type because these are syntactically monotone.

  2. When we move from strictly positive to positive types, then the inductive types cannot be viewed as trees any longer (the W-type encoding). Instead these introduce some form of impredicativity because the construction of a positive inductive type already quantifies over the type itself. Note that this is a somewhat mild form of impredicativity, as the semantics of such types can still be explained in terms of ordinal iteration of monotone functions.

  3. Matthes also provides some examples of positive inductive types. Particularly interesting are

    • the type of continuations $\mu.\, 1 + ((\alpha \to \rho) \to \rho)$, where $\alpha$ does not occur in $\rho$.
    • the type $\mu \alpha \forall \beta.\, (\alpha \to \beta) \to \rho[\beta/\alpha]$ that works for any type $\rho$ by turning it into a positive type. Note that this uses System F's impredicativity very heavily.

Matthes also uses positive inductive types to analyse double negation, for example, in this paper: https://www.irit.fr/~Ralph.Matthes/papers/MatthesStabilization.pdf. He introduces an extension of Parigot's $\lambda\mu$ and proves strong normalisation.

I hope that this helps with your question.

| cite | improve this answer | |

Your Answer

