3

I have an inductive definition which—after evaluating—prints the warning "Ignoring recursive call". It seems that the definition works perfectly fine. However, I am still curious why exactly this warning is given. Below is a minimal example.

Inductive testor :=
| Constr1 : list testor -> testor
| Constr2 : testor -> testor.

I think the culprit is list testor in the first constructor. On the other hand, the warning is not given without the second constructor.

Q: Why is the warning emitted? Does it mean a restriction is imposed on the inductive definition?

I am using Coq 8.5.

Improve this question
3
  • A side question: Why doesn't this have to be declared as Coinductive type?
    – Cryptostasis
    Commented Jun 3, 2016 at 5:17
  • @Cryptostasis I derived this example from a definition of a small programming language. I have never worked with coinductive types, but from what I understand, those are used when dealing with infinite objects. Usually, programs are finite. What is the advantage of declaring such definition as coinductive?
    – Garogolun
    Commented Jun 6, 2016 at 11:32
  • That was a wrong assumption. I thought testor would be a non terminating type. Now I see that testor is indeed terminating as Constr1 nil
    – Cryptostasis
    Commented Jun 6, 2016 at 12:57

1 Answer 1

Reset to default
4

The type testor is called a nested inductive type because of the occurrence of list testor. There is no restriction, you can safely use the definition, it's just the autogenerated induction principle is not very useful. This Coq-club thread deals with this issue. Here is an excerpt from Adam Chlipala's answer:

The warning is just about the heuristic attempts to generate a useful induction principle. Nested inductive types (like your [AllList] use here) call for some cleverness to build the right inductive case schemas.

For more details, see the "Nested Inductive Types" section in this chapter of CPDT.

Improve this answer

Not the answer you're looking for? Browse other questions tagged or ask your own question.