[Agda] WellFounded usage

[Sergei Meshveliani]

Dear all,

I have a certain problem with termination proof.
Consider the example: division with remainder for binary natural
numbers (the code is contrived).

-------------------------------------------------------------------
record DivMod (dividend divisor : Bin) : Set where
constructor result
field
quotient : Bin
remainder : Bin
equality : dividend ≡ remainder + quotient * divisor
rem<divisor : remainder < divisor

-- suc, +, ∾; *, < are of Bin, 1+, +n, ∾n; *n, <n are of ℕ.

∣_∣ : Bin → ℕ
∣ x ∣ = number of bits

divMod : (a b : Bin) → b ≢ 0# → DivMod a b
divMod a b b≢0 =
aux a (toℕ a) ≀-refl
where
aux : (a : Bin) → cnt → toℕ a ≀ cnt → DivMod a b
aux a 0 aN≀0 =
result 0# 0# a≡0+0*b 0<b
where
a≡0 = derived from aN≀0

aux 0# _ _ = result 0# 0# 0≡0+0*b 0<b

aux a (1+ cnt) aN≀1+cnt = -- here a ≢ 0#
let
aN = toℕ a
e = ∣ a ∣ ∞n ∣ b ∣ ...
d = (2^ e) * b -- 2^ e is by prepending several
-- zero bits.
a' = a ∞ d
a'N = toℕ a'

a'N≀cnt : a'N ≀n cnt
a'N≀cnt =
because a, d ≢ 0#, and toℕ∾homo.

