[Agda-dev] Termination

[Andreas Abel]

Yes, the termination analysis is cheap in that respect, it does not see 
that the call sequence

   stop (I :: n) --> stop (I :: n)

is impossible.  Someone (was it Jean-Yves Moyen?) suggested a smarter 
static call graph construction, e.g. from

1. stop I = 1
2. stop (O ∷ n) = stop n
3. stop (I ∷ n) = 1 + stop (O ∷ n)

construct the graph

2: stop (O :: n) --> stop n
3: stop (I :: n) --> stop (O :: n)

and observe that 3 has to be followed by 2, so we get only the static 
call graph

  stop2 --(<)--> stop2
  stop2 --(<)--> stop3
  stop3 --(=)--> stop2

which we complete by adding another call

  stop3 --(<)--> stop3

Now all loops are decreasing (<), and the function passes.

Such an analysis would be much more expensive, I guess.  The question is 
whether it is worth the effort.  As you observe, you can easily rewrite 
your program.  Often a simpler recursion pattern also helps when you 
want to prove properties of your function.  I guess I'd need to see more 
convincing examples, that not just contain functions that could benefit 
from a smarter termination check, but also proofs about these functions 
(that possibly also benefit from a smarter termination check).

Cheers,
Andreas


On 11.12.2014 05:47, Hans Peter Würmli wrote:
>
> The following simple program terminates, but the termination checker
> does not pass it:
>
> --------------------------------------------------
>
> module Termination where
>
> open import Data.Nat
>
> data Bit : Set where
>    O : Bit
>    I : Bit
>
> infixr 5 _∷_
>
> data bℕ : Set where
>    I : bℕ
>    _∷_ : Bit → bℕ → bℕ
>
> {-# NO_TERMINATION_CHECK #-}
> stop : (n : bℕ) → ℕ
> stop I = 1
> stop (O ∷ n) = stop n
> stop (I ∷ n) = 1 + stop (O ∷ n)
> -- stop (I ∷ n) = 1 + stop (n)      -- this would pass the termination
> checker
>
> open import Data.Nat.Show as NShow
> open import Data.String
> open import Data.Unit using (⊤)
> open import IO.Primitive
> open import IO
>
> main : IO.Primitive.IO ⊤
> main = run (IO.putStrLn (NShow.show (stop (I ∷ O ∷ I))))
>
> ---------------------------------------------
>
> It looks like the termination checker expects a lower height in each
> recursive step instead of checking other cases first.
>
> Cheers,
>
> Hans Peter
>
>
> _______________________________________________
> Agda-dev mailing list
> Agda-dev at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda-dev
>

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/