Haskellメモ 直観主義論理との対応

ざっくりといいますが、「古典論理（普通の論理）」から「排中律（$P \lor \neg P$）」を除いたものを直観主義論理と呼びます。
このような論理の体系を考える意義として、プログラムの型との対応関係が挙げられます¹。」

例えば、純粋関数型言語Haskellの型はこの直観主義論理の命題と対応しているらしいです（カリー＝ハワード同型対応）。

また、関数f: p -> qは命題$P \rightarrow Q$の証明に対応しているようです。

実際に具体例を考えて、このことを確かめてみたいと思います。

クリーネの公理系

Wikipediaにクリーネの公理系というものが載っています。具体例がたくさんあって良さそうなので、これで考えてみようと思います。

ここに載っている命題をHaskellに書き直してみます。
Haskell初心者の方（私含め）には良い練習となるのではないかと思います。

THEN-1

$P \rightarrow (Q \rightarrow P)$

一番最初に思いいついた証明はこれでした。

例1

then1 :: p -> (q -> p)
then1 p q = p

これはconstそのものでもあります。

例2

then1 :: p -> (q -> p)
then1 = const

THEN-2

($P \rightarrow (Q \rightarrow R)) \rightarrow ((P \rightarrow Q) \rightarrow (P \rightarrow R))$

例1

then2 :: (p -> (q -> r)) -> ((p -> q) -> (p -> r))
then2 pqr pq p = pqr p (pq p)

((->) p)がモナドであることに注意すると、これはapそのものです。

例2

import Control.Monad
then2 :: (p -> (q -> r)) -> ((p -> q) -> (p -> r))
then2 = ap

AND-1

$P \land Q \to P$
論理積（$P \land Q$）はタプル(p,q)を用いることで実現できます。

例1

and1 :: (p,q) -> p
and1 (p,q) = p

例2

and1 :: (p,q) -> p
and1 = fst

AND-2

$P \land Q \to Q$

例1

and2 :: (p,q) -> q
and2 (p,q) = q

例2

and2 :: (p,q) -> q
and2 = snd

AND-3

$P \to (Q \to (P \land Q))$

例1

and3 :: p -> (q -> (p,q))
and3 p q = (p,q)

例2

and3 :: p -> (q -> (p,q))
and3 = (,)

OR-1

$P \to (P \lor Q)$

論理和（$P \lor Q$）はEither p q型を用いることで実装できます。EitherにOrという別名を付けておきます。

例1

type Or = Either
or1 :: p -> Or p q
or1 p = Left p

例2

type Or = Either
or1 :: p -> Or p q
or1 = Left

OR-2

$Q \to (P \lor Q)$

例1

type Or = Either
or2 :: q -> Or p q
or2 q = Right q

例2

type Or = Either
or2 :: q -> Or p q
or2 = Right

OR-3

$(P \to R) \to ((Q \to R) \to (P \lor Q \to R))$

例1

type Or = Either
or3 :: (p -> r) -> ((q -> r) -> Or p q -> r)
or3 pr qr (Left p) = pr p
or3 pr qr (Right q) = qr q

NOT-1

$(P \to Q) \to ((P \to \neg Q) \to \neg P)$

矛盾に対応するのが値を持たない型で、Haskellではdata Bottomと宣言することで定義できるようです。
そして、$\neg P$はp -> Bottomの型シノニムとして定義します。

例1

data Bottom
type Not p = p -> Bottom
not1 :: (p -> q) -> ((p -> Not q) -> Not p)
not1 p_q p_notq p = (p_notq p) (p_q p)

例2

import Control.Monad
data Bottom
type Not p = p -> Bottom
not1 :: (p -> q) -> ((p -> Not q) -> Not p)
not1 = flip ap

NOT-2

$P \to (\neg P \to Q)$

爆発律です。これはよく分かりませんでした。
一応以下のようにすれば実装はできますが……。

例1

data Bottom
type Not p = p -> Bottom
not2 :: p -> (Not p -> q)
not2 p not_p = absurd (not_p p)

absurd :: Bottom -> q
absurd _ = undefined

これまでundefinedのことをあまり知らなかったのですが、undefinedは任意の型に含まれるようなので、Bottomは本当の意味での矛盾とは異なるようです。
ここは勉強中なのでよく分かっていませんが、Haskellと直観主義論理は完全に対応するわけではないようですね。

NOT-3

$P \lor \neg P$

排中律です。直観主義論理ではこの排中律を認めません。
undefinedを使えば実装すること自体はできてしまいますが、undefined（または他の同様の関数）の使用を禁止すれば、実装できないということだと思います。

まとめ

具体例をいくつか見ることで、Haskellと命題論理の関連性が少し分かった気がします。
一方で、undefinedについては謎が深まりました。
また、今回は命題論理について考えましたが、述語論理の場合も気になります。
今後も少しずつ勉強を進めていこうと思います。

参考

• "Haskellの型と直観論理". 朝日ネット　技術者ブログ. 2019-10-31. https://techblog.asahi-net.co.jp/entry/2019/10/31/125852, (参照 2024-07-28)
• "Haskell/カリー=ハワード同型". ウィキブックス. 2014-04-25. https://ja.wikibooks.org/wiki/Haskell/%E3%82%AB%E3%83%AA%E3%83%BC%3D%E3%83%8F%E3%83%AF%E3%83%BC%E3%83%89%E5%90%8C%E5%9E%8B, (参照 2024-07-28).
• "Curry-Howard の対応". 筑波大学. 2013. https://www.cs.tsukuba.ac.jp/~kam/lecture/complogic2013/slide2013.pdf, (参照 2024-07-28).

1. 古典論理と対応するものもあるようですが、私はよく分かっていません ↩