Strict Positivity

Strict positivity is a property of recursive types that there are no self-references in its constructors' parameters' contravariant positions. For instance, if type T has a constructor of type (T \to A) \to T for arbitrary A, 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 T that is not strictly positive will have the following constructor:

tt : (T \to T) \to T

Then, with the following functions:

g: T\to T\to T\\
g~(tt~f)~x=f~x\\~\\
w=tt~(\lambda x.~g~x~x)

We can obtain a term g~w~w, which, if we unfold the definition of g we get (\lambda x.~g~x~x)~w, and by \beta reduction we get g~w~w back again. This term has non-terminating reduction, which breaks the normalization property.

See also

• Inductive types
• W-types
• Induction-recursion
• Induction-induction

References

@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",
}