[Agda] termination example

Andreas Abel andreas.abel at ifi.lmu.de
Mon Sep 30 15:31:01 CEST 2013


There are two small things to change to make your example pass the 
termination checker:

1. add

   {-# OPTIONS --termination-depth=3 #-}

2. change the recursive call

   power cnt'' ...

    into

   power (suc (suc cnt)) ...

Explanations:

2. The termination checker does not see through 'where'-definitions. 
Thus, cnt'' is not expanded to (suc (suc cnt)) during termination 
checking.

1. When you want the termination checker to accept a recursive call with

     (suc (suc cnt))

   in the context of a function called with

     (suc (suc (suc cnt)))

   you have to make it count to 3.  [Usually it only counts to 1.]  So 
you have to set the termination-depth to 3.

Cheers,
Andreas

On 30.09.2013 08:25, Serge D. Mechveliani wrote:
> Please,
> why the checker does not prove termination of the function
> `power' in the attached program?
> (about 140 lines in the attached  Main.zip).
>
> The last clause of `power' has the first argument
>                                     suc (suc (suc cnt)),
>
> and `power' is recursively called in the RHS with the first
> argument
>                             cnt'' = suc (suc cnt).
>
> So, the checker must decide that `power' terminates.
> But it does not decide.
>
> It this an error in the checker?
>
> Thank you in advance for explanation,
>
> ------
> 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
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/
-------------- next part --------------
{-# OPTIONS --termination-depth=3 #-}

module Main where
open import Foreign.Haskell
open import IO.Primitive
open import Data.String as String using (toCostring)

open import Function using (_$_; _?_; case_of_)
open import Relation.Nullary.Core using (Dec; yes; no)
open import Relation.Binary
            using (DecTotalOrder; module DecTotalOrder;
                                  module StrictTotalOrder)
open import Relation.Binary.Core
         using (IsEquivalence; module IsEquivalence; _Preserves_?_)
open import Relation.Binary.PropositionalEquality as PropEq
                          using (_?_; _?_)
                          renaming (cong to ?cong; cong? to ?cong?)
import Relation.Binary.EqReasoning as EqR
open import Algebra      using (Semigroup; module Semigroup)
open import Data.Empty   using (?-elim)
open import Data.Sum     using (_?_; inj?; inj?)
open import Data.Product using (proj?)
open import Data.Nat as Nat
     using (?; suc; _<_; _?_; _>_; _?_; _?_; _?_; s?s; z?n; ?_/2?;
                                                module ?-Reasoning)
     renaming (decTotalOrder to natDTO)

open import Data.Nat.Properties using (?-step; pred-mono)
                              renaming (strictTotalOrder to natSTO)
open ?-Reasoning using ()
                 renaming (begin_ to ?begin_; _? to _?end;
                           _??_?_ to _??[_]_; _??_?_ to _?[_]_)


-------------------------------------------------------------------
half : ? ? ?
half = ?_/2?

open DecTotalOrder natDTO using ()
          renaming (isEquivalence to natEquiv; reflexive to ?refl;
                              trans to ?trans; antisym to ?antisym)
open IsEquivalence natEquiv using ()
                            renaming (refl to ?refl; sym to ?sym)
open StrictTotalOrder natSTO using (compare; <-resp-?)
                    renaming (irrefl to <-irrefl; trans to <-trans)

suc>0 : ? {m} ? suc m > 0
suc>0 = s?s z?n

<-antisym : ? {m n} ? m < n ? n ??m
<-antisym m<n n<m =  <-irrefl ?refl $ <-trans m<n n<m

m<suc-m : ? {m} ? m < suc m
m<suc-m = ?refl ?refl

m?suc-m : ? {m} ? m ? suc m
m?suc-m = ?-step $ ?refl ?refl

2+m>1 :  ? {m} ? suc (suc m) > 1  -- 2 ? suc suc m
2+m>1 =  s?s $ s?s z?n

??? : ? {m n} ? m < n ? m ? n ? m ? n
??? (inj? m=n) =  ?refl m=n
??? (inj? m<n) =  ?trans m?m' m<n  where
                                   m?m' = ?-step $ ?refl ?refl

<?? : ? {m n} ? m < n ? m ? n
<?? = ??? ? inj?

<?? : ? {m n} ? m < n ? m ? n
<?? {_} {n} m<n m=n =  <-irrefl ?refl n<n  where
                                           resp = proj? <-resp-?
                                           n<n  = resp m=n m<n
>?? : ? {m n} ? m > n ? m ? n
>?? m>n m?n =  <?? n<m n=m  where
                            n<m = m>n
                            n?m = <?? n<m
                            n=m = ?antisym n?m m?n

??? : ? {m n} ? m ? n ? m ? n
??? m?n m>e =  >?? m>e m?n

half? : (m : ?) ? half m ? m
half? 0             = z?n
half? (suc 0)       = z?n
half? (suc (suc m)) =
                  ?begin  half (suc (suc m))  ??[ ?refl ]
                          suc (half m)        ?[ s?s $ half? m ]
                          suc m               ?[ m?suc-m ]
                          suc (suc m)
                  ?end

monot-half : ? {m n} ? m ? n ? half m ? half n
monot-half {0}           {_}   _      =  z?n
monot-half {1}           {_}   _      =  z?n
monot-half {suc (suc m)} {0}   m''?0  =  ?-elim $ m''?0 suc>0
                                         where
                                         m''?0 = ??? m''?0

monot-half {suc (suc m)} {suc 0} m''?1 =  ?-elim $ m''?1 2+m>1
                                          where
                                          m''?1 = ??? m''?1

monot-half {suc (suc m)} {suc (suc n)} m''?n'' =
      ?begin
          half (suc (suc m))   ??[ ?refl ]
          suc (half m)          ?[ s?s $ monot-half {m} {n} m?n ]
          suc (half n)         ??[ ?sym ?refl ]
          half (suc (suc n))
      ?end
      where  m?n = pred-mono $ pred-mono m''?n''

------------------------------------------------------------------
data Even : ? ? Set where
                    even0  : Even 0
                    even+2 : {n : ?} ? Even n ? Even (suc (suc n))

even? : (n : ?) -> Dec (Even n)
even? 0              = yes even0
even? (suc 0)        = no (? ())
even? (suc (suc n))  with even? n
...                | yes p = yes (even+2 p)
...                | no  p = no  (\ {(even+2 x) ? p x})


-------------------------------------------------------------------
module Power-pack ? ?= (H : Semigroup ? ?=)
  where
  open Semigroup H using (_?_) renaming (Carrier to C)

  power : (cnt : ?) ? C ? (e : ?) ? e > 0 ? e < cnt ? C

  -- The power  x^e  computed by a binary method.
  -- cnt      is the counter used for termination proof
  --          (to be initiated as  suc e).
  -- e < cnt  is a certain condition to be used in proofs about
  --                                                      `power'.

  power 0   x  _            _  ()
  power _   x  0            ()
  power _   x (suc 0)       _  _     =  x
  power 1   _ (suc (suc e)) _  e''<1 =  ?-elim $ e''?1 e''<1
                                        where
                                        e''?1 = <-antisym 2+m>1
  power 2   _ (suc (suc e)) _  e''<2 =  ?-elim $ 2?e'' e''<2
                                        where
                                        2?e'' = s?s $ s?s z?n
                                        2?e'' = ??? 2?e''

  power (suc (suc (suc cnt))) x (suc (suc e)) _ e''<cnt''' =
                                            case  even? e  of \
                                            { (yes _) ? p ? p
                                            ; _       ? x ? (p ? p) }
        where
        e'     = suc e
        e''    = suc e'
        cnt'   = suc cnt
        cnt''  = suc cnt'
        half-e = half e
        half'e = suc half-e
        e?cnt  = pred-mono $ pred-mono $ pred-mono e''<cnt'''

        half-e?half-cnt : half-e ? half cnt
        half-e?half-cnt = monot-half e?cnt

        half'e<cnt'' : suc (suc half-e) ? cnt''
        half'e<cnt'' =
          ?begin  suc (suc half-e)      ?[ s?s $ s?s half-e?half-cnt ]
                  suc (suc (half cnt))  ?[ s?s $ s?s $ half? cnt ]
                  cnt''
          ?end

        p = power (suc (suc cnt)) x half'e suc>0 half'e<cnt''

------------------------------------------------------------
main : IO Unit
main = putStrLn $ toCostring "done"


More information about the Agda mailing list