P102の 20 コマドリで書かれている、ルリムクドリという鳥は、ルリツグミの間違い？ルリムクドリなんて出てこないよな？

タイトルの横に書いてある、POD版の意味を最近ようやく知った。 注文してから一部ずつ刷ってんのね。最後の一冊でラッキーとか書いてはずかしー。

Pである鳥 Aがいて、Qである鳥 Bがいる場合 Xである鳥がいることを示せ。みたいな問題で、 (exists A, P A) -> (exists B, Q B) -> exists C, X C.のように立式してたけど、 forall A B, P A -> Q B -> exists C, X C.でいいのか？ 証明も少し楽だ。 destruc…

そういや、: の左は、値。右は型。だった。 あるいは、: の左は証明。右は命題。 あるいは、: の左は命題。 右は命題型。つまり、 なんらかの命題 : Prop右に命題を書いてしまえば、左はその証明を用意しなくちゃならない。

Aに向ってBと呼びかければ、Aは同じ鳥Bの名を呼びもどすかもしれない。 その場合、鳥Aは鳥Bが好きであるという。 記号だと、AB = Bあらゆる鳥はすくなくとも一羽の鳥が好き。coqで。 Theorem any_bird_is_fond_of_least_one_bird : forall A, exists B, B = …

ひいた。正月そうそう縁起が悪い。

鳥xは自分自身が好きであれば、すなわちxのxへの応答がxであれば、自己中心的と呼ばれる。 記号的には、xx = x である。結合条件とものまね鳥がいる条件のもとで、少なくとも一羽の鳥は自己中心的であることを示せ。coqで。とりあえず。 Theorem there_is_eg…

正しくは、こうであった。 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は、何かしら鳥の名前を返事として応答する。そのとき返事として応答された鳥の…

#coq 去年末、スマリヤンのコンビネータ論理を使ったパズル本を手に入れて、これcoqで出来るんかもかもと試してみた。 出来んかった・・・本の回答だと、 forall x : Bird, exists C : Bird, bird_respond C x = bird_respond A (bird_respond M x)で xにCを…