Stream: Coq devs & plugin devs

Topic: Fixpoints non-wellfounded in erasable subterms accepted


view this post on Zulip Hugo Herbelin (Dec 31 2021 at 15:22):

(About the current coq-club discussion)
It is known for probably more than 15 years that Coq tolerates fixpoints with non guarded recursive calls in erasable subterms. My perception is that this has been kept as it (including by me) because considered rather anecdotical (mostly for the reasons given by @Pierre-Marie Pédrot that non-standard reduction is in theory not needed).

It is a bit inelegant in practice though. Shouldn't we do something? Beside not being able to assume strong normalization of Coq, it also defeats the claim that we want a decidable type-checking algorithm as shown is this example:

Definition K (x y : Prop) := x.
Fixpoint Kloop (n : nat) := K True (Kloop n).
Opaque K.
Check fun x : K True (Kloop 0) => x : Kloop 0. (* stack overflow *)

Fortunately, the code checking guard is already combining checking well-foundedness with incremental reduction. So, it seems to me that there would be an easy fix:

What do you think?

view this post on Zulip Enrico Tassi (Dec 31 2021 at 15:41):

Invest in size types?

view this post on Zulip Hugo Herbelin (Dec 31 2021 at 15:43):

Sure, but this looks long term (are there some news from William?).

view this post on Zulip Karl Palmskog (Dec 31 2021 at 16:09):

here I was hoping that sized types would be incorporated as an alternative way of getting explicit well-foundedness proofs "for free", not necessarily built into Coq's type checker...

view this post on Zulip Karl Palmskog (Dec 31 2021 at 16:11):

with Equations and so on, should one [i.e., should general Coq users] even be using Fixpoint/fix at all?

view this post on Zulip Gaëtan Gilbert (Dec 31 2021 at 16:59):

So, it seems to me that there would be an easy fix:

worth a try if easy to implement, worst case we get to see the impact on CI

view this post on Zulip Hugo Herbelin (Jan 02 2022 at 10:26):

Karl Palmskog said:

here I was hoping that sized types would be incorporated as an alternative way of getting explicit well-foundedness proofs "for free", not necessarily built into Coq's type checker...

I don't know the plans so well. One advantage of sized types (in the kernel) is also modularity: one can build fixpoints depending on size properties of some parameters w/o having to be constrained to give explicit instances of the parameters.
Afaiu, sophisticated proofs of well-foundedness, even if it could clearly be extended (e.g. with recursion on many arguments) are somehow already supported by the {wf ...}/{measure ...} architecture.

view this post on Zulip Karl Palmskog (Jan 03 2022 at 08:50):

well, I meant that sized types could be a more automated alternative to a specific measure specification, e.g., {sized ...}

view this post on Zulip Paolo Giarrusso (Jan 04 2022 at 19:15):

They seem less automated and less flexible, and their motivating examples in Agda are all things that Coq already supports; the only advantage is properly modular typechecking, at the cost of adding sizes to your spec

view this post on Zulip Paolo Giarrusso (Jan 04 2022 at 19:21):

Hm, I see https://github.com/coq/coq/wiki/CoqTerminationDiscussion#sized discusses some differences (including inference) in Sacchini's proposal...

view this post on Zulip Karl Palmskog (Jan 04 2022 at 19:22):

Pros: logically simple (compositional), minimal work from users when it works

That's the kind of mechanism I'm interested in, but not necessarily built into the [default] type checker.

view this post on Zulip Paolo Giarrusso (Jan 04 2022 at 19:30):

So you still need a kernel mechanism, plus an elaboration for sized types. Does the latter exists?

view this post on Zulip Karl Palmskog (Jan 04 2022 at 19:31):

no idea, but why does it have to be in the kernel?

view this post on Zulip Paolo Giarrusso (Jan 04 2022 at 19:32):

I'm just saying, sized types (or anthing really) must either be in the kernel or elaborate to something in-kernel

view this post on Zulip Karl Palmskog (Jan 04 2022 at 19:34):

OK sure, it has to pass the kernel at some point

view this post on Zulip Paolo Giarrusso (Jan 04 2022 at 19:35):

And you should hide the elaboration output from users, like when elaborating to eliminators.

view this post on Zulip Paolo Giarrusso (Jan 04 2022 at 19:37):

Equations and Lean do it somewhat, but I'm not sure all source-level definitional equality remain definitional after elaboration.

view this post on Zulip Ali Caglayan (Jan 04 2022 at 20:24):

There was a recent attempt to add sized typing to coq https://github.com/coq/coq/pull/12426

view this post on Zulip Ali Caglayan (Jan 04 2022 at 20:25):

But the authors concluded that there were performance issues in their implementation https://arxiv.org/abs/1912.05601

view this post on Zulip Karl Palmskog (Jan 04 2022 at 20:28):

sure, but this attempt was all about hacking the kernel

view this post on Zulip Paolo Giarrusso (Jan 04 2022 at 20:44):

given how elegant are ordinals to formalize in type theory, I wonder if elaboration is possible at all. https://arxiv.org/pdf/1903.08233.pdf says sized types “require” extensions of the underlying type theory (tho that might be a limit of what we know already).

view this post on Zulip Karl Palmskog (Jan 04 2022 at 20:47):

how do you prove that you have to extend the type theory? Seems like difficult to do. And if it turns out that all one needs is to add an axiom, that's fine by me if I get nice automation

view this post on Zulip Paolo Giarrusso (Jan 05 2022 at 00:18):

as I already tried to say, I don’t mean “provably impossible”, just that we haven’t figured out a way to do it yet.

view this post on Zulip Karl Palmskog (Jan 05 2022 at 11:16):

or, we haven't figured out the impossibility proof yet

view this post on Zulip Matthieu Sozeau (Jan 05 2022 at 13:46):

@Hugo Herbelin I thought allowing only linear reductions would solve the issue elegantly, is it not sufficient?

view this post on Zulip Hugo Herbelin (Jan 05 2022 at 14:57):

You mean forbidding any form of K-redexes in the body of a fix?

view this post on Zulip Matthieu Sozeau (Jan 06 2022 at 13:12):

I mean not allowing to unfold a K-redex indeed, forcing the body to be guard-checked

view this post on Zulip Hugo Herbelin (Jan 09 2022 at 13:08):

Matthieu Sozeau said:

I mean not allowing to unfold a K-redex indeed, forcing the body to be guard-checked

We can try that... though I'm unsure Equations or Program don't have patterns of the form fix aux ... := let H _ := ... in H aux ... end (which could certainly be adapted though if needed).

view this post on Zulip Hugo Herbelin (Jan 09 2022 at 13:27):

In any case, whatever decision is taken, I made an experiment of strongly checking guard at #15434.

view this post on Zulip Hugo Herbelin (Jan 09 2022 at 13:28):

It revealed one case of non strongly guarded fixpoint in CI (in fiat-crypto).

view this post on Zulip Matthieu Sozeau (Jan 10 2022 at 09:26):

Right, the partial applications might be a problem with the strategy I proposed.
It's great to know that #15434 has only one legitimate failure in the wild !


Last updated: Feb 01 2023 at 16:03 UTC