# [Agda] simple example

Serge D. Mechveliani mechvel at botik.ru
Thu Aug 16 12:15:13 CEST 2012

```On Wed, Aug 15, 2012 at 10:33:29AM -0400, Nils Anders Danielsson wrote:

[..]

>> 2. For the initial program, the compiler reports
>>
>>    Termination checking failed for the following functions:  rem
>>    Problematic calls:          rem (n Б┬╦ k) (suc k) p
>>    -- \.-  for subtraction
>>
>> How to fix this?

(this in on my function for remainder for division on Nat).

> You may want to have a look at Data.Nat.DivMod in the standard library
> (but I think I've seen less complicated implementations).

I have an impression that there is built a type representing all
inductive proofs for termination ...
I need to look into this.
Meanwhile, I have a question and a note.

1. Is it possible to  postulate termination  for a given function?

It is possible to  `postulate  newSymbol : T'   for any type T.
So, if the Agada compiler is able to convert each function definition
f  into a type  T(f)  representing termination proofs for  f,  then
`postulate  newSymbol : T(f)'  postulates the termination
-- this is a beginner fantasy.

2. I introduced a `step counter' in my function  rem,  and now its
rules become structurally decreasing:

rem : Nat -> (m : Nat└∙) -> IsPositiveat -> Nat

rem _ zero ()      -- unaccessible
rem n (suc k) _ =  rem' n n
where
rem' : Nat -> Nat -> Nat         -- \ n counter -> r,  counter  is the
--     number of subtractions applied
rem' zero    _         = zero
rem' n       zero      = zero            -- accessible only for  m = 1
rem' (suc n) (suc cnt) = if less n k then  suc n
else              rem' (subtract n k) cnt
-- subtract = \.-

A similar transformation is possible for many programs. This works
as a lemma which makes trivial the termination proof, but this may
complicate proofs for various important properties. On the other hand,
these properties can be postulated, in order to advance with a program
(for practical computing with partial verification), while I do not know
how to postulate termination in a simple way.

Thanks,

------
Sergei
```