6
$\begingroup$

I've been having a bit of difficulty proving termination of a particular kind of function. I'm quite new to using Lean, so it's possible that what I'm missing is a language feature and not a technique, but here goes.

To show what I mean, consider the following type of trees.

inductive Tree (α : Type u) : Type u where
  | empty : Tree α
  | node : α → List (Tree α) → Tree α

Consider then some function that traverses a tree, like this one.

def Tree.number_of_nodes : Tree α → Nat
  | .empty => 0
  | .node _ ts => List.foldl (fun a e => a + number_of_nodes e) 1 ts

The function is not accepted because termination cannot be proved automatically. "Structural recursion cannot be used."

My question then: what is the best approach to prove termination of functions like these, where it feels like the answer to the question "why does this function terminate" is "structural recursion, of course", but where that's obscured to the checker by the fact that the recursion is on a subterm of an immediate subterm, and not on the immediate subterm itself?

This comes up a lot whenever a type is given a definition where some container (a List, in this case) is used to hold values of the same type being defined. For example, if the type were that of binary trees, where the "intermediate" type were Tree α × Tree α instead of List (Tree α), the same error message would arise.

So far, I've been unable to think of a well-founded relation to give to termination_by in these cases, so I end up writing decreasing_by admit, but I'd like to stop doing that for obvious reasons.

P.S. I'm using the latest Lean 4 through the Code extension.

P.P.S. Any resources about techniques for showing termination in other cases are welcome as well, even if not Lean specific, but that's really for another question.

$\endgroup$
1

2 Answers 2

3
$\begingroup$

For reference, in Coq, termination checking “just works” on this function:

Require Import List.

Inductive tree {A : Type} : Type :=
| empty : tree
| node (x : A) (ts : list tree) : tree.
Arguments tree A : clear implicits.

Fixpoint number_of_nodes {A} (t : tree A) : nat :=
  match t with
  | empty => 0
  | node x ts => fold_left (fun a e => a + number_of_nodes e) ts 1
  end.

This is a bit mysterious, so we should work out why this works in Coq but not Lean (or Agda or Idris, for that matter). To my understanding, the crucial component is the separation between the top-level definition fold_left and the checked fixpoint operator fix which provides its recursion.

Let us look at the definition of fold_left, and also the core term this definition elaborates to. The definition looks a bit strange because of this Section business, but this actually turns out to be crucial. In the core term, we can see that fold_left is of the form fun A B (f : A -> B -> A) => fix .... The arguments A, B, and f appear outside the fix construct because, in the source program, they were bound in the Section, outside the Fixpoint declaration.

Section Fold_Left_Recursor.
  Variables (A : Type) (B : Type).
  Variable f : A -> B -> A.

  Fixpoint fold_left (l:list B) (a0:A) : A :=
    match l with
      | nil => a0
      | cons b t => fold_left t (f a0 b)
    end.

  (* ... *)

End Fold_Left_Recursor.

Arguments fold_left [A B]%type_scope f%function_scope l%list_scope a0.

Print fold_left.

(*
fold_left =
fun (A B : Type) (f : A -> B -> A) =>
fix fold_left (l : list B) (a0 : A) {struct l} : A :=
  match l with
  | nil => a0
  | b :: t => fold_left t (f a0 b)
  end
     : forall A B : Type, (A -> B -> A) -> list B -> A -> A
 *)

