[Agda] strange termination check

[Andreas Abel]

Unfortunately, the termination-depth-trick works only for natural 
numbers and sizes, not for lists and other data structures with a 
constructor that has more than one argument.

See my previous message

   https://lists.chalmers.se/pipermail/agda/2013/005855.html

for an implementation of powerToPos that works.

On 2013-10-11 08:45, Sergei Meshveliani wrote:
> On Thu, 2013-10-10 at 21:57 +0400, Sergei Meshveliani wrote:
>> Please, why the below  powerToPos  is not checked as terminating ?
>>
>>
>> {-# OPTIONS --termination-depth=3 #-}
>> module Report where
>> open import Level    using () renaming (zero to 0ℓ)
>> open import Function using (case_of_)
>> open import Relation.Binary
>>             using (module Setoid; module 
>> IsEquivalence;_Preserves_⟶_)
>> open import Relation.Binary.PropositionalEquality using (_≡_)
>> open import Algebra    using (Semigroup; module Semigroup)
>> open import Data.Empty using (⊥)
>> open import Data.List  using ([]; _∷_)
>> open import Data.Fin   using (Fin) renaming (zero to 0b; suc to 
>> sucB)
>> open import Data.Digit using (Bit)
>> open import Data.Bin   using (Bin⁺)
>>
>> 1b : Bit
>> 1b = sucB 0b
>>
>> postulate H : Semigroup 0ℓ 0ℓ
>>
>> open Semigroup H using (setoid; _≈_; _∙_)
>>                        renaming (Carrier to C; isEquivalence to 
>> ≈equiv)
>> open IsEquivalence ≈equiv using ()
>>                  renaming (refl to ≈refl; sym to ≈sym; trans to 
>> ≈trans)
>>
>> HasLast1 : Bin⁺ → Set       -- "is the bit list of a non-zero 
>> binary"
>> HasLast1 []           =  ⊥
>> HasLast1 (b ∷ [])     =  b ≡ 1b
>> HasLast1 (_ ∷ b ∷ bs) =  HasLast1 (b ∷ bs)
>>
>> powerToPos : C → (bs : Bin⁺) → HasLast1 bs → C
>>
>> [..]
>
>> The recursion     (b ∷ b' ∷ bs)  -->  (b' ∷ bs)
>>
>> by the second argument is well-founded. Why does not the checker see 
>> the
>> termination proof?
>
>
> Sorry, the implementation needs to be
>
> powerToPos _ []                    ()
> powerToPos x (0b      ∷ [])        ()
> powerToPos x (sucB 0b ∷ [])        _   =  x
> powerToPos x (sucB (sucB ()) ∷ [])
>
> powerToPos x (b ∷ b' ∷ bs)  last1-b:b':bs =
>                            case b of \ { 0b              → p ∙ p
>                                        ; (sucB 0b)       → x ∙ (p ∙ 
> p)
>                                        ; (sucB (sucB ()))
>                                        }
>                            where
>                            hl1 : HasLast1 (b' ∷ bs)
>                            hl1 = last1-b:b':bs
>
>                            p = powerToPos x (b' ∷ bs) hl1
> 
> -----------------------------------------------------------------------
>
> And again, I do not understand why is not it checked as terminating.
>
> Thanks,
>
> ------
> Sergei
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda

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

Theoretical Computer Science, University of Munich 
http://www.tcs.informatik.uni-muenchen.de/~abel/