(result q r a'≡r+q*b r<b) = aux a' cnt a'N≀cnt
in
restore a b q r a' r<b
------------------------------------------------------------------

This means that divMod a b is reduced to (divMod (a ∞ d) b),
where d = 2^e * b for a certain appropriate e : ℕ.

The counter cnt = (toℕ a) : ℕ is reduced to a smaller value by this
step.
Due to the structural decrement (suc cnt) -> cnt, Agda decides that
the recursion is terminating.

But this may lead to exponential performance cost, because the unary
representation of cnt is large, and the evaluation (suc cnt) -> snt
takes place not only in the proof part but also in regular evaluation.

To fix this, I change the counter to

cnt = ∣ a ∣ : ℕ = number of bits in a.

Then one needs to prove messy lemmata in order to prove that
∣ a ∣ >n ∣ a' ∣ in the loop.

The question is

does there exist a way for this example to join
* a normal code performance (as in the second method version),
* simple termination proof
?


I see in Standard library Induction/WellFounded.agda.

It is difficult to understand of how to apply this
(the impression is that it will complicate the program).

Can this tool be used to solve the above problem with divMod for Bin ?
Somehow to prove that _>_ is well-founded on Bin
(it is useful for many other programs),
use the tools from WellFounded.agda, and prove termination of divMod
in a simple way and without loosing run-time performance.

Can anybody, please, demonstrate, how this will change the above code
for divMod ?


Another question
----------------

Has it sense the language semantic extension with WellFoundedOrder ?

The property IsWellFoundedOrder concerns any StrictPartialOrder,
and its simple definition is

appended to this letter.

Imagine that the type checker of Agda-extended
sees in the above loop
a a' : Bin and a>a' : a > a',

sees the instance of StrictPartialOrder for _≡_ and _>_ on Bin,
sees the proof for IsWellFoundedOrder for this instance,
and concludes that divMod is terminating -- by the _implicit axiom_
of termination by a well-founded ordering.

With this, the proofs will be much simpler, simpler than with applying
the constructs of Induction of Library.

Agda is able to automatically find an argument in recursion that
decreases structurally. Similarly can it be able to find the argument
decreasing by _<_ and fit for well-founded recursion?

Agda sees that a is replaced with a' in the call, and it needs to
find where in the scope it is proved a > a'. At least this place for
a>a' can be marked, may be, by some pragma.

Thank you in advance for explanation,

------
Sergei

[Sergei Meshveliani]

I'll point out that I applied Induction/WellFounded.agda for exactly
the same purpose (see DivMod.agda and Rec.agda nearby).
Empirically this does not lead to exponential time in benchmarks (at
least when compiled to Haskell), but I don't know why.
Re: your second question, I think your definition is allowing
non-constructive proofs of termination (because IsWellFoundedOrder is
non-constructive), which is probably a significant extension of the
type theory (but I don't really know what I'm talking about).
You could change the definition to be constructive, of course, which
doesn't really affect the rest of the proposal too much.

Yes, it is also all right to relax
¬ IsDecreasing f
to the property
breakDecrease : (f : ℕ → C) → ∃ (\n → ¬ (f n > f (suc n)))

--
SM

Dear all,
I have a certain problem with termination proof.
Consider the example: division with remainder for binary natural
numbers (the code is contrived).
-------------------------------------------------------------------
record DivMod (dividend divisor : Bin) : Set where
constructor result
field
quotient : Bin
remainder : Bin
equality : dividend ≡ remainder + quotient *
divisor
rem<divisor : remainder < divisor
-- suc, +, ∸; *, < are of Bin, 1+, +n, ∸n; *n, <n are of
ℕ.
∣_∣ : Bin → ℕ
∣ x ∣ = number of bits
divMod : (a b : Bin) → b ≢ 0# → DivMod a b
divMod a b b≢0 =
aux a (toℕ a) ≤-refl
where
aux : (a : Bin) → cnt → toℕ a ≤ cnt → DivMod a b
aux a 0 aN≤0 =
result 0# 0# a≡0+0*b 0<b
where
a≡0 = derived from aN≤0
aux 0# _ _ = result 0# 0# 0≡0+0*b 0<b
aux a (1+ cnt) aN≤1+cnt = -- here a ≢ 0#
let
aN = toℕ a
e = ∣ a ∣ ∸n ∣ b ∣ ...
d = (2^ e) * b -- 2^ e is by prepending several
-- zero bits.
a' = a ∸ d
a'N = toℕ a'
a'N≤cnt : a'N ≤n cnt
a'N≤cnt =
because a, d ≢ 0#, and toℕ∸homo.
(result q r a'≡r+q*b r<b) = aux a' cnt a'N≤cnt
in
restore a b q r a' r<b
------------------------------------------------------------------
This means that divMod a b is reduced to (divMod (a ∸ d)
b),
where d = 2^e * b for a certain appropriate e : ℕ.
The counter cnt = (toℕ a) : ℕ is reduced to a smaller value
by this
step.
Due to the structural decrement (suc cnt) -> cnt, Agda decides that
the recursion is terminating.
But this may lead to exponential performance cost, because the unary
representation of cnt is large, and the evaluation (suc cnt) -> snt
takes place not only in the proof part but also in regular evaluation.
To fix this, I change the counter to
cnt = ∣ a ∣ : ℕ = number of bits in a.
Then one needs to prove messy lemmata in order to prove that
∣ a ∣ >n ∣ a' ∣ in the loop.
The question is
does there exist a way for this example to join
* a normal code performance (as in the second method
version),
* simple termination proof
?
I see in Standard library Induction/WellFounded.agda.
It is difficult to understand of how to apply this
(the impression is that it will complicate the program).
Can this tool be used to solve the above problem with divMod
for Bin ?
Somehow to prove that _>_ is well-founded on Bin
(it is useful for many other programs),
use the tools from WellFounded.agda, and prove termination of
divMod
in a simple way and without loosing run-time performance.
Can anybody, please, demonstrate, how this will change the above code
for divMod ?
Another question
----------------
Has it sense the language semantic extension with
WellFoundedOrder ?
The property IsWellFoundedOrder concerns any
StrictPartialOrder,
and its simple definition is
appended to this letter.
Imagine that the type checker of Agda-extended
sees in the above loop
a a' : Bin and a>a' : a > a',
sees the instance of StrictPartialOrder for _≡_ and _>_ on
Bin,
sees the proof for IsWellFoundedOrder for this instance,
and concludes that divMod is terminating -- by the _implicit axiom_
of termination by a well-founded ordering.
With this, the proofs will be much simpler, simpler than with applying
the constructs of Induction of Library.
Agda is able to automatically find an argument in recursion that
decreases structurally. Similarly can it be able to find the argument
decreasing by _<_ and fit for well-founded recursion?
Agda sees that a is replaced with a' in the call, and it needs to
find where in the scope it is proved a > a'. At least this place for
a>a' can be marked, may be, by some pragma.
Thank you in advance for explanation,
------
Sergei
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda