[Agda] Size change of higher order arguments

[Conor McBride]

Morning all

Just my two cents...

On 24 Apr 2008, at 02:10, 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

This makes some sort of sense if you see a function
as a generalized tuple, with application as projection.

>
>>  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.

I'm guessing that David Wahlstedt's thesis is a good place to
look.

[..]

> 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.

examples/OTT/ObsEq.agda contains a (non-zero) number of
non-toy functions accepted by size-change termination
but not under the previous regime. Equality of Pi-types
is defined to behave like this (notation informal):

   Pi S0 T0 <-> Pi S1 T1  =
     S1 <-> S0  /\
     all (x1 : S1)(x0 : S0) .
       (x1 == x0) => T0 x0 <-> T1 x1

So that's swapping in the contravariant domain position,
and higher-order in the covariant range position. The
swapping helps us define the induced map from Pi S0 T0
to Pi S1 T1, which necessarily works by transporting
inputs from S1 to S0, applying the function, then
transporting the outputs back.

Contravariance is one phenomenon which promotes swapping.
Swapping also shows up in some implementations of merge.

>
>>  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.

I'd climb on my high horse at this point, but I'd fall off.
Perhaps I might just express the wish to see size-change
explained within type theory as a derived recursion
principle. Martin Hofmann and I once speculated that
size-change arguments boil down to lexicographic recursions
on *bags* of values, where bag A is strictly smaller than
bag B if every element of A is strictly smaller than some
element of B. Is anything else going on?

I begin to wonder if one might formulate some suitably
heterogeneous notions of "smaller", and of "commensurate"
(which respects "smaller" appropriately). One might use
these to say that map is size-preserving, and that filter
is non-size-increasing, for example.

I'm not opposed to termination checkers, but I'm
uncomfortable with their current syntactic basis and
oracular status. Who isn't? I'd love to see the
termination checker augmented with the corresponding
proof synthesis process, if only we knew what it was.

All the best

Conor