[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
More information about the Agda
mailing list