[Agda] Size change of higher order arguments

[Nils Anders Danielsson]

2008/4/24 Shin-Cheng Mu <scm at iis.sinica.edu.tw>:
>
>  The definition passes the termination check, as I had wished.
>  However, I am curious why. In the recursive call:
>
>    acc-fold _<_ Φ y (h y y<z)
>
>  the third argument "h y y<z" does not seem structurally
>  "smaller" than "acc h", in the same way "n" is smaller than
>  "suc n", for example.

This is primitive recursion for higher-order types. If you are
defining f (c g), for some constructor c and function g, then f (g e)
is allowed on the right-hand side for any expression e (assuming that
the code is well-typed, of course). In other words:

  ∀ e. g e < c g

>  I had an impression that Agda uses a kind of size-change termination.

I believe this is currently the case, but I don't know the details.

The current termination checker should be strictly stronger than the
previous one, which I found quite easy to understand (perhaps because
I implemented it). The previous one was based on lexicographic
structural recursion, following Andreas Abel and Thorsten Altenkirch's
paper "A Predicative Analysis of Structural Recursion" (JFP 2002).

I think you can get a long way just by understanding lexicographic
structural recursion. With size-change termination you can define more
functions, for instance argument-swapping addition:

  _+_ : ℕ -> ℕ -> ℕ
  zero  + n = n
  suc m + n = suc (n + m)

However, I cannot remember having defined a non-toy function which was
accepted by size-change termination and not the previous termination
checker.

>  How is size-change of higher order arguments defined?
>  Is the termination checker of Agda documented somewhere?

I don't know too much about the current implementation. Andreas Abel
should be able to answer your questions.

-- 
/NAD