haskell-jp / beginners #17 at 2021-08-19 23:29:40 +0900

はじめまして。Haskell歴1ヶ月程度の初心者です。
現在、Haskellの型システムの上で定理証明器を作りたいと考えています。
やりたいことはに似ているのですが、
証明したい命題を型にどう変換して、証明をどう記述すればよいのかわかりません。
例えば、`((P -> Q) -> P) -> P`を証明する場合、Haskellではどのように書くのでしょうか？

その命題にはという名前が付いていて、直観主義論理では証明ができないことが知られています。なので、なんらかの形で “ズル” (再帰) をしないといけません。
あんまり詳しく見れていなくて具体的な回答ではなくて申し訳ないのですが、Logic.Propositional の二重否定除去則の実装の部分のソースなどを覗いてみると、これを使ってできると思います。
https://hackage.haskell.org/package/gdp-0.0.3.0/docs/Logic-Propositional.html#v:contradiction
定理証明支援機を作り始める上では、最初は直観主義の、もうちょっと簡単な命題 P -> P などから作り始めると良いと思います。
これは型 P の変数`x` を引数にとって x を返す関数を定義すれば良いです。

@K.Hirata
ありがとうございます。すみません、例がよくありませんでした。
では、例えばA->((A->B)->B)を証明しようとすると、以下のように一つずつ順に記述していく方法しか思いつかず、また、どこが仮定なのがわかりにくくなっていしまいます。
１行で書くことはできないのでしょうか。

h0 :: (Proof a -> Proof ((a --> b) --> b)) -> Proof (a --> ((a --> b) --> b))
h0 = introImpl

h1 :: (Proof (a --> b) -> Proof b) -> Proof ((a --> b) --> b)
h1 = introImpl

h2 :: Proof a -> Proof (a --> b) -> Proof b
h2 = elimImpl

ケチをつけると、それだと厳密には証明ができたことにはなっていないのではないでしょうか
“p の証明が完了した“、というのは Proof p の型の値が定義できた、ということのはずなので、h0、h1、h2 を更に組み合わせる必要があります。

この下の方が 1 行で書いた証明になっているはずです。(上に書いた simple~~ は証明のイメージです。)
```simpleModusPonens :: a -> (a -> b) -> b
simpleModusPonens x f = f x

myModusPonens :: Proof (a --> (a --> b) --> b)
myModusPonens = introImpl $ \proofA -> introImpl (\proofAtoB -> proofAtoB `modusPonens` proofA)
-- ちょっと短くすると
-- myModusPonens = introImpl $ \proofA -> introImpl (`modusPonens` proofA)```

ようやく理解しました。ありがとうございます。