TPPmark2017のAgda版解説

この記事は Theorem Prover Advent Calendar 2017 の12/10(日)の記事です。

The 13th Theorem Proving and Provers Meeting (TPP 2017) という定理証明系に関するワークショップでのお題の問題 TPPmark2017 を依存型プログラミング言語 Agda で解いた私の解答について簡単に紹介します。

お題：最長共通部分列問題

TPP2017 のサイトから問題文を引用しておきます。

二つの有限列 s と t を受け取って，その最長共通部分列（の一つ）を返す関数 LCS を定義してください．列はリストなど使用する証明支援系にある適切なデータ構造を使ってください．また，列の要素の型は自然数など適当な型に固定して構いません．

定義した関数が共通部分列を返す，つまり LCS s t が s と t のいずれの部分列にもなっていることを証明してください（必要ならば，部分列であることを表す述語も定義した上で）．

定義した関数が返す共通部分列が最長である，つまり u も s と t の共通部分列ならば u の長さは LCS s t の長さ以下であることを証明してください．

証明全体について

証明自体は https://github.com/msakai/tppmark2017 にあり、この記事を書いている時点での最新版(そしてTPP2017の当日に説明したコード)は、v0.2.0 です。

環境としては、 Agda 2.5.3 と Agda standard library (agda-stdlib) 0.14 を用いています。

`LCS` 関数の定義

まずは証明対象となる LCS 関数の定義ですが、ここではまずはリスト型を対象としDP(動的計画法)を用いない最も単純な実装を対象とすることにしました。これを証明できれば、DPを用いる実装についても同様に証明できるか、もしくはこの実装との等価性を示すことで示すことができると考えたためです（結局DPを用いる実装での証明はやっていないですが）。

要素の型については、決定可能(decidable)な等号が定義された型であれば何でも良いですが、Agdaでそのような関数（Haskellであれば型クラスを使って定義するような関数）を定義する際の流儀を知らないので、ここではとりあえず自然数型 ℕ を用いることにしました。（Agdaでの流儀を知っている人がいたら教えてください！）

longest : ∀ {ℓ} {A : Set ℓ} → List A → List A → List A
longest xs ys with length xs ≤? length ys
... | yes xs≤ys = ys
... | no  xs≰ys = xs

LCS : List ℕ → List ℕ → List ℕ
LCS [] _ = []
LCS (_ ∷ _) [] = []
LCS (x ∷ xs) (y ∷ ys) with x ≟ y
... | yes x≡y = x ∷ LCS xs ys
... | no x≢y  = longest (LCS (x ∷ xs) ys) (LCS xs (y ∷ ys))

ここで _≟_ は (a : ℕ) → (b : ℕ) → Dec (a ≡ b) という型の関数で、 a ≡ b の証明もしくは ¬ (a ≡ b) の証明からなる値を、それぞれ yes, no というコンストラクタで包んで返します。 ≤? も同様です。

先頭要素の比較 x ≟ y と再帰で定義された関数となっています。ここで LCS 関数は再帰呼び出しの際に２つの引数のうちのいずれかが構造的に小さな値となっているため、停止性チェッカが停止性を確認することができ、停止性検査によるエラーは起こりません。

部分列関係の形式化

部分列関係の形式化としては、以下のような定義を用いました。

infix 4 _⊑_

data _⊑_ {ℓ} {A : Set ℓ} : List A → List A → Set ℓ where
  empty : ∀ {xs} → [] ⊑ xs
  here  : ∀ {xs ys x} → xs ⊑ ys → (x ∷ xs) ⊑ (x ∷ ys)
  there : ∀ {xs ys y} → xs ⊑ ys → xs ⊑ (y ∷ ys)

これは、型からも分かるように、以下のことを表しています。

空リストは任意のリストの部分列 (empty)
xs が ys の部分列ならば、両方に x を前置したものも、部分列関係にある (here)
xs が ys の部分列ならば、xs は ys に余計なものを前置した列の部分列でもある
(there)
部分列関係はこれらの規則だけから帰納的に定義される関係である。

部分列の定義としてはごく自然な定義で、他の解答でも同様の定義を持ちいているものが多かったです。

構築子の名前に関しては、以前に見た「リストの要素であること」の以下のような定義を思い出して、この名前を付けました。が、あまり良くない名前だったかも知れません。良い名前があれば教えてください！

data _∈_ {A} (a : A) : List A → Set where
  here  : ∀ {xs} → a ∈ (a ∷ xs)
  there : ∀ {x xs} → a ∈ xs → a ∈ (x ∷ xs)

