Strict positivity is a property of recursive types that there are no self-references in its constructors' parameters' contravariant positions. For instance, if type has a constructor of type for arbitrary , then it is not strictly positive.
Strictly positive inductive types, that are also called well-founded inductive types, are isomorphic to specializations of the W-type.
As an example, a simple inductive type that is not strictly positive will have the following constructor:
Then, with the following functions:
We can obtain a term , which, if we unfold the definition of we get , and by reduction we get back again. This term has non-terminating reduction, which breaks the normalization property.
Michael Abbott, Thorsten Altenkirch, and Neil Ghani. "Containers: Constructing strictly positive types". Theoretical Computer Science 342, no.1 (2005): 3 - 27.
@article{ABBOTT20053,
title = "Containers: Constructing strictly positive types",
journal = "Theoretical Computer Science",
volume = "342",
number = "1",
pages = "3 - 27",
year = "2005",
note = "Applied Semantics: Selected Topics",
issn = "0304-3975",
doi = "https://doi.org/10.1016/j.tcs.2005.06.002",
url = "http://www.sciencedirect.com/science/article/pii/S0304397505003373",
author = "Michael Abbott and Thorsten Altenkirch and Neil Ghani",
keywords = "Type theory, Category theory, Container functors, W-Types, Induction, Coinduction, Initial algebras, Final coalgebras",
}