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

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

例えば、純粋関数型言語Haskellの型はこの直観主義論理の命題と対応しているらしいです（[カリー＝ハワード同型対応](https://ja.wikipedia.org/wiki/%E3%82%AB%E3%83%AA%E3%83%BC%EF%BC%9D%E3%83%8F%E3%83%AF%E3%83%BC%E3%83%89%E5%90%8C%E5%9E%8B%E5%AF%BE%E5%BF%9C)）。

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

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

# クリーネの公理系

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

https://ja.wikipedia.org/wiki/%E5%91%BD%E9%A1%8C%E8%AB%96%E7%90%86#%E5%85%AC%E7%90%86%E7%B3%BB1

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

## THEN-1
$P \rightarrow (Q \rightarrow P)$

一番最初に思いいついた証明はこれでした。
```haskell:例1
then1 :: p -> (q -> p)
then1 p q = p
```

これは```const```そのものでもあります。
```haskell:例2
then1 :: p -> (q -> p)
then1 = const
```

## THEN-2
($P \rightarrow (Q \rightarrow R)) \rightarrow ((P \rightarrow Q) \rightarrow (P \rightarrow R))$

```haskell:例1
then2 :: (p -> (q -> r)) -> ((p -> q) -> (p -> r))
then2 pqr pq p = pqr p (pq p)
```

```((->) p)```がモナドであることに注意すると、これは```ap```そのものです。
```haskell:例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)```を用いることで実現できます。
```haskell:例1
and1 :: (p,q) -> p
and1 (p,q) = p
```

```haskell:例2
and1 :: (p,q) -> p
and1 = fst
```

## AND-2

$P \land Q \to Q$

```haskell:例1
and2 :: (p,q) -> q
and2 (p,q) = q
```

```haskell:例2
and2 :: (p,q) -> q
and2 = snd
```

## AND-3

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

```haskell:例1
and3 :: p -> (q -> (p,q))
and3 p q = (p,q)
```

```haskell:例2
and3 :: p -> (q -> (p,q))
and3 = (,)
```

## OR-1

$P \to (P \lor Q)$

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

```haskell: 例1
type Or = Either
or1 :: p -> Or p q
or1 p = Left p
```

```haskell: 例2
type Or = Either
or1 :: p -> Or p q
or1 = Left
```

## OR-2

$Q \to (P \lor Q)$

```haskell: 例1
type Or = Either
or2 :: q -> Or p q
or2 q = Right q
```

```haskell: 例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))$

```haskell: 例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```の型シノニムとして定義します。

```haskell: 例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)
```

```haskell: 例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)$

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

```haskell: 例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).