# [Agda] strange termination check

Sergei Meshveliani mechvel at botik.ru
Sat Oct 12 11:42:15 CEST 2013

```On Sat, 2013-10-12 at 14:33 +0900, Andreas Abel wrote:
> 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.
>

The consequence is that one does not know how to provide termination
without complications brought with inductive types.
For example, I tried to replace in the below example the step
(b ∷ b' ∷ bs)  -->   b' ∷ bs

with one-level step, by denoting  b'' = b' :: bs  ...
And failed.

Is this difficult (if correct) to implement in Agda, say,
"termination by a proper subterm" ?

> See my previous message
>
>    https://lists.chalmers.se/pipermail/agda/2013/005855.html
>
> for an implementation of powerToPos that works.

The story is as follows.

My current aim is
(1) to have the binary exponentiation method  powerToPos  both for  Bin
(Bin⁺)  and for  Nat,
(2) to provide a proof
powerEq :  ...  powerToPos x (suc n) == x ∙ (powerToPos x n)

for  n : Bin⁺,  Nat
(for  Bin⁺,  suc is converted to  (addCarryToBitList 1b)).

I think that it is better to do all this first for  Bin⁺, and then to
prove this for Nat by applying the conversions  Nat <-> Bin⁺.

And the law (2) does not hold for your version of  binPower
(probably, this can be tackled somehow).

So, I try another version:  powerToPos,  with the condition argument
(Positive bs)  expressing  "last bit is 1".
There I have a strange problem with the recursion step
(b ∷ b' ∷ bs)  -->  b' ∷ bs,
"has it sense for Agda to generalize the termination condition
respectively?"
(also is it difficult to implement?).

Meanwhile, I modify the implementation for  HasLast1  to

data Positive : Bin⁺ → Set         -- "has last 1"
where
single : Positive (1b ∷ [])
cons   : {b : Bit} → {bs : Bin⁺} → Positive bs → Positive (b ∷ bs)

And this helps with termination for  powerToPos.
I do not know precisely, why, but probably because Agda sees the step of
(cons positive-bs) --> positive-bs
in another argument.
(In HasLast1, this argument was evaluated to  b == 1b  by normalization,
and this was not a constructor for a recursion step).

But this success is by occasion. In other examples the absence of an
automatic generalized recursion step will bite programmers.

Now, the proof for  (2) for Bin⁺  is close to end. I hope to finish it,
and then hope that  Nat <-> Bin⁺  will help.

Thanks,

------
Sergei

> On 2013-10-11 08:45, Sergei Meshveliani wrote:
> > On Thu, 2013-10-10 at 21:57 +0400, Sergei Meshveliani wr (b ∷ b' ∷ bs)ote:
> >> 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
>

```