Coq lets you define an inductive type of the following form:
Inductive Foo :=
| Base : Foo
| Positive : (nat -> Foo) -> Foo.
because the position of Foo
in the premise of the Positive
constructor is considered by Coq to be a positive position.
Coq rejects an inductive definition where the type being defined appears in a negative position in a premise. Accepting such a definition would enable the construction of non-normalizing terms. In particular, it is not possible to create an induction principle for such a definition.
For example:
Inductive SnaFoo :=
| Negative : (SnaFoo -> nat) -> SnaFoo.
is rejected with the error message:
Error: Non strictly positive occurrence of "SnaFoo" in "((SnaFoo -> nat) -> nat) -> SnaFoo".
But Coq also rejects the following definition:
Inductive Bar :=
| IsItPositive : ((Bar -> nat) -> nat) -> Bar.
The position of Bar
in the premise of the IsItPositive
constructor is not obviously positive but I have seen a presentation (sorry, I can no longer find the link) that accepted this position as positive. I could formulate a plausible inductive principle for Bar
as follows:
Definition Bar_ind (P : Bar -> Prop) :=
(forall (F : (Bar -> nat) -> nat),
(forall f g, (forall (b : Bar), P b -> f b = g b) -> F f = F g)
-> P (IsItPositive F))
-> forall (b : Bar), P b.
More importantly, assuming the existence of enough inaccessible cardinals, I think I can prove that there is a model of Coq's type theory that contains inductive types like Bar
, with the inductive principle that I proposed. I did prove that the presence of $\omega^2$ inaccessibles is enough to accommodate Bar
itself, assuming that all the other inductive types in the model conform to Coq's positivity rules. I don't know how many inaccessibles will be required to relax the positivity assumptions of Coq in general.
My question is twofold:
First, what is the reason that Coq does not admit definitions like Bar
?
Second, what is a good reference for the topic of admissibility of inductive types?
Bar
using inaccessibles? As soon asBar
has more than one element, the cardinality of $(B \to \mathbb{N}) \to mathbb{N}$ will exceed that of $B$. $\endgroup$