排中律やPeirce's lawの挙動 - chiguriの生態（嘘や誇張アリ）
これは、Theorem Proving Advent Calendarの四日目の記事である。 ぱっと見ではあまりTheorem Provingらしくないかと思われるかもしれないが、たまにはこういう話もよいだろう、ということで。 お題 今回使う道具は、Curry-Howard同型対応、直観主義で失われる二重否定除去、そして栄光のcall/cc*1である。 ただ、これらの背景を説明すると滅茶苦茶に長くなるので、あとで解説用のスライドを作成しようと思う。 今回はこれらがわかっている前提で話を進める。 着眼点1：二重否定除去以外の規則群 直観主義論理と二重否定除去の組み合わせは古典論理と同じ計算能力を有する。 つまり、二重否定除去をつけると「直観主義論理で証明できなかったもの（のうち古典論理で正しいもの）が証明できる」こととなる。 また、同時にこれは逆が言える場合もあり、その規則を直観主義論理に付
Practical Foundations for Programming Languages
Practical Foundations for Programming Languages Robert Harper Carnegie Mellon University Spring, 2011 [Version 1.8 of 07.22.2011.] Copyright c 2010 by Robert Harper. All Rights Reserved. The electronic version of this work is licensed under the Cre- ative Commons Attribution-Noncommercial-No Derivative Works 3.0 United States License. To view a copy of this license, visit http://creativecommons.o
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
http://pllab.is.ocha.ac.jp/~asai/cw2011tutorial/main-j.pdf
CiteSeerX
https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.26.6893&rep=rep1&type=pdf
Contrasting Exceptions and Continuations
fam.cx
8.4 対応関係の拡張