[Agda] strange termination check

[Sergei Meshveliani]

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,
and ask:
    "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
>