Back in number_of_nodes, the termination checker sees the definition as follows. I have inlined the definition of fold_left, β-reduced away arguments A, B, and f, and β-reduced away the two arguments to f. The termination checker is happy to unfold definitions and do β-reductions, because these steps on their own are not recursive, and thus do not jeopardise the termination of the termination checking algorithm itself. However, we cannot do any unfolding of the fix construct, because it would become unclear when to stop. In Lean (I'm guessing), the equivalent of the fix construct appears immediately at the top of the function definition, stopping all of these β-reductions happening.

Fixpoint number_of_nodes {A} (t : tree A) : nat :=
  match t with
  | empty => 0
  | node x ts =>
    (fix fold_left (l : list (tree A)) (a0 : A) {struct l} : A :=
      match l with
      | nil => a0
      | e :: es => fold_left es (a0 + number_of_nodes e)
      end) ts 1
  end.

The important feature is that the occurrence of number_of_nodes is now applied to its argument (e), so we can ask whether e is structurally smaller than t. This seems plausible: ts is smaller than t because it's an argument to its constructor. Then, l is structurally decreasing in the fix-construct, so it is at most as big as ts in all calls. Finally, e is smaller than l, so by transitivity, we get what we wanted.


Thanks to Andrej for suggesting I write up this answer.

$\endgroup$
5
  • $\begingroup$ Thanks for writing it up! $\endgroup$ Jul 13, 2023 at 10:56
  • 1
    $\begingroup$ I believe you're mostly missing why it works in Coq and why it doesn't in Lean. It seems the crucial aspect is what you're describing after the "important feature": that Coq's syntactic termination checker has an explicit rule for taking nested fixpoints into account (coq.inria.fr/files/adt-2fev10-barras.pdf#page=15, which features a basically identical example). This is not a rule that fits into Lean's recursor-based representation that imposes a very strict shape on the recursion and if we simulate it by rewriting the inner fix, the result will not be defeq to the original definition $\endgroup$ Jul 14, 2023 at 13:45
  • $\begingroup$ That is, I don't think there's a way for number_of_nodes (node x ts) = fold_left (fun a e => a + number_of_nodes e) ts 1 to hold definitionally in Lean $\endgroup$ Jul 14, 2023 at 13:46
  • $\begingroup$ @SebastianUllrich Thanks for the comment. Looking back at my answer, what I explained was why this works in Coq but not Agda, which is the best I could do given that I don't know Lean. If I were to add something to the effect of “Coq has fix, whereas Lean elaborates recursive definitions to eliminators. The former cannot generally be elaborated to the latter.”, would that constitute an explanation? $\endgroup$
    – James Wood
    Jul 15, 2023 at 8:47
  • $\begingroup$ @JamesWood Yes, that statement is definitely true -- at least without losing expected definitional equalities $\endgroup$ Jul 15, 2023 at 15:36
3
$\begingroup$

The part of Lean that tries to determine whether recursion is well-founded does not look inside definitions (it's dangerous to do so when one is dealing with recursive definitions). You can solve the problem by showing the definition of foldl down its throat.

inductive Tree (α : Type u) : Type u where
  | empty : Tree α
  | node : α → List (Tree α) → Tree α

def Tree.number_of_nodes : Tree α → Nat
  | .empty => 0
  | .node _ ts => foldl 1 ts
where
    foldl : Nat → List (Tree α) → Nat
      | n, [] => n
      | n, (t :: ts) => foldl (n + number_of_nodes t) ts

#eval Tree.number_of_nodes (.node 1 [.node 2 [], .node 3 [.node 5 []]])

It's not ideal, perhaps someone else knows a better way.

$\endgroup$
8
  • $\begingroup$ This would be the solution in agda --safe. Coq has a better solution, based on the fix construct. Perhaps a Lean expert could tell us whether Lean has an analogous fix – otherwise this answer should be accepted. $\endgroup$
    – James Wood
    Jul 11, 2023 at 11:10
  • $\begingroup$ What's particular about agda --safe that warrants singling it out in this situation? $\endgroup$ Jul 11, 2023 at 15:11
  • $\begingroup$ Lack of sized types. $\endgroup$
    – James Wood
    Jul 11, 2023 at 16:28
  • $\begingroup$ I am now consfused, as my answer says nothing about sized types. I think it would be most useful if you wrote your own answer and explained what you have in mind in more detail. I'd love to learn about an alternative (apart from sized types, I know about those). $\endgroup$ Jul 11, 2023 at 21:17
  • $\begingroup$ I don't know Lean, and I interpreted the question as being about Lean (I don't really know how seriously to take the “not Lean specific” remark if the solutions involve major changes to Lean's core calculus). I basically know three common solutions: inlining (your answer), Coq-style fix, and sized types. Inlining applies in all three of Lean, Agda, and Coq. fix only applies in Coq, and maybe Lean (but I don't know it). Sized types only apply in unsafe Agda (the current implementation is known to cause inconsistencies), and I'm fairly sure Lean doesn't implement sized types. $\endgroup$
    – James Wood
    Jul 12, 2023 at 9:41

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.