Named global fixpoints and cofixpoints

[herbelin]

Rendered

[gares]

One detail to be analyzed is the one of termination checking. In particular it should be made more tolerant on the result of lambda lifting. For example Definition map A B (f : A -> B) := fix ... is not possible, only Fix map A B f ... is. When map is used with another fixpoint (eg the one being defined) as the argument f then one cannot simply reduce and see, as we do today, since reduction will not unfold the fixpoint (used to unfold the constant and beta reduce f) but one has to track where f is used, symbolically. Fixpoints like map are also the result of section discharging, you cannot really avoid hand them I'm afraid.
IIRC this is not super hard, but slightly different than what the code does today. Details are in http://www-sop.inria.fr/members/Enrico.Tassi/smallcc.pdf page 51. We had no proof of correctness, just intuition, but it is better than nothing ;-)

Another detail is very related to a recent PR of yours about fixpoints with no rec call. With global fixpoints one can define "hard" projections as non recursive fixpoints. It is useful because the reduction behavior is what one really expect from a projection (a bit like primproj, but without the optimization of parameters).

[herbelin]

Fixpoints like map are also the result of section discharging, you cannot really avoid hand them I'm afraid.
IIRC this is not super hard, but slightly different than what the code does today. Details are in http://www-sop.inria.fr/members/Enrico.Tassi/smallcc.pdf page 51.

We should definitely apply this to Coq.

With global fixpoints one can define "hard" projections as non recursive fixpoints.

Wouldn't it be a bit hackish? I mean: the need for triggering a delta only under some specific restrictions of normalization of the arguments is a perfectly legitimate need, as the case of projections show. But I would suggest to give to this need its full value rather than artificically declaring non-recursive functions as recursive just because only fixpoints (currently) support these restrictions.

This being said, I don't know how to proceed. Do you think it would be worth to write another CEP on each of these two points?

[gares]

I'd leave more time to others to comment, and try to give a more detailed roadmap with intermediate milestones. It seems a large change for just one PR, it may be reasonable to foresee intermediate "releasable/mergeable" status of the feature.

[Zimmi48]

I would avoid having CEPs depending on other CEPs. You can definitely have a CEP describing a long plan that should be implemented in many PRs.

[Blaisorblade]

FWIW: while this change sounds good, AFAIK Agda (not Adga) goes further, like Equations: the only reduction rules are for add (S m) n -> S (add m) n and add 0 n -> n. Anything else is neutral (including AFAIK add itself; even their analogue of the match construct is derived by lambda-lifting to the top-level). That might not be flexible enough for Coq, but in this common case reduction Just Works (tm) out of the box. But I've just used it, not investigated the relevant metatheory.

[Blaisorblade]

But to be sure — this comment probably amounts to "here's a possible research direction, which I'm not fully qualified to judge". EDIT: moreover agda chooses to make top-level names generative, which (as you say) would create additional incompatibilities.

[herbelin]

The basic question is whether you want to have a new world with a new add in parallel to the current add or if you want to extend the current add. In general, I tend to be on the side of preserving the existing with minimal changes, so that we can continue to benefit of all what has been done so far.

PS: typo fixed, thanks.

[herbelin]

After having made some experiment to implement the proposal, I arrived to the conclusion that this was a wrong direction.

A much simpler solution would just be to add an extra field to Fix/CoFix terms that tells how to "refold" the term after expansion. E.g., internally, instead of:

Fix (([|0|], 0), ([|(Name add)|], [|nat->nat->nat|], [|... body ...|])

we would have

Fix (([|0|], 0), ([|(Name add, Some Nat.add)|], [|nat->nat->nat|], [|... body ...|]

so that, at reduction time, we can expand by substituting the body not with the Fix ... itself but instead with Nat.add

Kernel-wise, to accept the extra Some Nat.add, a check would have to be made that Nat.add is indeed convertible to the Fix ... itself.

Note that the extra optional information has to be a term rather than just a constant because the general form for a constant is to be a sequence of fun over a fix/cofix (as mentioned above in the discussion). For instance, for List.map, it would be List.map A B f for the appropriate values of A, B and f.

Remark: it is unclear whether this would be enough to provide simpl-style refolding, that is a refolding that refolds not only one but virtually an arbitrary long reversible chain of nested constants, as, say, in Definition add' := Nat.add, which we would like to eventually refold to add'.

[SkySkimmer]

Kernel-wise, to accept the extra Some Nat.add, a check would have to be made that Nat.add is indeed convertible to the Fix ... itself.

but when the kernel sees the definition of Nat.add, Nat.add does not yet exist. How is that checked?

[herbelin]

Good question. For defining Nat.add, I guess we have to check it in an environment that first declares it (unchecked).

This seems similar to what happens in programming languages where we prepare a slot beforehand for the recursive definition in the environment and eventually "tie the loop".

[silene]

Perhaps, it is a bad idea to store the term in the original definition. It might be better for the kernel to just create it on the fly when unfolding a definition with a non-empty stack. For example, if the kernel decides to unfold List.map, while the stack contains A, B, and f, it ends up with a fix and can annotate it on the fly with List.map A B f. But, if the stack contains less than three elements, then information is lost and the fixpoint will not be refolded later on. This solves the issue with Nat.add, but also with add'. Also, it means that there is no need to check for actual convertibility, since it is then by construction. The downside is that two equivalent terms might now be different, depending on whether the kernel successfully annotated them or not.

[herbelin]

Perhaps, it is a bad idea to store the term in the original definition. It might be better for the kernel to just create it on the fly when unfolding a definition with a non-empty stack. For example, if the kernel decides to unfold List.map, while the stack contains A, B, and f, it ends up with a fix and can annotate it on the fly with List.map A B f. But, if the stack contains less than three elements, then information is lost and the fixpoint will not be refolded later on. This solves the issue with Nat.add, but also with add'. Also, it means that there is no need to check for actual convertibility, since it is then by construction. The downside is that two equivalent terms might now be different, depending on whether the kernel successfully annotated them or not.

I would say that what you describe is what cbn is doing (??). That's indeed an option but if one wants lazy, cbv, or even any reduction done in the system to refold named fix/cofix, it is not clear how to do it well. For instance, is it not clear to me that this would combine well with the sharing used in lazy.

[gares]

I think making the info optional is better, since qed type checking could just behave as today, while the upper layers could use this extra datum to implement refolding. Lazy could be parametrized on this. It would have the status of a pretty printing hint, lake the names on binders.