部分列関係の基本的な性質

続いて部分列関係の基本的な性質を幾つか示しておきます。具体的な証明はここでは省略しますが、いずれも _⊑_ の定義に関する構造的再帰で自明に証明することができます。

tail-⊑ : ∀ {ℓ} {A : Set ℓ} {x : A} {xs} {ys} → x ∷ xs ⊑ ys → xs ⊑ ys

tail-⊑-tail : ∀ {ℓ} {A : Set ℓ} {x : A} {xs} {ys} → x ∷ xs ⊑ x ∷ ys → xs ⊑ ys

length-⊑ : ∀ {ℓ} {A : Set ℓ} {xs ys : List A} → xs ⊑ ys → length xs ≤ length ys

⊑-refl : ∀ {ℓ} {A : Set ℓ} {xs : List A} → xs ⊑ xs

⊑-trans : ∀ {ℓ} {A : Set ℓ} {xs ys zs : List A} → xs ⊑ ys → ys ⊑ zs → xs ⊑ zs

ここでは先に定義してますが、実際には後の証明を行う際に必要なことに気づいてから、戻ってきて証明しています。

ついでに、共通部分列であることを定義しておきます。

_is-common-subsequence-of_ : ∀ {ℓ} {A : Set ℓ} → List A → List A × List A → Set ℓ
_is-common-subsequence-of_ zs (xs , ys) = (zs ⊑ xs) × (zs ⊑ ys)

`longest` 関数に関する基本的な性質

次に　LCS 関数を定義する際に使った longest 関数についても基本的な性質を示しておきます。これらも実際には後の証明を行う際に必要なことに気づいてから戻ってきて証明したものです。

longest-either : ∀ {ℓ₁} {A : Set ℓ₁} {ℓ₂} (P : List A → Set ℓ₂) {xs ys : List A} → P xs → P ys → P (longest xs ys)

longest-left : ∀ {ℓ} {A : Set ℓ} (xs ys : List A) → length xs ≤ length (longest xs ys)

longest-right : ∀ {ℓ} {A : Set ℓ} (xs ys : List A) → length ys ≤ length (longest xs ys)
longest-right xs ys with length xs ≤? length ys
... | yes xs≤ys = ≤-refl
... | no  xs≰ys =
        begin
          length ys
        ≤⟨ n≤1+n (length ys) ⟩
          suc (length ys)
        ≤⟨ ≰⇒> xs≰ys ⟩
          length xs
        ∎
  where open ≤-Reasoning

longest-right についてだけ定義を書いておきましたが、 ≤-Reasoning モジュールを用いると、このように不等式の連鎖の形で不等式の証明を書くことができます（実際には 〈〉 で囲った証明を ≤ の推移律で連鎖させる形の証明になります。参考: TPPmark2014のAgda版解説)

`LCS` が共通部分列を返すことの証明

LCS の再帰と同じ構造を持つ帰納法で自明に示すことができます。

LCS は longest で LCS (x ∷ xs) ys) と LCS xs (y ∷ ys) のどちらかを選んでいるので、どちらが選ばれても大丈夫なことを longest-either を使って示しています。

LCS-⊑-left : ∀ xs ys → LCS xs ys ⊑ xs
LCS-⊑-left [] _     = empty
LCS-⊑-left (_ ∷ _) [] = empty
LCS-⊑-left (x ∷ xs) (y ∷ ys) with x ≟ y
... | yes x≡y = here (LCS-⊑-left xs ys)
... | no  x≢y = longest-either (\zs → zs ⊑ x ∷ xs) (LCS-⊑-left (x ∷ xs) ys) (there (LCS-⊑-left xs (y ∷ ys)))

LCS-⊑-right : ∀ xs ys → LCS xs ys ⊑ ys
LCS-⊑-right [] _       = empty
LCS-⊑-right (_ ∷ _) [] = empty
LCS-⊑-right (x ∷ xs) (y  ∷ ys) with x ≟ y
LCS-⊑-right (x ∷ xs) (.x ∷ ys) | yes refl = here (LCS-⊑-right xs ys)
LCS-⊑-right (x ∷ xs) (y  ∷ ys) | no  x≢y  = longest-either (\zs → zs ⊑ y ∷ ys) (there (LCS-⊑-right (x ∷ xs) ys)) (LCS-⊑-right xs (y ∷ ys))

