Termination checker with high order functions

Stream: new members

[MrQubo]

Is it possible to prove termination when the recursive function is passed as an argument to high order function, by directly unfolding the high order function definition?

Example:

def foo (a : α -> β) b  := a b

def bar : Nat → Nat
  | 0 => 0
  | Nat.succ x => foo bar x
termination_by x => x
decreasing_by
  simp_wf
  admit

It seems what I wanted to do is impossible, the goal doesn't mention foo at all. It wants me to prove that the recursive call to bar with any argument is decreasing.

[Aaron Liu]

Well founded recursion abstracts occurrences of bar a to pass to docs#WellFounded.fix. So when you write foo bar x, bar gets eta-expanded into fun a => bar a so that bar a can be abstracted, and then you have to prove that this recursive call to a is decreasing, which is obviously impossible since a is now a new free variable.

[MrQubo]

Yes, I think I understand what happened.
I'm asking whether it's somehow possible to prove that function bar is in fact terminating.

[Aaron Liu]

Usually, the solution would be to modify foo to pass in some more arguments to bar, and then maybe these additional assumptions are enough to prove the recursive call is decreasing.

[Aaron Liu]

To do this without modifying foo is trickier. Since the elaborator needs to abstract out bar a, you need a way to unfold foo, which may not always be possible (what if instead of foo, you had a free variable?).