正しくは、こうであった。 Axiom bird_composition : forall A B : Bird, exists C : Bird, forall x : Bird, bird_respond C x = bird_respond A (bird_respond B x).Coqで証明出来るということから逆算した正しさに過ぎないけどな!しかし、世の数学の偉い…

この森の任意の鳥A,Bに対して、任意の鳥xを取れば、Cx = A(Bx)となるような鳥Cがいる。 任意の鳥A,Bに対して,AとBを結合する鳥Cが存在する。 Axiom bird_composition : forall A B : Bird, exists C : Bird, forall x : Bird, bird_respond C x = bird_respo…

ものまね鳥は任意の鳥xに対して、次の条件が成り立つような鳥Mのことである。Mx = xxMに対してxと呼んでも、xに対しxと呼んでも同じ応答が得られる。そうな。 Axiom there_is_mockingbird : exists M, forall x, bird_respond x x = bird_respond M x.疲れた…

たぶんすぐ飽きる。というか分からなくなって投げだすと思うが、真似てみる。この本の9章。 ある森に鳥たちが住んでる。任意の鳥AとBがいるとして、Aに向かってBの名を呼べば、Aは、何かしら鳥の名前を返事として応答する。そのとき返事として応答された鳥の…