(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:
NotEnoughArgumentsForFixCall
) but not in the other cases of failures and in particular not if it is a non-guarded recursive call.What do you think?
Invest in size types?
Sure, but this looks long term (are there some news from William?).
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...
with Equations and so on, should one [i.e., should general Coq users] even be using Fixpoint
/fix
at all?
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
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.
well, I meant that sized types could be a more automated alternative to a specific measure specification, e.g., {sized ...}
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
Hm, I see https://github.com/coq/coq/wiki/CoqTerminationDiscussion#sized discusses some differences (including inference) in Sacchini's proposal...
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.
So you still need a kernel mechanism, plus an elaboration for sized types. Does the latter exists?
no idea, but why does it have to be in the kernel?
I'm just saying, sized types (or anthing really) must either be in the kernel or elaborate to something in-kernel
OK sure, it has to pass the kernel at some point
And you should hide the elaboration output from users, like when elaborating to eliminators.
Equations and Lean do it somewhat, but I'm not sure all source-level definitional equality remain definitional after elaboration.
There was a recent attempt to add sized typing to coq https://github.com/coq/coq/pull/12426
But the authors concluded that there were performance issues in their implementation https://arxiv.org/abs/1912.05601
sure, but this attempt was all about hacking the kernel
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).
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
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.
or, we haven't figured out the impossibility proof yet
@Hugo Herbelin I thought allowing only linear reductions would solve the issue elegantly, is it not sufficient?
You mean forbidding any form of K-redexes in the body of a fix?
I mean not allowing to unfold a K-redex indeed, forcing the body to be guard-checked
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).
In any case, whatever decision is taken, I made an experiment of strongly checking guard at #15434.
It revealed one case of non strongly guarded fixpoint in CI (in fiat-crypto).
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: Nov 29 2023 at 18:01 UTC