無限リストと証明じゃないCoqの話

プログラミング

Haskellではじめて無限リストのコードを見たときはとても驚いた。遅延評価など知らないから、どうみても無限ループに陥りそうなプログラムがちゃんと動いているのが不思議だった。

無限に続くデータさえ表現できる遅延データ構造はとても強力だ。大量のデータを扱う場合でも、関数を合成していって（あるいはメソッドチェーンで）簡単に処理が書ける。遅延リストがあるのはHaskellだけじゃなくて、Ruby 2.0でもEnumerableにlazyメソッドが来るそうだし、自分もMoonScript上で遅延リストを実装してみたのだけれども、遅延データ構造がデフォルトのHaskellでは様々なデータ構造が同様に遅延評価される。

プログラミング言語を作るとしたら、無限リストは絶対に標準機能にしたいと思った。

一方で悪いこともあって、Haskellのリストは有限で終わるのか、それとも無限に続くのかが分からない。無限のリストに対してsumとかしたら、ひょっとしたら値が返ってこないかもしれない。無限ループバグはHaskellの検査では検出できないから、非正格な関数があるとはいえ、結局は⊥ができないように気をつけながらプログラミングをしなければならない。

そんなことを考えていたら、思い出した。そうか、Coqを使えばいいんだ。

Coqは定理証明のイメージが強いけど、それ自体強力なプログラミング言語らしい。友人もよくHaskellなんかじゃなくてCoq使えばいいのにみたいなことを言っていたのだけれども、証明が必要なプログラムを書く予定はなかったから、あまり考えていなかった。けど、今考えていることはまさにCoqが解決していることなんだ。

Coqは停止する。なぜ停止するかと言えば、Coqが扱うデータは必ず構成的だからだ。停止する関数に、帰納的なデータ。それらを停止することが証明されている方法で組み合わせてプログラムを作れば、停止するに決まっている。

早速Coqで無限リストを構成的に作ってみようと思い、インストールしたまま放っておいたCoq IDEを起動した。無限リストの構成方法のアイディアはMoonScriptで無限リストを実装した時と同じだ。先頭のデータと、イテレーターのペアで表現できる。プログラミングCoqを見ながらコードを書いた。

Inductive Stream (A : Type) :=
  | iterate : (A -> A) -> A -> Stream A.

これはちゃんとCoqをパスした……のだけれども、これだとiterateでしか無限ストリームを作成できない。じゃあ、こうしたらどうかな。

Inductive Stream (A B : Type) :=
  | unfold : (B -> A) -> B -> Stream A B.

これも通ったけど、無限リストにしたいAとは関係ない型Bが定義に入っている。どうしよう。

ひょっとして、標準ライブラリに既にあるのでは?




Standard Library | The Coq Proof Assistant

定義をみてみる。

Section Streams.

Variable A : Type.

CoInductive Stream : Type :=
    Cons : A -> Stream -> Stream.

CoInductive…… あー、なるほど。帰納じゃなくて余帰納で定義するのか。余帰納が何かはよく知らないけど。あとSectionを使うことでAを関数定義の外側に括り出せるのね。


帰納的なデータ構造では何もない所から少しずつ大きなデータ構造を作っていく。どんなに大きくなっても有限だから、データを分解していけばいつかはベースに到達する。一方、余帰納的なデータ構造は、分解していっても終点がない（かもしれない）データ構造として定義されている。

とにかく、Haskellで遅延データ構造を使って表現するような、無限につづくデータは余帰納で定義できることが分かった。停止しなければいけないCoqは無限に続くデータを扱えないのではないかとかなんとなく思っていたのだけれども、完全に誤解だった。

ライブラリの定義を参考にしつつ、iterateとtakeを定義してみた。

Require Import List.
Require Import Coq.Lists.Streams.

Section Generate_Stream.
  Variable A : Type.

  CoFixpoint iterate (f : A -> A) (x : A) : Stream A :=
    Cons x (iterate f (f x)).

  Fixpoint take (n : nat) (s : Stream A) : list A :=
    match n with
      | O => nil
      | S n1 => (hd s) :: take n1 (tl s)
    end.
End Generate_Stream.

CoFixpointで定義した関数をExtractionでOCamlに変換すると、ちゃんとlazyで表現されていることがわかる。

(** val iterate : ('a1 -> 'a1) -> 'a1 -> 'a1 stream **)

let rec iterate f x =
  lazy (Cons (x, (iterate f (f x))))