[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