gotoとカリーハワードと限定継続と排中律
-
- いいね！0
Yusuke Matsushita
@shiatsumat
@stibear1996 @___yuni @__int 「gotoが排中律に対応する」というのはカリーハワード対応の話とは少し違う言いかたなのでよくわからない。とりあえずカリーハワード対応はふつうのプログラミングにおいてはそこまで気にしなくていいような気がする。
2013-10-05 13:22:24
Yusuke Matsushita
@shiatsumat
@stibear1996 @___yuni @__int プログラミングにおいて「がちの記号論理学」は必要ないと思うけど、純粋に論理学というものに興味があって、論理学に触れてみたいならば、野矢茂樹「論理学」か、戸田山和久「論理学をつくる」がいいと思う。どちらも学校図書館にある。
2013-10-05 13:40:34
わさびず
@___yuni
@shiatsumat @stibear1996 @__int gotoの話は間違っていたのをあとから気づいたのであれだけど、プロシージャ間ジャンプがあればカリーハワード同型対応で排中立に相当する型を持つ関数が作れる(正確にいうとPeirce's law)
2013-10-05 14:01:10
Yusuke Matsushita
@shiatsumat
@___yuni @stibear1996 @__int やっぱりカリーハワード対応の話だったんですね。ささいなことについていろいろ言ってしまってすみません。
2013-10-05 14:08:33
わさびず
@___yuni
@qnighy rubyはブロックの中にreturnを書くとメソッドへのリターンになるよね、それが今僕がプロシージャ間ジャンプと呼んでいるものなんだけど、rubyを出したのは単にプロシージャ間ジャンプがあって知名度があるからで、そういう意味ではscalaで話を進めたほうがいいかも
2013-10-05 14:25:11
わさびず
@___yuni
@qnighy scalaはrubyみたいなreturnを持っていて、それを使うと型レベルで排中律が示せるという話。限定継続があれば同じことが可能というのは納得だけどreturnでもそれができるというのが面白くて僕はそれがどの程度”弱い”構文でも可能なのかにとても興味がある
2013-10-05 14:34:35
わさびず
@___yuni
@qnighy resetは継続に特殊なマーキング(shiftからは見えるが他のいかなるオペレータからは無視される)を施すので、resetの中でshiftが呼ばれないという条件で全く同じ
2013-10-05 14:41:37
Yusuke Matsushita
@shiatsumat
@functional_yy 確かに証明可能ですね。(A→B)∨(B→A)が古典論理だと恒真なんですね。ご指摘ありがとうございます。
2013-10-05 14:58:54
Masaki Hara
@qnighy
@___yuni ようやく理解しました。def..return..endはcall/ccの制限された形なんですね。具体的には、関数終了後にreturnが呼ばれたときに復帰できずにエラーになる。
2013-10-05 15:37:32
Masaki Hara
@qnighy
@___yuni 実際、Rubyのdef..return..endで排中律に相当するコードを書くと def em Right.new (lambda {|p| return (Left.new p) }) end となって、このreturnは呼ばれたら確実に失敗すると。
2013-10-05 15:38:34
Masaki Hara
@qnighy
@___yuni この制限によって、call/ccにありがちな非直感的な挙動は起きない。つまり、def..return..endのやっている事は、その操作的意味論の違いを除けば、call/ccと同様だと考えて良さそうですね。
2013-10-05 15:42:51
わさびず
@___yuni
@qnighy 全くその通りでその内側のproc(lambdaではなくprocですね)の型はP -> _|_と型付けすることができます。NonLocalJumpに限らず例外でもおなじものが作れます。
2013-10-05 15:51:41
Masaki Hara
@qnighy
callcc (λc. ... (c x) ... ) のc xが評価対象になったら、この項全体をx[c:=error] で置き換える callcc (λc. x) のxがもはや評価できなくなったら、この項全体をx[c:=error] で置き換える
2013-10-05 15:52:55