Intuition Behind Strict Positivity?

Question

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?

Answer 1

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.

Answer 2

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.