トップ «前の日記(2004-11-04) 最新 次の日記(2004-11-06)» 月表示 編集

日々の流転


2004-11-05 [長年日記]

λ. Super Mario Hopscotch

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

λ. A206 峠の村

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

4日目開始段階での可能性
ニコラス
(占い師CO,襲撃された)
ヤコブ
(占い師CO)
ジムゾン
(村人CO,処刑された)
オットー
(霊能者CO)
カタリナ
(霊能者CO,処刑された)
オットーの
カタリナ人間判定
オットーの
カタリナ人狼判定
占い師人狼人狼霊能者狂人
占い師人狼人狼狂人人狼
占い師狂人人狼霊能者人狼
占い師人狼人狼霊能者人狼
狂人占い師人狼霊能者人狼
狂人人狼人狼霊能者
狂人人狼人間人狼人狼
Tags: 人狼

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

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, 「Γ,α⊢β ⇔ Γ⊢α→β」)を使ってしまえば良かったのか。そりゃそうだ。

Tags: 向井研
本日のツッコミ(全2件) [ツッコミを入れる]
ψ 通りすがり (2006-09-03 15:35)

S(KS)K ではだめですか

ψ さかい (2006-09-03 18:07)

もちろんOKです。<br># このときは気づかなかったのですが、これBコンビネータだったんですね。