朝日ネット 開発者ブログ

朝日ネットのエンジニアによるリレーブログ。今、自分が一番気になるテーマで書きます。

論理式が生成される確率を求める

こんにちは。株式会社朝日ネット開発部の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} となります。

実行例その2

では実際に、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

上記結果より、論理式をランダムに約86億個生成すれば、P\supset Pの証明にたどりつけそうなことがわかりました。 また、パラメータを変更してP\supsetのみが出てくるようにすれば、約13万個の論理式の生成で、証明できそうなことがわかりました。

まとめ

論理式が生成される確率を求める関数を作成し、「論理式をランダムに生成して証明」した場合にいくつぐらいの論理式が必要かを見積もりました。

採用情報

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