命題論理のヒルベルト流をHaskellで実装する - 朝日ネット　技術者ブログ

こんにちは。株式会社朝日ネット開発部のxfuzzyです。数学や関数型言語に興味があります。 Haskellという言語に、興味はあるのですが、プログラムを作ったことはほぼありませんでした。そのため、Haskellを実際に使って学習をしつつプログラムを作ってみたいと思っていました。また、数学に興味がありながら、計算をするのは苦手でした。特に、論理式の変形は、ルールは単純なのですが、長い式が出てくると、手計算ではミスが発生して残念だと思っていました。そこで私は、Haskellを使って、論理式の操作をするプログラムを作ってみることにしました。

概要
背景の説明
プログラムの説明と実行例
まとめ
採用情報

概要

命題論理の体系のひとつ「ヒルベルト流」を実装しました。論理式を表すデータ型と、ヒルベルト流に基づいて推論を行うロジックを作成しました。ソースは以下にあります。

https://github.com/xyzfuzzy/hilbert

背景の説明

命題論理とヒルベルト流について、次の書籍を参考にして、解説します。

論理と計算のしくみ - 岩波書店

論理式とトートロジー

本記事における論理式は次のように構成されます。

$P$ や $Q$ などの変数は論理式
$\phi$ を論理式として $\neg\phi$ は論理式
$\phi$ と $\psi$ を論理式として、 $\phi\wedge\psi$ 、 $\phi\vee\psi$ 、 $\phi\supset\psi$ は論理式（それぞれ「かつ」「または」「ならば」の意味）
上記で構成できるもののみが論理式

記法として、 $\supset$ は右結合とします。つまり $P\supset (Q\supset R)$ の括弧は省略して $P\supset Q \supset R$ と書くことにします。

論理式の中でも $P\supset P$ のように、変数の値によらず真となる論理式をトートロジーと呼びます。

ヒルベルト流

トートロジーを導く方法のひとつに、「ヒルベルト流」があります。以下の方法で導ける論理式をヒルベルト流で導いた定理とします。

下記のいずれかの形の論理式（公理）は、定理である
1. $P\supset Q \supset P$
2. $(P\supset Q \supset R) \supset (P\supset Q) \supset P\supset R$
3. $P\supset Q\supset P\wedge Q$
4. $P\wedge Q\supset P$
5. $P\wedge Q\supset Q$
6. $P\supset P\vee Q$
7. $Q\supset P\vee Q$
8. $(P\supset R)\supset (Q\supset R)\supset P\vee Q \supset R$
9. $(\neg P\supset \neg Q)\supset Q\supset P$
$P$ と $P\supset Q$ が定理ならば、 $Q$ は定理である
上記のみが定理である

ヒルベルト流の例

ヒルベルト流で推論する例を紹介します。

$P\supset P$ という定理の証明をする際は、次のステップで推論を行います。

2番目の公理¹において、 $Q$ として $P\supset P$ を、 $R$ として $P$ をとると、 $(P\supset (P\supset P) \supset P) \supset (P\supset P\supset P) \supset P\supset P$ になるので、この論理式は定理である。
1番目の公理²において、 $Q$ として $P\supset P$ をとると $P\supset (P\supset P) \supset P$ になるので、この論理式は定理である。
1.の論理式³は「(2.の論理式⁴) $\supset\sim$ 」という形をしているので、 $\sim$ の部分である $(P\supset P\supset P) \supset P\supset P$ は定理である。
1番目の公理⁵において、 $Q$ として $P$ をとると $P\supset P \supset P$ になるので、この論理式は定理である。
3.の論理式⁶は「(4.の論理式⁷) $\supset\sim$ 」という形をしているので、 $\sim$ の部分である $P\supset P$ は定理である。

以上のステップで $P\supset P$ が定理であることが証明できました。簡単そうな証明にも複雑な論理式の操作が出てきました。

プログラムの説明と実行例

プログラムでは、次のことをしています。

論理式のデータ型の定義
定理のリストを与えて、ある論理式が定理かどうか判定する

以下、Haskellの対話環境であるGHCiでプログラムを実行した際の実行例を紹介します。次のようにしてGHCiを起動しておきます。

$ ghci
GHCi, version 8.0.1: http://www.haskell.org/ghc/  :? for help
Prelude> :set -XOverloadedStrings

論理式のデータ型

PropLangというデータ型で論理式を表します。⁸

data PropLang
    = Atom String
    | Not PropLang
    | PropLang :∧ PropLang
    | PropLang :∨  PropLang
    | PropLang :⊃ PropLang
    deriving (Eq, Show, Read)

