関数型言語でプログラミングできない人が読む「プログラミング Coq」
なにやら日本語で書かれた定理証明支援系言語 Coq の良質なチュートリアルが公開されたとのことで、とりあえず読んでみました。
http://www.iij-ii.co.jp/lab/techdoc/coqt/
定理証明支援系とは何か、 Coq で何ができるのか、という話題についてはここでは触れませんので、興味のある方は検索してみるなり、 Twitter でハッシュタグ #coqt をつけて誰かに聞いてみるのが良いと思います。
さて、公開された最初の記事「http://www.iij-ii.co.jp/lab/techdoc/coqt/coqt1.html」では最初に読者に前提として求める知識についての記述があります。
読者の前提知識としては OCaml や Haskell などの関数型言語でプログラミングできることを想定します。
http://www.iij-ii.co.jp/lab/techdoc/coqt/coqt1.html
ここではこの前提条件を満たさない、つまり関数型言語でのプログラミングができない人がこの記事をどう読んだか、を記そうと思います。なんでそんなことをするかというと、「関数型言語でのプログラミング経験がないけど、この記事に興味を持った」人は少なからずいるのではないかと自分が考えているからです。そういう人の読解の一助になればいいな、というのが動機です。
間違いやおかしいところなどがあれば、指摘いただければありがたいです（って書いとくと id:pi8027 君あたりが大量に指摘くれるはず）。
環境の準備（Windows）
ちょうどこの記事を読んだとき、 Windows を使用していたので、 CoqIDE の Windows 版をインストールしました。このあたりは、元記事を読んでいただければ概ね問題ないと思いますが、 Windows 版の場合、インストールした場所によっては、以下のエラーがでます。
Could not load preferences (Sys_error("C:\\Documents and Settings\\********/.coqiderc: No such file or directory")).このエラーが出た場合は、インストールしたディレクトリにある .coqiderc を "C:\\Documents and Settings\\********" にコピーしてから再度起動すれば上手くいくはずです。
関数の定義
チュートリアルの最初に例示されている関数は以下の形です。
Definition plus (n : nat)(m : nat) : nat := n + m.
これを手続き型っぽく書くと以下のようになると思います（ C 言語っぽく記述してみました）。
int plus(int n, int m) { return n + m; }
上記の2つの plus 関数は、概念はともかく処理の内容は結果的には同じです（ただし、 int が整数型であるのにたいして nat は自然数型なので負の整数を扱えるかどうかの違いや扱える数の大きさの違いがある）。それぞれ、以下のように対応します。
| Coq | C | 説明 |
|---|---|---|
| (n : nat) | int n | 第1引数 |
| (m : nat) | int m | 第2引数 |
| plus ... : nat | int plus(...) | 戻り値が nat / int の関数 plus |
| := n + m | return n + m; | 第1引数と第2引数の和を返す |
無名関数
チュートリアルでは、無名関数としての実装例も記されています。
Definition plus' : nat -> nat -> nat := fun n m => n + m.
まず、関数名の直後に nat が3つ並んでいますが、1つ目から順に、「第1引数の型」「第2引数の型」「戻り値の型」を指しています。
次に、 fun の後の n m ですが、これはそれぞれ第1引数、第2引数を指します。最後の n + m は関数の行う処理ですね。
後半で提示されるサンプルコードを見ると無名関数での実装例が多いので、この形を理解できるかどうかが、このチュートリアルを理解できるかどうかの重要な分かれ目だと思います。
forall
次のサンプルコードの無名関数版では、全量化子 forall なるものがでてきます。これは、数学記号の∀（全ての）のことだと思います。例では引数 A にたいして「全ての」とつけていますが、 forall の他にどんなものがここに入るのかは知らないので、予約されていない型を用いる場合には基本的につけるものなのかな、という認識でいます（予約語を見る限り、 forall の他には exists とかが入りそうですね）。
アリストテレスの三段論法
1つ目の証明を飛ばして、いきなり2つ目の証明にうつります。ここで例示されているコードの解釈で詰まった人がいるのではないかと思うので、自分なりの解釈を書きます。
Definition prop1 : forall (A B C : Prop), (B -> C) -> (A -> B) -> (A -> C) := fun A B C f g x => f (g x).
"forall (A B C : Prop), (B -> C) -> (A -> B) -> (A -> C)" までは問題ないかと思います。『全ての「命題を表す型」A、B、C にたいして、「BならばC」ならば「AならばB」ならば「AならばC」』という型の関数を書きますよ、ということですね。ここまではチュートリアルの説明どおりの認識です。
問題は、その関数の実装である "fun A B C f g x => f (g x)" の部分です。A、B、Cはともかく、f、g、xとはなんなのか。それがわからないと "f (g x)" の意味がわからないと思います。
ここで、かなり前に説明した plus の無名関数を思い出してみましょう。
Definition plus' : nat -> nat -> nat := fun n m => n + m.
この plus' 関数と prop1 関数をパーツごとに比較してみます。
| plus' | prop1 |
|---|---|
| fun n m | fun A B C f g x |
| nat -> nat -> nat | (B -> C) -> (A -> B) -> (A -> C) |
plus' 関数では引数 n、m の型はどちらも nat でした。では、 f、g、x の型は何になるでしょうか。最後の (A -> C) が戻り値の型だとすると、引数3つに対して型が (B -> C) と (A -> B) の2つになってしまいますね。引数の型をわかりやすく理解するために、該当箇所の表記を変えてみます。
| plus' | prop1 |
|---|---|
| fun n m | fun A B C f g x |
| nat -> nat -> nat | (B -> C) -> (A -> B) -> A -> C |
この形だと、3つの引数の型がわかりやすいと思います。つまり、 f の型は (B -> C) 、 g の型は (A -> B) 、 x の型は A です。そして、この3つの引数で表現される式 f (g x) の型は戻り値の型 C になることがわかります。
手続き型っぽく書くと、
C f(B){}; // 型 B の引数をとって型 C の値を返す関数 f
B g(A){}; // 型 A の引数をとって型 B の値を返す関数 g
C prop1(A x)
{
B temp1 = g(x);
C temp2 = f(temp1);
return temp2;
}
という感じでしょうか。
