ブログっ...!

最近はミソフォニアのことばかり書いています。もうミソフォニアブログです。

読んだめも1

よんだはしかたないやつだ!(それは「やんだ」である。。)(よつばとネタ)


callccによる排中律の証明 - sumiiの日記

これ面白かったw
寸劇の話はcallccというワードがヒントになって、わかったw おもしろい。

callccがカリーハワード同型で二重否定に当たる、という話は小耳に挟んだことはあるが、
あんまりよく知らなかった(調べることを忘れていた)ので、調べた。
下のリンクの「call/ccの型」

call/ccと古典論理のカリー・ハワード対応 - 再帰の反復

途中の
λx.(Left x) : A→A∨¬A
のとこで、なんでこうなんだ?と思っていたが、そうだった。
記憶が薄れてて困る。
(下、AgdaのData.Sumリンク。
http://www.cse.chalmers.se/~nad/repos/lib/src/Data/Sum.agda)
(ので、ひとつめのリンク先のInRight(λx:T. k(InLeft x)))は、
InLeft x : T v not T
k(InLeft x) : not
λx:T. k(InLeft x)) : T -> not
となって、InRight(λx:T. k(InLeft x))) : T v not T となるのが解釈。(%s/not/¬/g))
(いっこっつ型を確認する主義)

すごくわかりやすい記事だった...
しっかり理解している方の説明はしゅごいありがたい。

更にこれを読んで、納得してシメ。

http://www.kmonos.net/wlog/61.html#_0538060508

はわわ。。

あと次いでに、voidの話もよんだ。

void - sumiiの日記

Void (コンピュータ) - Wikipedia

あと、前回の記事書いた続きとして、
直観主義論理の話のリンクを超かみつまんで読んだ。

http://www.kurims.kyoto-u.ac.jp/~terui/summer2013.pdf


はっっ、こんなことをしていたらゆうがたに。。じゃあ。。