論理式が生成される確率を求める - 朝日ネット　技術者ブログ

こんにちは。株式会社朝日ネット開発部のxfuzzyです。数学や関数型言語に興味があります。

前回の記事では論理式をランダムに生成するプログラムを作成してみました。今回は、前回紹介した方法で、特定の論理式が生成される確率を求めるプログラムを作成します。このようなプログラムを作成したのは、「論理式をランダムに生成して、証明をしようとしたときに、目的の結果を得るまでにいくつぐらいの論理式が必要か」を知りたいと思ったからです。

概要
実装
実行例
実行例その２
まとめ
採用情報

概要

論理式を与えて、その論理式が生成される確率を求める関数を作成します。

実装

次のコードは、与えられた論理式の生成される確率を返します。

getProbability :: Param -> PropLang -> Rational
getProbability p f = case f of
    Atom "p" -> (ra p % sum)
    N f1 -> (rn p % sum) * (gpp f1)
    f1 :∧ f2 -> (rc p % sum) * (gpp f1) * (gpp f2)
    f1 :∨ f2 -> (rd p % sum) * (gpp f1) * (gpp f2)
    f1 :⊃ f2 -> (ri p % sum) * (gpp f1) * (gpp f2)
    where sum = ra p + rn p + rc p + rd p + ri p
          gpp = getProbability p

上記において、PropLangは前々回の記事で定義しました。Paramは前回の記事で定義した、論理式をランダムに生成する際に与える、パラメータ（それぞれの記号の出やすさ）になります。また、Rationalは有理数を表す型です。確率の計算なのでDouble等の浮動小数点数型を使ってもよいのですが、ここでは誤差なく計算するために、Rationalを使っています。

実行例

実行例は以下になります。

$ ghci PropRandom.hs
GHCi, version 8.0.1: http://www.haskell.org/ghc/  :? for help
[1 of 3] Compiling PropLang         ( PropLang.hs, interpreted )
[2 of 3] Compiling PropLangOps      ( PropLangOps.hs, interpreted )
[3 of 3] Compiling Main             ( PropRandom.hs, interpreted )
Ok, modules loaded: PropLang, PropLangOps, Main.
*Main> param = Param 4 1 1 1 1
*Main> getProbability param p
1 % 2
*Main> getProbability param $ p ∧ p
1 % 32

論理式に含まれる $P$ や $\wedge$ などの記号の数だけ、対応する確率をかけたものであることがわかります。上記の例では、 $P$ の確率は $\frac{1}{2}$ で、 $\wedge$ の確率は $\frac{1}{8}$ ですので、 $P\wedge P$ の確率は $\frac{1}{2}\times\frac{1}{8}\times\frac{1}{2}=\frac{1}{32}$ となります。

実行例その２

では実際に、 $P\supset P$ の証明をするのに必要な論理式の数（の期待値）を求めてみましょう。

$ ghci PropRandom.hs
GHCi, version 8.0.1: http://www.haskell.org/ghc/  :? for help
[1 of 3] Compiling PropLang         ( PropLang.hs, interpreted )
[2 of 3] Compiling PropLangOps      ( PropLangOps.hs, interpreted )
[3 of 3] Compiling Main             ( PropRandom.hs, interpreted )
Ok, modules loaded: PropLang, PropLangOps, Main.
*Main> ex1 = [(p ⊃ (p ⊃ p) ⊃ p  ) ⊃ (p ⊃ p ⊃ p) ⊃ (p ⊃ p), p ⊃ (p ⊃ p) ⊃ p, (p ⊃ p ⊃ p) ⊃ (p ⊃ p), p ⊃ p ⊃ p, p ⊃ p]
*Main> param = Param 4 1 1 1 1
*Main> fromRational $ sum $ map ((1 /)  . getProbability param) ex1
8.5900744e9
*Main> param = Param 1 0 0 0 1
*Main> fromRational $ sum $ map ((1 /)  . getProbability param) ex1
131752.0