[Agda-dev] Termination

[Hans Peter Würmli]

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda-dev/attachments/20141211/87d28521/attachment.html