ものまね鳥をまねる coqで

たぶんすぐ飽きる。というか分からなくなって投げだすと思うが、真似てみる。

この本の9章。

ある森に鳥たちが住んでる。任意の鳥AとBがいるとして、Aに向かってBの名を呼べば、Aは、何かしら鳥の名前を返事として応答する。そのとき返事として応答された鳥の名前をABとする。

ABは、Bの名前を聞いたAの鳥が名づけた鳥の名前ということになる。

各鳥は、鳥の名前を入力にして、別の鳥の名前を返す関数みたいなもの。というかそれそのものである。(鳥とその名前とか、区別する必要すらない感じもするが)

ということで、鳥の定義である。coqで。

Inductive Bird : Type :=
| var_bird (x : nat)
| bird_respond (A B : Bird).

コンビネータ論理パズルの本と書いてあるので、コンビネータの定義をだいたいそのまま
http://shop.comiczin.jp/products/detail.php?product_id=21601
から貰った。

安くて薄い本だが残念ながら中身は理解出来てない。そもそも関係とか推移的閉包とか出てきて読み進めることが出来ない。