thereom-1 : ∀ xs ys → LCS xs ys is-common-subsequence-of (xs , ys)
thereom-1 xs ys = (LCS-⊑-left xs ys , LCS-⊑-right xs ys)

あー、 theorem を thereom とtypoしてますね。恥ずかしい……

`LCS` が共通部分列の中で最長のものを返すことの証明

証明したい命題は以下になります。

theorem-2 : ∀ xs ys zs → zs is-common-subsequence-of (xs , ys) → length zs ≤ length (LCS xs ys)

LCS と同じ構造の再帰と zs is-common-subsequence-of (xs , ys) すなわち zs ⊑ xs および zs ⊑ xs の(empty, here, there による)場合分けで示せそうだったのだけど、そうすると停止性チェッカによるエラーを解消することができなかったので、明示的に整礎帰納法（well-founded induction）を用いて書くことに。

順序の定義

書きたいのは LCS と同じ構造の再帰なので、「２つのリストのいずれかが構造的に小さくなっている」ことを表す整礎な順序を定義すれば良いのですが、代わりに同値な「2つのリストの長さの和が小さくなっている」という順序を考えると定義が簡単になります。

まず、sum-length という補助関数を定義します。

sum-length : ∀ {A : Set} → List A × List A → ℕ
sum-length (xs , ys) = length xs + length ys

すると、 sum-length した結果を比較する順序は _<_ on sum-length として定義できます。このような on 関数の使い方は Haskell でも良く使われるので、馴染み深い人も多いでしょう。ちなみに、 _⊰_ という記号はUnicodeのコード表の不等号っぽい記号から適当に選びました（笑）。

_⊰_ : ∀ {A : Set} → Rel (List A × List A) Level.zero
_⊰_ = _<_ on sum-length

次に、この順序が整礎であることの証明ですが、 Induction.WellFounded モジュールには Inverse-image.well-founded という便利な関数が定義されており、これを使うとこのような「関数適用結果を整礎な順序で比較する」順序の整礎性を簡単に示すことができます。

⊰-well-founded : ∀ {A : Set} → Well-founded (_⊰_ {A})
⊰-well-founded = Inverse-image.well-founded sum-length <-well-founded

続いて、 Induction.WellFounded の All モジュールで定義されている関数を、使いやすい名前にリネームしてインポートしておきます。筆者はAgdaのレコードやモジュールの機構をちゃんと理解していないので、 Induction.Nat モジュールでの定義を適当に真似しただけです。

module _ {ℓ} {A} where
  open All (⊰-well-founded {A}) ℓ public
    renaming ( wfRec-builder to ⊰-rec-builder
             ; wfRec to ⊰-rec
             )

そして、 LCS の再帰呼び出しで使われる、 xs, xs のいずれかが短くなる場合、また両方が短くなる場合のそれぞれについて、この順序で小さくなっていることを示しておきましょう。証明はいずれも自明です。

⊰-left : ∀ {A} (x : A) (xs ys : List A) → (xs , ys) ⊰ (x ∷ xs , ys)

⊰-right : ∀ {A} (xs : List A) (y : A) (ys : List A) → (xs , ys) ⊰ (xs , y ∷ ys)

⊰-both : ∀ {A} (x : A) (xs : List A) (y : A) (ys : List A) → (xs , ys) ⊰ (x ∷ xs , y ∷ ys)

整礎帰納法による証明

そして、ようやく実際の証明に。

帰納法の構造が分かりやすいように、示したい性質を P として明示的に定義すると、全体の構造は以下のようになります。

P : ∀ p → Set
P (xs , ys) = ∀ zs → zs is-common-subsequence-of (xs , ys) → length zs ≤ length (LCS xs ys)

step : ∀ p → (∀ q → q ⊰ p → P q) → P p
step (xs , ys) rec = ?

theorem-2′ : ∀ p → P p
theorem-2′ = ⊰-rec P step

theorem-2 : ∀ xs ys zs → zs is-common-subsequence-of (xs , ys) → length zs ≤ length (LCS xs ys)
theorem-2 xs ys = theorem-2′ (xs , ys)

ここで step の定義の中では、 rec : ∀ q → q ⊰ p → P q を使うことが出来ますが、これは「⊰ の意味で p より小さな任意の q について P q が示せている」という帰納法の前提に対応し、この step が帰納法のステップの実現になっていることがわかると思います。

最終的な証明は少し変更して、以下のようにしました。先程の step から更に zs と zs is-common-subsequence-of (xs , ys) を引数に加えたうえで、パターンマッチによって示しています。

