日々の流転

λ. Agda2でクイックソート

LLTV後の飲み会でranhaさんが、クイックソートの停止性をAgda2の停止性チェッカに説得できないというような事を話していた(参考: 修行失敗 - Yet Another Ranha (2009-08-27))ので、Agdaさんを説得してみた。 基本的には length (filter p xs) ≦ length xs の証明 と Wellfounded induction in Agda2 で書いたのを組み合わせただけなんだけど、Agda2のライブラリの使い方を調べるのが面倒くさかったよ……

module Quicksort where

open import Data.Bool
open import Data.Nat
open import Data.List
open import Relation.Binary using (Rel)
import Induction.WellFounded as WF
open WF using (Acc; acc)
open WF _<′_ using () renaming (Acc to <-Acc)
open import Induction.Nat using (<-allAcc)

R : ∀ {A} → Rel (List A)
R {A} xs ys = length xs <′ length ys

R-allAcc : ∀ {A} xs → Acc (R {A}) xs
R-allAcc xs = f xs (<-allAcc (length xs))
  where
    f : ∀ xs → <-Acc (length xs) → Acc R xs
    f xs (acc rs) = acc (λ ys h → f ys (rs (length ys) h))

s≤′s : ∀ {m n} → (m ≤′ n) → suc m ≤′ suc n
s≤′s ≤′-refl = ≤′-refl
s≤′s (≤′-step h) = ≤′-step (s≤′s h)

length-filter
  : ∀ {A} → (f : A → Bool) → (xs : List A)
  → length (filter f xs) ≤′ length xs
length-filter f [] = ≤′-refl
length-filter f (x ∷ xs) with f x
... | true  = s≤′s (length-filter f xs)
... | false = ≤′-step (length-filter f xs)

length-filter′
  : ∀ {A} → (f : A → Bool) → (x : A) → (xs : List A)
  → length (filter f xs) <′ length (x ∷ xs)
length-filter′ f x xs = s≤′s (length-filter f xs)

quicksort′
  : ∀ {A} → (A → A → Bool) → (xs : List A)
  → ((ys : List A) → R ys xs → List A) → List A
quicksort′ _≤?_ [] f = []
quicksort′ _≤?_ (x ∷ xs) f = f ys ys-lem ++ [ x ] ++ f zs zs-lem
  where
    ys = filter (λ y → y ≤? x) xs
    zs = filter (λ y → not (y ≤? x)) xs
    ys-lem : R ys (x ∷ xs)
    ys-lem = length-filter′ (λ y → y ≤? x) x xs
    zs-lem : R zs (x ∷ xs)
    zs-lem = length-filter′ (λ y → not (y ≤? x)) x xs

quicksort : ∀ {A} → (A → A → Bool) → List A → List A
quicksort {A} _≤?_ = wfRec (λ _ → List A) (quicksort′ _≤?_)
  where open WF.All R R-allAcc

参考

• Coqで、クイックソート - にわとり小屋でのプログラミング日記(2008-03-08)