[Agda] simple example

[Serge D. Mechveliani]

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