結局 Coq の講義は履修しないでなんとなく遊ぶことにした. 来年履修するかもしれない, まぁ正直なところ単位はどうでもいい.
しかし Coq, 違うとは聞いていたけど違いすぎてとりあえずビックリしている. いや, そもそも関数型プログラミング言語*1初見の僕だから, Coq 自身というよりもその書き方とか表面的なことに驚いている. この記事では Coq 特有の話は一切しない*2が, サンプルコードは Coq (と C言語) しか出てこない. まぁまだ慣れ始めの段階だということで理解していただきたい.
足し算してみた.
Definition plus n m := n+m. Eval compute in plus 3 4. (* => 7*)
なんて書いてみたりしている*3. 正直これで足す関数が定義できている実感はまるでない. けど抵抗感や嫌悪感はまったくなかったので, もう少し粘って取り組んでみようかと思っている.
気に入ったところ
合成関数がきれいに書けるのはよい.
Definition double := fun x => x + x. Definition quad := fun x => double (double x) Eval compute in double 4 (*=> 8 *) Eval compute in quad 4 (*=> 16*)
同じことを C 言語でやってみると,
#include<stdio.h> int twotimes(int a) { return a + a; } int fourtimes(int a) { return twotimes(twotimes(a)); }
となる. むむむ. できるけど個人的にはあまり気分がよくない. もし 倍でなくても, 一般に
する必要があるなら, たぶんこうする.
(これが最適解だとは思えないが)
int mthtimes(int n, int m) { if (m == 0) return 1; // 0 乗は 1 int i, k; k = n; for (i = 1; i < m; i++) { n = k * n; } return n; }
これで が計算できるはず.
しか考えてないが. 再帰で同じことできないかなー……と考えても浮かばない. 困った. これでは C 言語のほうがサンプルコードが長い.
ということでちょっと頑張って書いてみた. 再帰関数で を計算する:
Fixpoint mthtimes (n m :nat) {struct m} : nat := match m with | 0 => 1 | S m' => n * (mthtimes n m') end.
のときは
を返し,
が
でなければ
倍するというやつ*4.
たぶんこれでいいと思う...
{struct m} が帰納でうごく変数. 実は明示しなくても推測してくれるらしい. スゴイ.
雑感のまとめ
なんか明確にこう違う, とは言えないけどこれだけで今まで僕が見たことのあるプログラミングとは全然違うんだなーって感じがする. どっちが好きともまだ断定できないけれど, 少なくともこの記事を書いていて楽しかったので, Coq の勉強は続けたいと思う.
参考にしたもの
*1:という表現で正しいのだろうか, ていうかそもそも Coq は関数型プログラミング言語であるという認識は間違っていないのだろうか, そこから不安である.
*2:しかし, 私はほかに関数型プログラミング言語を知らないのでこの記述も間違っているかもしれない. まぁないと思うけれど.
*3:はてなは Coq のシンタックスハイライトには対応していないようなので, Ocaml のハイライトを適用しています.
*4:これは C 言語でもかけるなと思ったけどさすがにそれをやると無限ループになるのでやめる.
*5:ネット上に公開されているんだけど微妙に隠されているのでここからリンク貼っていいか微妙なので載せないでおきます.