PropLangを読み込んで、使ってみましょう。

Prelude> :load PropLang.hs
[1 of 1] Compiling PropLang         ( PropLang.hs, interpreted )
Ok, modules loaded: PropLang.
*PropLang> "p" :∧ "q"
Atom "p" :∧ Atom "q"
*PropLang> pq = "p" :∧ "q"
*PropLang> qp = "q" :∧ "p"
*PropLang> pqqp = pq :⊃ qp
*PropLang> pqqp
Atom "p" :∧ Atom "q" :⊃ Atom "q" :∧ Atom "p"

match関数

matchという関数で、ある論理式が特定のパターンになっているかを判定します。

次の実行例では、「 $a\supset b$ というパターンに $p\wedge q\supset q\wedge p$ という式は当てはまるか？」を判定しています。結果は「 $a$ として $p\wedge q$ 、 $b$ として $q\wedge p$ をとれば当てはまる」というものです。

*PropLang> match ("a" :⊃ "b") pqqp
fromList [("a",Atom "p" :∧ Atom "q"),("b",Atom "q" :∧ Atom "p")]

次の実行例のように、パターンに当てはまらない場合、fromList []という値を返します。

*PropLang> match ("a" :⊃ "a") pqqp
fromList []

このような関数を定義したのは、ある論理式が、ヒルベルト流の公理に当てはまるかどうかを判定するためです。

論理式を書きやすくする

PropLangでは「∧」や「∨」にコロンをつける必要があり面倒だと思ったので、記述を少し楽にするモジュールPropLangOpsも作成しました。 PropLangOpsのもとでは、以下のように、論理式の入力時に「∧」や「∨」にコロンをつけなくてもOKです。

*PropLang> :load PropLangOps.hs
[1 of 2] Compiling PropLang         ( PropLang.hs, interpreted )
[2 of 2] Compiling PropLangOps      ( PropLangOps.hs, interpreted )
Ok, modules loaded: PropLang, PropLangOps.
*PropLangOps> match (p ⊃ q) (p∧q ⊃ q∧p)
fromList [("p",Atom "p" :∧ Atom "q"),("q",Atom "q" :∧ Atom "p")]

ヒルベルト流の推論を行う

ヒルベルト流の推論を行う関数がinferです。

infer :: [PropLang] -> PropLang -> Maybe InferDetail

第１引数として今までにある定理のリストを指定し、第２引数としてこれから推論したい論理式を指定します。第２引数の論理式が推論できる場合は、Justとなります。推論できない場合は、Nothingとなります。

*PropLangOps> :load Hilbert.hs
[1 of 3] Compiling PropLang         ( PropLang.hs, interpreted )
[2 of 3] Compiling PropLangOps      ( PropLangOps.hs, interpreted )
[3 of 3] Compiling Hilbert          ( Hilbert.hs, interpreted )
Ok, modules loaded: PropLang, PropLangOps, Hilbert.
*Hilbert> infer [] (p⊃p⊃p)
Just (Axiom (Atom "p" :⊃ (Atom "q" :⊃ Atom "p")) (fromList [("p",Atom "p"),("q",Atom "p")]))
*Hilbert> infer [p, p⊃q] q
Just (MP (Atom "p" :⊃ Atom "q"))
*Hilbert> infer [p, p⊃q] p
Nothing

上記において、Axiomはヒルベルト流の1.の方法で導かれたということ、MP（modus ponensの略）はヒルベルト流の2.の方法で導かれたということを表しています。

まとめ

Haskellにて、次のものを実装しました。

論理式のデータ構造
今までにあった定理をもとに、ある論理式が定理かどうか判定するロジック

私にとっては、Haskellに慣れて、理解を深めることができました。また、数学の学習の側面では、プログラムを書いていろいろ動かしたことで命題論理の理解が深まったと思います。今後は、証明の探索を行うなどのプログラムを作ってみたいと思いました。

採用情報

朝日ネットでは新卒採用・キャリア採用を行っております。

$(P\supset Q \supset R) \supset (P\supset Q) \supset P\supset R$ ↩
$P\supset Q \supset P$ ↩
$(P\supset (P\supset P) \supset P) \supset (P\supset P\supset P) \supset P\supset P$ ↩
$P\supset (P\supset P) \supset P$ ↩
$P\supset Q \supset P$ ↩
$(P\supset P\supset P) \supset P\supset P$ ↩
$P\supset P \supset P$ ↩
この宣言の中では中置記法にするために:を使っています。Haskellでは、コンストラクタの名前を:で始めることで中置記法にすることができます。↩