Alloy でクリプキ可能世界意味論！ - これは圏です（はてな使ったら負けだとおもっていた）
Alloy でクリプキの可能世界意味論をエンコードしてみた記録。 論理学をきちんと勉強した訳じゃないので、もし誤りがあったら是非教えてください。 可能世界意味論と云うのは、偉大な論理学者ソール・クリプキが、なんと高校生の頃に思い付いた様相論理の意味論です。 様相論理って云うのは、通常の命題論理に、「□P (必然的に P)」とか「◇P (Pであることが可能)」と云う二つの記号を付け加えて出来る論理体系です。要は可能性を扱う論理学ですね！ ひとくちに様相論理と云っても色々種類があるそうで、「必然的にP なんだったらどう考えてもPだろうよ」「必然的にPであるためにはまずPが可能じゃないといけないんじゃね？」「必然から可能が必然だよな*1！」とかみんな色々な法則を提唱してるんだとか。みんながみんなオレオレ様相論理を作るので、それぞれが一体どういう関係にあるのか？とか、本当にそれで大丈夫なの？とか、
ヒビルテ(2008-10-14)
λ. SmallCheck and Lazy SmallCheck: automatic exhaustive testing for small values SmallCheck and Lazy SmallCheck: automatic exhaustive testing for small values. Colin Runciman, Matthew Naylor and Fredrik Lindblad. in Haskell '08: Proceedings of the first ACM SIGPLAN symposium on Haskell を読んだ。 QuickCheck がランダムテストなのに対して、SmallCheck は指定した上限までの範囲の網羅的な検査を行う*1。 QuickCheckでは値が適切に分散するように値の生成機を書くのは簡単ではないが、Sm
Haskellの文法(再帰編) - あどけない話
構造化定理によれば、分岐、反復、逐次があれば、すべてのロジックは記述できます。分岐については、Haskellの文法(分岐編)で説明しました。今日は反復について説明します。逐次に関しては、少し難しい内容ですが、QAで学ぶMonadを読んで下さい。 for 文 多くの言語では、素朴な繰り返しを実現するためには for 文や while 文を使います。for文を単純に数え上げとして使う場合、カウンターである変数 i が再代入できるとことが前提になっています。 Haskell では、変数に再代入はできません。それは、for 文がないことを意味します。どうやって、繰り返しを実現するのでしょうか？ その答えは、再帰です。 対比するための言語として JavaScript を用いることにします。まず、以下のように渡された整数の配列の要素をすべて足し合わせるプログラムを考えて下さい。 function su
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
処理を実行中です
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
http://blog.ezyang.com/2011/08/8-ways-to-report-errors-in-haskell-revisited/
