継続と反証はカリーハワード対応するか

2984 ワード
論理学 継続 カリーハワード対応 古典論理 哲学 継続 テキストリンク

概要

継続の概念に対応する論理的な概念として反証を想定できるが、対応は限定的になる、というアイデアメモ。

カリーハワード対応

カリーハワード対応というものがある。これは、論理についての概念である証明と、計算機についての概念である式（プログラム）の間にある緊密な対応を指す。

通常、次のような対応関係が念頭に置かれる。

論理 計算機
証明 式
カノニカル証明 値
証明の簡約 式の評価
命題 型
含意命題(AならばBという意味で$A \to B$) 関数型(AからBの関数という意味で$A \to B$)

この対応のおかげで、論理/計算機で成り立つことがらを、概念を交換して計算機/論理で成り立つことがらにできる。例えば、「命題の証明を簡約してカノニカル証明にできる」という論理学的な事実を、「型が付いた式を評価して値にできる」という計算機科学的な事実ともみなせる。

継続の論理的対応物

ところで、計算機科学には継続という概念があるが、これに対応する論理的な概念はないだろうか？

多分自然な候補は反証だと思う。

なぜかというと、継続には普通$\lnot A \equiv A \to \bot$、継続型をつける。ここで登場する$\bot$は、値が存在しない型。

一方、論理的にも反証が示すのは$\lnot A \equiv A \to \bot$、否定の命題である。ここで登場する$\bot$は矛盾を表現し、カノニカル証明が存在しない命題。

よって、さっき紹介した対応を次のように拡張できるように見える。

論理 計算機
証明 式
カノニカル証明 値
証明の簡約 式の評価
命題 型
含意命題(AならばBという意味で$A \to B$) 関数型(AからBの関数という意味で$A \to B$)
反証 継続
否定命題($\lnot A \equiv A \to \bot$) 継続型($\lnot A \equiv A \to \bot$)

本当にそうか？

上記のように反証と継続を対応させる考え方は一定程度うまくいくのだが、型や命題が表現したいことを考えると、不一致が出てくる。

否定命題$A \to \bot$を示す反証は、「入力は$A$のカノニカル証明、出力は$\bot$のカノニカル証明」であるようなものである。

一方、継続型$A \to \bot$で型が付く継続は、「入力は$A$の値、出力は$\bot$の値」であるようなものである。

ただし$\bot$のカノニカル証明/値などというものは定義上存在しない。だから、$A \to \bot$を示す反証/と型がつく継続があっても、こいつが$A$のカノニカル証明/値を受け取って$\bot$のカノニカル証明/値を返すことはない。ここまでは対応している。

違うのはここから。反証の場合、$A \to \bot$を示す反証があっても、こいつが$A$のカノニカル証明を受け取って$\bot$のカノニカル証明を返すことはない。よって、$A \to \bot$を示す反証があるなら、$A$のカノニカル証明は存在しない、と考える（だからこそ$A$の否定になる)。反証にカノニカル証明が与えられることはない。

一方継続の場合はこうなる。$A \to \bot$で型がつく継続があっても、$A$の値を受け取って$\bot$の値を返すことはない。だが$A \to \bot$で型がつく継続に、$A$の値を与えるのはごく普通に発生する事態である。だから継続の場合は、継続に値を与えても、値が返されることがない、と考える。

つまり反証と継続は、同じ「入力$A$、出力$\bot$」ではあるが、表現したいことが微妙に異なる。否定命題は「入力$A$」を排除する命題として意図され、継続型は「出力$\bot$」を排除する型として意図されている。ここにおいて、読み替えは破綻する。

結論+α

型や命題が表現したいことを考えると、継続と反証の対応は崩れる。

そもそも論でいうと、継続を扱うプログラミングでは値を返さず（値を返す以外の作用という意味での）副作用だけを起こす式が登場するが、論理の世界ではカノニカル証明を返さない証明が何者か理解しがたい。ただ、論理の世界における副作用として行為を考えれば、行為に帰結する推論はカノニカル証明を返さない証明なのでは、とか妄想中。