step : ∀ p → (∀ q → q ⊰ p → P q) → P p
step ([]    , _ ) rec .[] (empty , _) = ≤-refl
step (_ ∷ _ , []) rec .[] (_ , empty) = ≤-refl
step (x ∷ xs ,  y ∷ ys) rec zs (zs⊑x∷xs , zs⊑y∷ys ) with x ≟ y
step (x ∷ xs ,  y ∷ ys) rec [] _ | yes _ = z≤n
step (x ∷ xs , .x ∷ ys) rec (.x ∷ zs) (here zs⊑xs  , x∷zs⊑x∷ys  ) | yes refl = s≤s (rec (xs , ys) (⊰-both x xs x ys) zs (zs⊑xs , tail-⊑-tail x∷zs⊑x∷ys))
step (x ∷ xs , .x ∷ ys) rec (.x ∷ zs) (x∷zs⊑x∷xs   , here  zs⊑ys) | yes refl = s≤s (rec (xs , ys) (⊰-both x xs x ys) zs (tail-⊑-tail x∷zs⊑x∷xs , zs⊑ys))
step (x ∷ xs , .x ∷ ys) rec zs        (there zs⊑xs , there zs⊑ys) | yes refl = ≤-step (rec (xs , ys) (⊰-both x xs x ys) zs (zs⊑xs , zs⊑ys))
step (x ∷ xs ,  y ∷ ys) rec [] _ | no _ = z≤n
step (x ∷ xs , .x ∷ ys) rec (.x ∷ zs) (here zs⊑xs , here zs⊑ys) | no x≢x = ⊥-elim (x≢x refl)
step (x ∷ xs ,  y ∷ ys) rec zs (zs⊑x∷xs , there zs⊑ys) | no x≢y =
  begin
    length zs
  ≤⟨ rec (x ∷ xs , ys) (⊰-right (x ∷ xs) y ys) zs (zs⊑x∷xs , zs⊑ys) ⟩
    length (LCS (x ∷ xs) ys)
  ≤⟨ longest-left (LCS (x ∷ xs) ys) (LCS xs (y ∷ ys)) ⟩
    length (longest (LCS (x ∷ xs) ys) (LCS xs (y ∷ ys)))
  ∎
  where open ≤-Reasoning
step (x ∷ xs ,  y ∷ ys) rec zs (there zs⊑xs , zs⊑y∷ys) | no x≢y =
  begin
    length zs
  ≤⟨ rec (xs , y ∷ ys) (⊰-left x xs (y ∷ ys)) zs (zs⊑xs , zs⊑y∷ys) ⟩
    length (LCS xs (y ∷ ys))
  ≤⟨ longest-right (LCS (x ∷ xs) ys) (LCS xs (y ∷ ys)) ⟩
    length (longest (LCS (x ∷ xs) ys) (LCS xs (y ∷ ys)))
  ∎
  where open ≤-Reasoning

前述のように LCS と同じ構造の再帰と zs is-common-subsequence-of (xs , ys) すなわち zs ⊑ xs および zs ⊑ xs の(empty, here, there による)場合分けとなっていて、ちょっと場合分けが複雑ですが、読んでもらえば何をしているかは分かると思います。場合分けはちょっと複雑ですが、すべての場合を網羅していることは Agda がきちんと検査してくれています。

また、帰納法の仮定である rec を呼び出す際には「引数が小さくなっていることの証明」を指定していることがわかります。

場合分けの複雑さに関しては、 x ≡ y の場合と ¬ (x ≡ y) の場合の両方で zs が空の場合を書かなくてはならないなど若干不満はあるのですが、これを解消とすると他の箇所がより複雑になってしまったりしたので、とりあえずこれにしています。より良い方法を知っている方はお知らせいただければ幸いです。

いずれにせよ、これで証明完了です。

まとめ

いかがでしたでしょうか。

Agda は Coq などと比べ発展途上であり、またタクティックによる自動化はあまり行われていない一方で、書かれた証明は関数プログラムとして読むことでができるため、(証明をリプレイしなくても)何をやっているのか証明の構造が分かりやすいという利点があるように思います。また、タクティックによる自動化を追求する代わりに、証明を簡潔かつ読みやすく書くための高レベルなライブラリを整備する方向で発展しているように思います。

これを読んで興味を持たれた方は、是非 Agda で証明やプログラムを書いてみて下さい。そして、来年のTPPmarkにも挑戦してみましょう！