Stream: Coq devs & plugin devs

Topic: the definition of structurally smaller


view this post on Zulip Lapinot (May 10 2023 at 15:41):

Hi coq devs! In presence of impredicativity, the "structurally smaller" rule for acceptable inductive calls become tricky. See for example agda issue https://github.com/agda/agda/issues/3883 where termination checker sees x as a syntactic subterm of b x and thus decides x Bad bad is "structurally smaller" than b x. Coq rightfully rejects this definition, what's the magic? Is there any pointer to something describing this case of termination checking?

view this post on Zulip Lapinot (May 10 2023 at 15:45):

We had in mind marking some arguments of constructors as "recursive positions" and restricting the syntactic check to these. But there is trouble with "nested" or layered definitions.

view this post on Zulip Lapinot (May 10 2023 at 15:49):

We just found https://coq.inria.fr/files/adt-2fev10-barras.pdf . So there is no escaping constructing a "deep" annotation of recursive positions?

view this post on Zulip Guillaume Melquiond (May 10 2023 at 16:23):

I am not sure what you mean with "deep". The argument of the constructor b does not syntactically have type Bad, so it does not qualify as a subterm. There is no advanced analysis at work here, as far as Coq is concerned.

view this post on Zulip Lapinot (May 10 2023 at 19:30):

By deep i mean that in the following definition, l does not qualify as a subterm of ListCon l, but xs qualifies as a subterm of the deep pattern ListCon (Right (x , xs)). So the analysis of which places qualify as subterms doesn't take place on patterns but on deep patterns.

Variant sum (A B : Type) : Type :=
| Left (a : A) : sum A B
| Right (b : B) : sum A B
.
Inductive list (A : Type) : Type :=
| ListCon (l : sum A (A * list A) : list A

In the linked slides, it is hinted that there is a definition-time analysis of Inductive constructions which marks which of the variables of these deep patterns are valid subterms. Is this right? Slide 7 hints at an analysis on deep patterns.

Your answer seem to hint more to an other idea we had, which would be a usage-time criterion (at the time of checking validity of a recursive definition). This criterion is harder to put simply and seems less principled, but amount to: in a pattern branch, if i'm trying to call myself recursively on an argument who's head of the spine is a variable x bound as an argument of some (possibly deep) pattern, the rightmost element of the telescope of its type has to be convertible (before application of the telescope to arguments) to the type we are doing induction on.

On top of this being already hard to state, there are question marks in the case of inductive families (most likely we want the type parameters to match also, but the family indices could be different), and it seems like we would miss some valid definitions in case of mutual induction. So I'd be happier with the definition-time analysis of which variables of deep patterns are considered subterms.

view this post on Zulip Gaëtan Gilbert (May 10 2023 at 20:00):

I can confirm that this list gets a mind_recargs of

  Rec{(Mrec[foo.list, 0],
        (Norec,
          Rec{(Nested[foo.sum, 0], (Norec, (Norec)),
                (Norec,
                  Rec{(Nested[Coq.Init.Datatypes.prod, 0],
                        (Norec, (Norec), #2,0))}))}))}

I don't really understand this type but it certainly looks like an analysis of the nested structure

view this post on Zulip Guillaume Melquiond (May 11 2023 at 07:58):

To be clear, I was not hinting at all at a usage-time criterion. The fact that the argument of the constructor b is syntactically non-recursive is a definition-time criterion.

view this post on Zulip Lapinot (May 12 2023 at 12:07):

Thanks to you two for the answers! We are in the process of understanding the use of regular trees and their construction. @Gaëtan Gilbert is there a debug flag to get the content of mind_recargs for a given def? (or a file) Thanks again!

view this post on Zulip Gaëtan Gilbert (May 12 2023 at 12:41):

I don't think so, I used ocamldebug, the Drop functionality may also be useful

view this post on Zulip Lapinot (May 12 2023 at 13:06):

Thanks, i will try with Drop.

view this post on Zulip Matthieu Sozeau (May 27 2023 at 05:15):

@Lapinot indeed the regular trees handle nested inductive occurrences and one has to find syntactic occurrences of the (possibly mutual) inductive type in the constructor’s types under an of instantiation of the regular tree for the nested inductive type with the parameters used in the toplevel definition. At least that’s how I understand it. You can see that it’s an inductive definition-time analysis as it is not possible to write useful recursive defs on list rose for example.


Last updated: Jun 14 2024 at 18:01 UTC