RFC: termination_by syntax: less wiggle-room with variables

[nomeata]

Status quo

Currently (assuming #2921), the termination_by syntax expect a list, possibly empty, of identifiers (or _), then =>, and then the body.

The semantics is that the names in the list override any variable names from the back. Examples:

def foo (n : Nat) : Nat := foo (n-1)
termination_by n => n

works but equivalently

def foo (n : Nat) : Nat := foo (n-1)
termination_by => n

or

def foo (n : Nat) : Nat := foo (n-1)
termination_by m => m

This is a bit silly: Why would the user not want to use the variable name given in the header? Is there ever a compelling reason?

Of course, the list of variables do have their justification: When the function arguments are not in the header, but bound by a lambda or by match equations:

def foo : Nat → Nat := fun n => foo (n-1)
termination_by n => n

or

def foo : Nat → Nat
 | 0 => 0
 | n => foo (n-1)
termination_by n => n

If there are variables both in the header and in the lambda/matches, the list is applied from the right:

def foo (a b : Nat) : Nat → Nat → Nat
 | 0, 0 => 0
 | c, d => foo (a-1) (b - 1) (c - 1) (d-1)
termination_by _ x y z => x -- termination goal: b - 1 < b

and you can wildly mix overriding variable names and referring to the original name using _:

termination_by x _  _ y => x + b + y -- termination goal: (a - 1) + (b - 1) + (d - 1) < a + b + d

Oddities

This works, and knowing the implementation it’s not surprised it behaves like this, but it is a bit odd:

• When no variable needs to be introduced, the arrow in termination_by => n looks odd.
• The right-to-left rule is probably not intuitive.
• Usually it is easy to predict how many parameters “after the :” lean considers, but maybe not always.
• I find hard to justify why the user even can change a to x here.

Proposed change

I wonder if our users are not better served with a more rigid syntax:

• The number of variables mentioned must match the number of “unnamed” variables (lambda after the := or discriminants in matches equations). No fewer and not more.
• If there are no such variables, the => must be omitted.

So above the valid variants would be:

def foo (n : Nat) : Nat := foo (n-1)
termination_by n

def foo : Nat → Nat := fun n => foo (n-1)
termination_by n => n

def foo : Nat → Nat
 | 0 => 0
 | n => foo (n-1)
termination_by n => n

def foo (a b : Nat) : Nat → Nat → Nat
 | 0, 0 => 0
 | c, d => foo (a-1) (b - 1) (c - 1) (d-1)
termination_by _ y => a + b + y -- termination goal: (a - 1) + (b - 1) + (d - 1) < a + b + d

If the system requires the user to get the number of variables right, the effect will more likely match the user’s intention than the more liberal “override from left to right”.

Impact

As we are changing the syntax anyways in #3040, the pain of having to touch this code would be mostly alleviated.

The implementation would probably have to carry around a bit of extra book keeping to remember which variables were originally bound before the : and which were afterwards. (This is maybe the reason it’s not already like this). But maybe worth for the extra guard rails.

Maybe there is an good compelling reason to allow users to rename variables? I don't see one yet.

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

[Kha]

• When no variable needs to be introduced, the arrow in termination_by => n looks odd.
• The right-to-left rule is probably not intuitive.

Not necessarily contradicting you here but note that this is the same behavior as case and similar tactics.

[nomeata]

Yeah, I'm somewhat on the fence over this change overall.

Also, omitting the => when the list of variables is empty means the parser has to backtrack/look ahead, not sure how desirable that is

[kim-em]

Another alternative for "less wiggle room" would be to require naming all the variables!

I think more important than the actual requirement is what the error messages are when it is not fulfilled.

[nomeata]

Yes, that's a possible alternative. I think “all variables” can be confusing, though, or at least counter intuitive, as it would involve variable variables, or variables closed over by lifting out a letrec. Also unnecessary verbose.

(The last bit makes me wonder what happens if only the termination_by clause in a local letrec mentions a parameter of the enclosing function, if that gets correctly added to the lifted function's parameters. Probably not, and probably not a relevant corner case, but I should at least open an issue and create a test.)

[nomeata]

I started to implement that on top of #3040 in #3099 now in #3040.

The change I have to make to user code “feel right”, changes like

@@ -468,7 +468,7 @@ theorem State.join_le_left (σ₁ σ₂ : State) : σ₁.join σ₂ ≼ σ₁ :=
       next => apply cons_le_cons; apply le_trans ih (erase_le _)
       next => apply le_trans ih (erase_le_cons (le_refl _))
     next h => apply le_trans ih (erase_le_cons (le_refl _))
-termination_by σ₁ _ => σ₁.length
+termination_by σ₁.length

So worth persuing.

I am hitting a slight snag in the interaction with GuessLex, which infers a termination order, and wants to use parameters that come before the :, but are not named (e.g. type class parameters, autoImplicit parameters, shadowed parameters). From the user we’d expect to name them before using them, but we can't do that in GuessLex.

At least currently, GuessLex goes through the same interface at the user. The new check is applied before, so only applies to user-written code, but it still means we can’t have all of these:

• GuessLex finds termination orders that use implicit parameters.
• The termination argument found (and printed on demand) by GuessLex adheres to the syntax requirements we have for users, and can thus pasted directly.

A pragmatic way forward may be to suggest termination_by clauses that may not work right away, but may require the user to first name/rename some parameters, or trim the list of variables. I’ll see what I can do.

Ah, or I can pass them on with the full array to rename everything to the next stage, but print it with the trimmed list of variables. This should be pretty and working in most cases, and be hopefully only mildly annoying in other cases.

[nomeata]

Done as per #3040