読んだめも1
よんだはしかたないやつだ!(それは「やんだ」である。。)(よつばとネタ)
これ面白かった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の話もよんだ。
あと、前回の記事書いた続きとして、
直観主義論理の話のリンクを超かみつまんで読んだ。
http://www.kurims.kyoto-u.ac.jp/~terui/summer2013.pdf
はっっ、こんなことをしていたらゆうがたに。。じゃあ。。