[Agda] Size change of higher order arguments

[Andreas Abel]

Dear Shin-Cheng,

what Nisse has answered you is all correct.  It makes sense to think of 
a whole function to be bigger than one of it's value:

    f a <= f

This is sound for predicative type theories.  The idea is by Thierry 
(Pattern matching ..., TYPES 92) and there is a formal proof of 
well-foundedness by Thorsten and me in the paper cited below (JFP 02).

The termination checker works still as described in the JFP 02 article: 
  extraction of call graphs and call matrices, completion, etc.  The 
only difference is that we now use the "size-change" termination criterion:

   For each function f of the completed call graph, consider the calls

        A
     f --> f   with *idempotent* call matrix A, i.e., A o A = A

   Then A needs to decrease in one argument, i.e., A_ii = "<" for one i.

This termination criterion is easier to check (the code to construct a 
lexicographic ordering is no longer needed).  However it is harder to 
verify, it requires the Ramsey theorem (see PhD by David Wahlstedt and 
the POPL'01 Paper by Neil Jones).

To answer the last question belo:

   "higher-order" is orthogonal to "size-change".

"higher-order" affects phase 1 of the termination checker: extraction of 
calls from the intermediate code and comparing call arguments with 
function parameters to come up with the initial call matrices. 
Comparison involves some notion of structural order which involves the 
"higher-order" principle f a <= f.

"size-change" affects phase 2: call graph completion and 
finding/checking the termination criterion.

Hope that clarifies things a bit, please get back to me if questions remain.

Cheers,
Andreas

Nils Anders Danielsson wrote:
> 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.
> 
> 
> 
> ------------------------------------------------------------------------
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda