<p>It sounds like you want an overview of normalization arguments for type systems with positive datatypes. I'd recommend Nax Mendler's PhD dissertation: <a href="http://www.nuprl.org/documents/Mendler/InductiveDefinition.html" rel="noreferrer">http://www.nuprl.org/documents/Mendler/InductiveDefinition.html</a>.</p>

<p>As the date suggests, this is pretty classic work. The basic intuition is that an ordinal <span class="math-container">$\lambda$</span> can be associated to any element of a positive inductive type, e.g. for the data type</p>

<p><code>Inductive Ord = Zero : Ord | Suc : Ord -&gt; Ord | Lim : (Nat -&gt; Ord) -&gt; Ord</code></p>

<p>We would get:</p>

<p><span class="math-container">$$ \lambda(t) = 0$$</span>
if <span class="math-container">$t$</span> is a normal form which is not a constructor
<span class="math-container">$$ \lambda(\mathrm{Zero}) = 0$$</span>
<span class="math-container">$$ \lambda(\mathrm{Suc}(o)) = \lambda(o)+1$$</span>
and
<span class="math-container">$$ \lambda(\mathrm{Lim}(f)) = \sup_n \lambda(f\ n)$$</span></p>

<p>where <span class="math-container">$n$</span> ranges over terms with normal forms. The caveat is that this interpretation is only defined in the 3rd case when <span class="math-container">$f\ n$</span> has a normal form as well, which requires some care in the definitions.</p>

<p>One can then define recursive functions by induction over this ordinal.</p>

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

CC BY-SA 4.0
2019-04-02T16:24:11.370Z
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?
Joey Eremondi
CC BY-SA 4.0
2019-04-02T20:16:24.843Z
@jmite, you can, but ordinals in constructive theories are a bit strange, and you might as well work with well-founded orders or trees (*a la* W-type as molikto suggests). It might be hard to have a single uniform type which captures well-foundedness of *every* inductive in the object language though...
cody
CC BY-SA 4.0
2019-04-03T06:26:22.460Z
@cody Isn't the example Ord that you give a strictly positive type?
Henning Basold
CC BY-SA 4.0
2019-04-03T11:51:04.323Z
@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.
cody
CC BY-SA 4.0
2019-04-03T11:53:32.177Z
@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!
cody
CC BY-SA 4.0
2019-04-06T09:57:26.320Z
@cody Indeed, the question was mainly about strict positivity and somehow my brain filtered out only the last two questions!
Henning Basold
CC BY-SA 4.0
2019-04-06T10:16:03.673Z
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](https://www.ams.org/journals/tran/1961-100-02/S0002-9947-1961-0151396-X/S0002-9947-1961-0151396-X.pdf)
Henning Basold
CC BY-SA 4.0
2019-04-02T12:52:52.157Z
2019-04-02T12:52:52.157Z
cody
<p>Another good source for going beyond strictly positive types is the PhD thesis of Ralph Matthes: <a href="http://d-nb.info/956895891" rel="noreferrer">http://d-nb.info/956895891</a></p>

<p>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.</p>

<ol>
<li><p>We can add least fixed points for <em>any</em> type <span class="math-container">$\rho$</span> with free variable <span class="math-container">$\alpha$</span> , as long as we can provide a monotonicity witness <span class="math-container">$\forall \alpha \forall \beta.\, (\alpha \to \beta) \to \rho \to \rho[\beta/\alpha]$</span>. 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.</p></li>
<li><p>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.</p></li>
<li><p>Matthes also provides some examples of positive inductive types. Particularly interesting are</p>

<ul>
<li>the type of continuations <span class="math-container">$\mu.\, 1 + ((\alpha \to \rho) \to \rho)$</span>, where <span class="math-container">$\alpha$</span> does not occur in <span class="math-container">$\rho$</span>.</li>
<li>the type <span class="math-container">$\mu \alpha \forall \beta.\, (\alpha \to \beta) \to \rho[\beta/\alpha]$</span> that works for <em>any</em> type <span class="math-container">$\rho$</span> by turning it into a positive type. Note that this uses System F's impredicativity very heavily.</li>
</ul></li>
</ol>

<p>Matthes also uses positive inductive types to analyse double negation, for example, in this paper: <a href="https://www.irit.fr/~Ralph.Matthes/papers/MatthesStabilization.pdf" rel="noreferrer">https://www.irit.fr/~Ralph.Matthes/papers/MatthesStabilization.pdf</a>. He introduces an extension of Parigot's <span class="math-container">$\lambda\mu$</span> and proves strong normalisation.</p>

<p>I hope that this helps with your question.</p>

CC BY-SA 4.0
2019-04-03T06:55:27.073Z
2019-04-03T06:55:27.073Z
Henning Basold
<p>I'm wondering if someone can give me the intuition behind why strict positivity of inductive data types guarantees strong normalization.</p>

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

<p><code>data X where Intro : (X-&gt;X) -&gt; X</code></p>

<p>we can write a divergent function.</p>

<p>But I'm wondering, how can we prove that strictly positive inductive types <em>don't</em> 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?</p>

CC BY-SA 4.0
2019-04-02T01:08:17.437Z
I think the idea is strictly positive types can convert to W types, conceptually. Also non-strict-positive type is inconsistent with Coq http://vilhelms.github.io/posts/why-must-inductive-types-be-strictly-positive/ . It is commented that positive type is consistent with Agda, but I'd like to see a conceptual explanation also...
molikto
CC BY-SA 4.0
2019-04-02T03:19:57.427Z
@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?
Joey Eremondi
<reference-request><pl.programming-languages><type-theory><type-systems><dependent-type>
Intuition Behind Strict Positivity?
Joey Eremondi
# Intuition Behind Strict Positivity?

(Asked by: username_0 on 2019-04-02)

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?

**Tags:** reference-request, pl.programming-languages, type-theory, type-systems, dependent-type
> **Comments:**
> **username_1**: I think the idea is strictly positive types can convert to W types, conceptually. Also non-strict-positive type is inconsistent with Coq http://vilhelms.github.io/posts/why-must-inductive-types-be-strictly-positive/ . It is commented that positive type is consistent with Agda, but I'd like to see a conceptual explanation also...  
> **username_0**: @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?  

---

## 2 answers

### Answer by username_2 on 2019-04-02. Score: 9 | Accepted answer

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.

> **Comments:**
> **username_0**: 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?  
> **username_2**: @jmite, you can, but ordinals in constructive theories are a bit strange, and you might as well work with well-founded orders or trees (*a la* W-type as molikto suggests). It might be hard to have a single uniform type which captures well-foundedness of *every* inductive in the object language though...  
> **username_3**: @cody Isn't the example Ord that you give a strictly positive type?  
> **username_2**: @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.  
> **username_2**: @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!  
> **username_3**: @cody Indeed, the question was mainly about strict positivity and somehow my brain filtered out only the last two questions!  
> **username_3**: 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](https://www.ams.org/journals/tran/1961-100-02/S0002-9947-1961-0151396-X/S0002-9947-1961-0151396-X.pdf)  

---

### Answer by username_3 on 2019-04-03. Score: 6

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.


---

