module WellfoundRecursion where open import Relation.Nullary open import Relation.Binary.PropositionalEquality open import Data.Empty open import Data.Product open import Data.Sum open import Data.Nat open import DownwardLeq -- Well-founded recursion. Most of the utilitiies are already -- defined in Induction.WellFounded in Standard Library. -- Accessibility data Acc {a : Set}(_<_ : a -> a -> Set) : a -> Set where acc : (x : a) -> (forall y -> y < x -> Acc _<_ y) -> Acc _<_ x acc-elim : {a : Set} (_<_ : a -> a -> Set) {P : a -> Set} -> ((x : a) -> (forall y -> y < x -> Acc _<_ y) -> (forall y -> y < x -> P y) -> P x) -> (x : a) -> Acc _<_ x -> P x acc-elim _<_ Φ x (acc .x h) = Φ x h (\y y acc-elim _<_ Φ y (h y y a -> Set) {P : a -> Set} -> ((x : a) -> (forall y -> R y x -> P y) -> P x) -> (x : a) -> (accx : Acc R x) -> P x acc-fold R {P} f x (acc .x h) = f x (\y yRx -> acc-fold R f y (h y yRx)) well-found : {a : Set} -> (a -> a -> Set) -> Set well-found _<_ = forall x -> Acc _<_ x rec-wf : {a : Set} {_<_ : a -> a -> Set} {P : a -> Set} -> well-found _<_ -> ((x : a) -> ((y : a) -> y < x -> P y) -> P x) -> (x : a) -> P x rec-wf {a}{_<_} wf f x = acc-fold _<_ f x (wf x) -- Example: Nat ℕ<-wf : well-found _<′_ ℕ<-wf n = acc n (access n) where access : (n : ℕ) -> (m : ℕ) -> m <′ n -> Acc _<′_ m access zero m () access (suc n) .n ≤′-refl = acc n (access n) access (suc n) m (≤′-step m ℕ half = rec-wf ℕ<-wf body where body : (n : ℕ) -> ((m : ℕ) -> m <′ n -> ℕ) -> ℕ body zero rec = zero body (suc zero) rec = zero body (suc (suc n)) rec = suc (rec n (≤′-step ≤′-refl)) -- Example: intergal division. -- this definition does not pass the termination check. div : ℕ -> ℕ -> ℕ div zero n = zero div (suc m) zero = suc m div (suc m) (suc n) = suc (div (suc m ∸ suc n) (suc n)) -- well, I feel lazy proving this... postulate sm-sn ((suc m ∸ suc n) <′ suc m) -- terminating version of div div-wf : ℕ -> ℕ -> ℕ div-wf m n = rec-wf ℕ<-wf (body n) m where body : (n : ℕ) -> (m : ℕ) -> ((k : ℕ) -> k <′ m -> ℕ) -> ℕ body n zero rec = zero body zero (suc m) rec = suc m body (suc n) (suc m) rec = suc (rec (suc m ∸ suc n) (sm-sn ℕ -> Acc _<′_ m -> ℕ div-wf' zero n _ = zero div-wf' (suc m) zero _ = suc m div-wf' (suc m) (suc n) (acc .(suc m) h) = suc (div-wf' (suc m ∸ suc n) (suc n) (h (suc m ∸ suc n) (sm-sn ℕ -> ℕ -> Set m < n ≤ k = (m <′′ n) × (n ≤′′ k) ◁ : ℕ -> ℕ -> ℕ -> Set (◁ k) m n = n < m ≤ k ◁-access : forall k m n -> (m <′′ k) -> (m < n ≤ k) -> Acc (◁ k) n ◁-access .(suc m) m .(suc m) ≤′′-refl (≤′′-refl , 1+m≤1+m) = acc (suc m) (\y 1+m ⊥-elim (¬[m ◁-access k (suc m) y 1+m well-found (◁ k) ℕ◁-wf k m = acc m access where access : forall n -> (m <′′ n × n ≤′′ k) -> Acc (◁ k) n access n (m ℕ -> Set P k n = Σ ℕ (\fn -> n ≤′′ k -> fn ≡ k) f : (k : ℕ) -> (n : ℕ) -> P k n f k = rec-wf (ℕ◁-wf k) body where body : (i : ℕ) -> ((j : ℕ) -> i < j ≤ k -> P k j) -> P k i body n rec with (k ≤′′? n) ... | inj₁ k≤n = (n , \n≤k -> ≤′′-antisym n≤k k≤n) ... | inj₂ n n <′′ i) (≡-sym m≡k) n m ≤′′ i) m≡k ≤′′-refl) ... | (h , m≤k⇒h≡k) = (h , \_ -> m≤k⇒h≡k (≡-subst (\i -> m ≤′′ i) m≡k ≤′′-refl)) -- Building new accessibility from old. -- relations ℙ : Set -> Set1 ℙ A = A -> Set singleton : {A : Set} -> A -> ℙ A singleton a = \b -> a ≡ b _←_ : Set -> Set -> Set1 B ← A = A -> B -> Set _º : {A B : Set} -> B ← A -> A ← B (r º) b a = r a b infixr 8 _·_ infixr 9 _○_ _·_ : {A B : Set} -> (B ← A) -> ℙ A -> ℙ B (R · s) b = ∃ (\a -> (s a × R a b)) _○_ : {A B C : Set} -> C ← B -> B ← A -> C ← A (R ○ S) a = R · (S a) infixr 2 _⊆_ _⊇_ _⊆_ : {A : Set} -> ℙ A -> ℙ A -> Set r ⊆ s = forall a -> r a -> s a _⊇_ : {A : Set} -> ℙ A -> ℙ A -> Set r ⊇ s = s ⊆ r infixr 6 _⊑_ _⊒_ _⊑_ : {A B : Set} -> (B ← A) -> (B ← A) -> Set R ⊑ S = forall a -> R a ⊆ S a _⊒_ : {A B : Set} -> (B ← A) -> (B ← A) -> Set R ⊒ S = S ⊑ R fun : {A B : Set} -> (A -> B) -> (B ← A) fun f a = singleton (f a) acc-⊑ : {a : Set}{_≪_ _<_ : a -> a -> Set} -> _≪_ ⊑ _<_ -> (x : a) -> Acc _<_ x -> Acc _≪_ x acc-⊑ {a}{_≪_} ≪⊑< x (acc .x h) = acc x access where access : (y : a) -> (y ≪ x) -> Acc _≪_ y access y y≪x = acc-⊑ ≪⊑< y (h y (≪⊑< y x y≪x)) acc-fRfº : {a b : Set}{R : a -> a -> Set}{f : a -> b} -> (x : a) -> Acc (fun f ○ R ○ ((fun f) º)) (f x) -> Acc R x acc-fRfº {a}{b}{R}{f} x (acc ._ h) = acc x access where access : (y : a) -> R y x -> Acc R y access y xRy = acc-fRfº y (h (f y) (x , ((y , (≡-refl , xRy)) , ≡-refl))) -- transitive closure data _⁺ {a : Set}(R : a -> a -> Set) : a -> a -> Set where ⁺-base : forall {x y} -> R x y -> (R ⁺) x y ⁺-step : forall {x z} -> Σ a (\y -> R y z × (R ⁺) x y) -> (R ⁺) x z acc-tc : {a : Set}{R : a -> a -> Set} -> (x : a) -> Acc R x -> Acc (R ⁺) x acc-tc {a}{R} x ac = acc x (access x ac) where access : (x : a) -> Acc R x -> (y : a) -> (R ⁺) y x -> Acc (R ⁺) y access x (acc .x h) y (⁺-base yRx) = acc-tc y (h y yRx) access x (acc .x h) y (⁺-step (z , (zRx , yR⁺z))) = access z (h z zRx) y yR⁺z {-- Expanding the definition, we get: rec_wf {a}{_<_} wf f x with wf x ... | (acc .x h) = f x (\y y acc_rec _<_ (\z _ -> f z) y (h y y rec_wf wf f y) x₁ x₂ x₃ . --} } wf f x = f x (\y y rec_wf wf f y) x₁ x₂ x₃ . --}