Djinn は定理証明者です。あなたの質問は次のようです: 定理の証明はプログラミングと何の関係がありますか?
厳密に型指定されたプログラミングは、ロジックと非常に密接な関係にあります。特に、ML の伝統における伝統的な関数型言語は、直観主義者の 命題論理と密接に関連しています。
スローガンは「プログラムは証明であり、プログラムが証明する命題はその型である」です。
一般的に考えられるのは
foo :: Foo
と言うように、それfooは式の証明ですFoo。たとえば、タイプ
a -> b
aは からまでの関数に対応するbので、 の証明aと の証明があれa -> bば の証明がありますb。したがって、関数は論理の含意に完全に対応します。同様に
(a,b)
接続詞（論理と）に対応します。したがって、論理トートロジーa -> b -> a & bは Haskell 型に対応し、 a -> b -> (a,b)
次の証明があります。
\a b -> (a,b)
これが「アンド導入ルール」でありながら、「アンド排除ルール」の2つに相当するfst :: (a,b) -> a。snd :: (a,b) -> b
同様にa OR b、Haskell 型に対応しEither a bます。
この対応は、 Haskell CurryとWilliam Alvin Howardにちなんで「Curry-Howard Isomorphism」または「Curry-Howard Correspondence 」と呼ばれることもあります。
この話は、Haskell の非全体性によって複雑になります。
Djinn は「ただの」定理証明者です。
クローンの作成に興味がある場合は、「Simple Theorem Prover」の Google 検索結果の最初のページに、SML で記述されているように見える LK の定理証明の作成について説明して いる論文があります。
編集：「定理はどのように証明できるのですか？」答えは、ある意味では難しいことではないということです。これは単なる検索の問題です。
次のように言い直した問題を考えてみましょう: S を証明する方法を知っている一連の命題と、P を証明したい命題があります。まず最初に、S における P の証明は既にあるのでしょうか? そうであれば、それを使用できます。そうでない場合は、P でパターン マッチを行うことができます。
case P of
(a -> b) -> add a to S, and prove b (-> introduction)
(a ^ b) -> prove a, then prove b (and introduction)
(a v b) -> try to prove a, if that doesn't work prove b (or introduction)
それらのどれも機能しない場合
for each conjunction `a ^ b` in S, add a and b to S (and elimination)
for each disjunction `a v b` in S, try proving `(a -> P) ^ (b -> P)` (or elimination)
for each implication `a -> P` is S, try proving `a` (-> elimination)
本物の定理証明者にはいくらかの頭脳がありますが、考え方は同じです。「意思決定手続き」の研究領域では、機能することが保証されている特定の種類の式の証明を見つけるための戦略を調べます。一方、「タクティクス」では、証明探索を最適に順序付ける方法に注目しています。
について: 「証明を Haskell に変換するにはどうすればよいですか?」
形式システムの各推論規則は単純な Haskell 構造に対応しているため、推論規則のツリーがあれば、対応するプログラムを作成できます。Haskell は結局のところ証明言語です。
含意導入:
\s -> ?
または紹介
Left
Right
そして紹介
\a b -> (a,b)
そして排除
fst
snd
等
augustss は、彼の回答で、彼が Djinn でこれを実装する方法は、SO の回答には少し面倒だと述べています。ただし、自分で実装する方法を理解できると思います。