RFC: termination_by structurally x

[nomeata]

Proposal

Right now if the user writes a recursive function without annotation, Lean tries

• structural recursion on each argument
• well-founded recursion with GuessLex

If the user wants to be explicit about well-founded recursion, they can use termination_by x. But they have no way of indicating that they want to use structural recursion on a specific argument.

Right now the above search procedure is not slow, so the need isn’t high, but once we have structural recursion on mutually recursive functions, the first step might consider many combinations, and it would be good if the user can just declare their intent.

Furthermore, if the user can be specific, they get a less noisy error message when the derecursifying fails.

Initial proposal for the syntax is

termination_by structurally x      -- if x is bound before the colon
termination_by structurally x => x -- if x is bound after the colon

in analogy to the existing termination_by. This way, no new “definition trailing keyword” is introduced.

It can also be extended to more variants in the future, such as termination_by tail-recursion (which isn’t really “termination”, sigh.)

Once we have this, then termination_by? should not force well-founded recursion and should, if lean detects structural recursion, suggest the corresponding termination_by structurally … annotation.

Community Feedback

(none yet)

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.

[nomeata]

I am happy to hear alternative syntax ideas; the termination_by structurally x suggested above is somewhat clunky.

[digama0]

I think it should be styled closer to options in tactic syntax, e.g. termination_by (method := structural). This also gives a bit more freedom to tweak the syntax without clashing with either the expr or ident parser.

[b-mehta]

I can't comment on the implementation here, but the proposal is something I would absolutely find valuable. Can we, however, make sure that the expected behaviour is documented somewhere?

[nomeata]

Yes, of course! I hope that by the end of the year there will be an amazing reference manual that’s a joy to keep updated as I add features. Until then we are a bit in a limbo. But that’s for the reminder to at least keep the docstring on termination_by up-to-date (docstring extended in c3398e3).