[Agda] proposal with WellFounded
Sergei Meshveliani
mechvel at botik.ru
Tue Aug 21 13:09:00 CEST 2018
(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
-------------- next part --------------
-- This is type-checked in Agda-2.5.4.
module WellFounded-2 where
open import Function using (flip; _∘_)
open import Relation.Binary using (Rel; StrictPartialOrder; StrictTotalOrder)
open import Data.Sum using (_⊎_)
open import Data.Product using (_,_; ∃)
open import Data.Nat using (ℕ; suc)
--****************************************************************************
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
IsDecreasing : Sequence C → Set _
IsDecreasing f =
∀ n → f (suc n) < f n
DecrementBreak : Sequence C → Set _
DecrementBreak f = ∃ (\n → f n ≤ f (suc n))
IsWellFoundedOrder : Set _
IsWellFoundedOrder = (f : Sequence C) → DecrementBreak f
------------------------------------------------------------------------------
module WellFounded-<-Nat -- Example. IsWellFoundedOrder for _<_ on ℕ
where
open import Relation.Binary using (Tri)
open import Relation.Binary.PropositionalEquality using
(_≡_; refl; sym; cong; subst)
open import Data.Sum using (inj₁; inj₂)
open import Data.Nat using (_<_; z≤n; s≤s) renaming (_≤_ to _≤'_)
open import Data.Nat.Properties using (<-cmp; pred-mono)
renaming (≤-refl to ≤'-refl; ≤-trans to ≤'-trans;
<⇒≤ to <⇒≤'; <-strictTotalOrder to sto)
open StrictTotalOrder sto using ()
renaming (strictPartialOrder to spo)
open OfWellFounded spo using (IsWellFoundedOrder; _≤_; DecrementBreak)
-- _≤_ of OfWellFounded is defined via disjunctionб unlike Nat._≤_,
-- but these realtions are equal on ℕ.
0<1+n : {n : ℕ} → 0 < suc n
0<1+n = s≤s z≤n
≤'0⇒≡ : {n : ℕ} → n ≤' 0 → n ≡ 0
≤'0⇒≡ z≤n = refl
≤'⇒⊎ : {m n : ℕ} → m ≤' n → m < n ⊎ m ≡ n
≤'⇒⊎ {0} {0} _ = inj₂ refl
≤'⇒⊎ {0} {suc n} _ = inj₁ 0<1+n
≤'⇒⊎ {suc m} {suc n} (s≤s m≤n) with ≤'⇒⊎ m≤n
... | inj₂ m=n = inj₂ (cong suc m=n)
... | inj₁ m<n = inj₁ m''≤n'
where
m' = suc m
m''≤n' : suc m' ≤' suc n
m''≤n' = s≤s m<n
0≤ : {n : ℕ} → 0 ≤ n
0≤ = ≤'⇒⊎ z≤n
open Tri
----------------------------------------------------------------------------
isWellFoundedOrder : IsWellFoundedOrder
-- prove that _<_ is WellFounded on ℕ
isWellFoundedOrder f = decrBreak 0 (f 0) ≤'-refl
where
decrBreak : (n v : ℕ) → f n ≤' v → DecrementBreak f
decrBreak n 0 fn≤'0 =
(n , fn≤f-suc-n)
where
fn≡0 = ≤'0⇒≡ fn≤'0
fn≤f-suc-n = subst (_≤ (f (suc n))) (sym fn≡0) 0≤
decrBreak n (suc v) fn≤'suc-v with <-cmp (f n) (f (suc n))
...
| tri< fn<f-suc-n _ _ = (n , inj₁ fn<f-suc-n)
... | tri≈ _ fn≡f-suc-n _ = (n , inj₂ fn≡f-suc-n)
... | tri> _ _ fn>f-suc-n = decrBreak (suc n) v f-suc-n-≤'-v
where
suc-f-suc-n-≤'-suc-v = ≤'-trans fn>f-suc-n fn≤'suc-v
f-suc-n-≤'-v = pred-mono suc-f-suc-n-≤'-suc-v
{- This is a commentary **************************************************
Example of using IsWellFoundedOrder.
---------------------------------------------------------------------
module WellFounded-<-bin where
open import BinOrd using (strictPartialOrder)
open OfWellFounded strictPartialOrder using
(IsWellFoundedOrder; _≤_; DecrementBreak)
isWellFoundedOrder : IsWellFoundedOrder
-- prove that IsWellFounded for _<_ on Bin
isWellFoundedOrder f = decrBreak 0 (f 0) ≤-refl
where
...
-------------------------------------------------------------------------
module LogarithmOnBin where
data Bin : Set where
0# : Bin
2suc : Bin → Bin -- \n→ 2*(1+n) arbitrary nonzero even
suc2* : Bin → Bin -- \n→ 1 + 2n arbitrary odd
log₂ : (x : Bin) → x ≢ 0# → ℕ -- integer part of logarithm₂
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. Here 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.
-}
More information about the Agda
mailing list