日々の流転

λ. Super Mario Hopscotch

ラブ・ファミコン より。ちとはまってしまった。2つ目のステージのパーフェクトを取るのが難しかった。

λ. A206 峠の村

4日目にヤコブが人狼COしてオットーを狂人と言ったのだが、これは変だなぁと思った。仮にオットーが狂人なら、オットーがカタリナに人間判定を出した理由が理解出来ないのだ。狂人オットーはヤコブが最後の人狼だと知っていることになるので、ヤコブが人狼確定してしまうカタリナ人間判定よりも、ヤコブが人狼確定せずに済むカタリナ人狼判定を出すべきだからだ。

• 人狼BBS:A A206 峠の村
• 人狼BBS まとめサイト - A206村

λ. (β→γ)→(α→β)→α→γ

First Steps in Modal Logic について雑談してるときに「(β→γ)→(α→β)→α→γ」をヒルベルト流(ただし論理公理は (s) (α→β→γ)→(α→β)→α→γ と (k) α→β→α のみ)でとっさに証明できなくてちょっと悔しかった。λ式で書くなら λf.λg.λx. f (g x) でおしまいだし、自然演繹やシーケント計算でもそれは同じだけど、ヒルベルト流だとすぐには思いつかんよ。

後でこのλ式をSKIコンビネータの式に機械的に変換してみると「S(S(KS)(S(S(KS)(S(KK)(KS)))(S(S(KS)(S(S(KS)(S(KK)(KS)))(S(S(KS)(S(KK)(KK)))(S(KK)(KS)))))(S(S(KS)(S(S(KS)(S(KK)(KS)))(S(S(KS)(S(KK)(KK)))(S(KK)(KK)))))(S(S(KS)(S(KK)(KK)))(KI))))))(S(S(KS)(S(S(KS)(S(KK)(KS)))(S(S(KS)(S(S(KS)(S(KK)(KS)))(S(S(KS)(S(KK)(KK)))(S(KK)(KS)))))(S(S(KS)(S(S(KS)(S(KK)(KS)))(S(S(KS)(S(KK)(KK)))(S(KK)(KK)))))(S(KK)(KI))))))(S(S(KS)(S(KK)(KK)))(S(KK)(KI))))」になった。もっと短く出来そうではあるけど、流石にこれは思いつけないよなぁ……

というか、アレだ。演繹定理(Deduction Theorem, 「Γ,α⊢β ⇔ Γ⊢α→β」)を使ってしまえば良かったのか。そりゃそうだ。