[Agda] proposal with WellFounded

[Sergei Meshveliani]

(what is a correct place to submit proposals on the language?)


Dear Agda developers,

I propose to add to Agda _language_ the construct of well-founded
recursion

(see the attachment to this letter).

I believe it is easy to implement.
The extension will preserve all the existing applied code.

The reason for adding this construct is that using the feature of
WellFounded of Standard library complicates programs essentially.


Example
-------

----------------------------------------------
data Bin : Set -- A new definition of Bin
where
0# : Bin
2suc : Bin → Bin -- \n→ 2*(1+n) arbitrary nonzero even
suc2* : Bin → Bin -- \n→ 1 + 2n arbitrary odd

{-# TERMINATING #-}
log₂ : (x : Bin) → x ≢ 0# → ℕ -- integer part of (logarithm₂ x)

log₂ 0# 0≢0 = contradiction refl 0≢0
log₂ (2suc x) _ = 1+ (log₂ (suc x) suc≢0) -- (*)
log₂ (suc2* 0#) _ = 0
log₂ (suc2* (2suc x)) _ = 1+ (log₂ (2suc x) 2suc≢0)
log₂ (suc2* (suc2* x)) _ = 1+ (log₂ (suc2* x) suc2*≢0)
---------------------------------------------------------


`TERMINATING' is set because the rule of (*) is not by a structural
recursion.

Then I prove various properties:

---------------------------------------------------------
log₂∘2* : (x : Bin) → (nz : x ≢ 0#) → (2x≢0 : 2* x ≢ 0#) →
log₂ (2* x) 2x≢0 ≡ 1+ (log₂ x nz)

log₂∘2* 0# nz _ = contradiction refl nz
log₂∘2* (2suc _) _ _ = refl
log₂∘2* (suc2* x) x'≢0 2x'≢0 = ...
...
---------------------------------------------------------


To remove `TERMINATING', it is needed either to add some counter
processing to the loop or to apply WellFounded recursion on Bin that
uses the inequality suc x < 2suc x.

The first approach complicates the program greatly. It becomes
considerably more complex than the fragment in possible textbook or a
paper:

< The source of log₂ >
++
"(*) terminates, because IsWellFoundedOrder _<_ and because
lt : suc x < 2suc x
lt = BinOrd.suc-x<2suc-x x
".

The second approach currently is possible only by using the feature of
WellFounded of Standard library:


----------------------------------------------------------------
open All <-wellFounded using () renaming (wfRec to <-rec)

P : Bin → Set
P x = (x ≢ 0#) → ℕ

log₂ : (a : Bin) → P a -- signature changed

log₂ = <-rec _ P log
where
log : (a : Bin) → (∀ x → x < a → P x) → P a

log 0# _ 0≢0 = contradiction refl 0≢0
log (2suc x) logRec _ =
1+ (logRec (suc x) suc-x<x' suc≢0)
where
suc-x<x' =
begin suc x <[ x<2x (suc x) suc≢0 ]
2* (suc x) ≡[ sym (2suc-as∘ x) ]
2suc x
∎

log (suc2* 0#) _ _ = 0
log (suc2* (2suc x)) logRec _ =
1+ (logRec x' (x<suc2*-x x') 2suc≢0)
where
x' = 2suc x

log (suc2* (suc2* x)) logRec _ =
1+ (logRec x' (x<suc2*-x x') suc2*≢0)
where
x' = suc2* x
----------------------------------------------------------------

A proof for suc-x<x' is all right, it is needed in any approach.

But the program is complicated greatly:
the signature of
(a : Bin) → a ≢ 0# → ℕ
is changed to (a : Bin) → P a,

the call (<-rec _ P log) appears, with a certain complicated signature
for log.

Furthermore, the proofs are broken. For example, the rule

log₂∘2* (2suc _) _ _ = refl

is not type-checked any more.
I expect difficulties in reorganizing proofs.


Proposal
========

To add to Agda _language_ the construct of well-founded recursion --
in the following way.

1. Add to Standard library the notion of IsWellFoundedOrder :

--------------------------------------------------------------------
Sequence : ∀ {α} → (A : Set α) → Set α -- infinite sequences in A
Sequence A = ℕ → A

module OfWellFounded {α α= α<} (PO : StrictPartialOrder α α= α<)
where
open StrictPartialOrder PO using (_≈_; _<_) renaming (Carrier to C)

_≀_ : Rel C _
x ≀ y = x < y ⊎ x ≈ y

DecrementBreak : Sequence C → Set _
DecrementBreak f = ∃ (\n → f n ≀ f (suc n))

IsWellFoundedOrder : Set _
IsWellFoundedOrder = (f : Sequence C) → DecrementBreak f
--------------------------------------------------------------------

The property is "any sequence has a decrement break".



2. The language construct is as in the following example with log₂:

---------------------------------------------------------------
log₂ : (x : Bin) → x ≢ 0# → ℕ -- signatures do not change!

log₂ 0# 0≢0 = contradiction refl 0≢0
log₂ (2suc x) _ =
1+ (recurseWith isWellFoundedOrder lt
(log₂ (suc x) suc≢0)
)
where
lt : suc x < 2suc x
lt = Ord0.suc-x<2suc-x x

log₂ (suc2* 0#) _ = 0
log₂ (suc2* (2suc x)) _ = 1+ (log₂ (2suc x) 2suc≢0)
log₂ (suc2* (suc2* x)) _ = 1+ (log₂ (suc2* x) suc2*≢0)
---------------------------------------------------------------


Here the result of
(recurseWith isWellFoundedOrder lt (log₂ (suc x) suc≢0))
is
(log₂ (suc x) suc≢0).

recurseWith is a built-in function.
In this example, it makes the type checker to do the following.
It checks the proofs for lt and isWellFoundedOrder,
and thus it concludes that this recursive call of log₂ is well founded.
As other rules for log₂ use structural recursion, it concludes that
log₂ is terminating.

This is a termination _axiom_ by IsWellFoundedOrder applied by the
_type checker_.

How difficult is it to implement in the type checker?

The user program remains clear.
I hope, the proofs written for the `TERMINATING' version will remain.

It is easy to prove IsWellFoundedOrder for Nat._<_, Bin._<_, and so
on.

I appreciate: WellFounded of Standard is a clever way to bring a
traditional termination proof tool without extending language.
Programmers are free to use it.

But it is also desirable to give the possibility to write "normal"
programs, in the style of somewhat an ordinary mathematical paper, that
can be understood by mathematicians (and by the program author himself).

Advanced algorithms in mathematics need effort to program.
Many people will like rather to use this small language extension than
to complicate further the program by artificially changing signatures in
a clever way.

I append to this letter the full source for the IsWellFoundedOrder
feature, together with its implementation for ℕ.

Regards,

------
Sergei

[Sergei Meshveliani]

Another point: what is about the performance overhead?

Is there known a simple example when the well-founded recursion by
WellFounded of Standard increases the run-time cost essentially?

--
SM

Post by Sergei Meshveliani
(what is a correct place to submit proposals on the language?)
Dear Agda developers,
I propose to add to Agda _language_ the construct of well-founded
recursion
(see the attachment to this letter).
I believe it is easy to implement.
The extension will preserve all the existing applied code.
The reason for adding this construct is that using the feature of
WellFounded of Standard library complicates programs essentially.
Example
-------
[..]

[Ulf Norell]

Post by Sergei Meshveliani
(what is a correct place to submit proposals on the language?)

The best place to submit language extension proposals is to the github
issue tracker:

https://github.com/agda/agda/issues/new

/ Ulf