論理式をランダムに生成する - 朝日ネット　技術者ブログ

こんにちは。株式会社朝日ネット開発部のxfuzzyです。数学や関数型言語に興味があります。前回の記事では、Haskellを使って、論理式を表す型を定義し、ヒルベルト流の推論を定義しました。今回は論理式をランダムに生成する関数を作ってみたいと思います。そのような関数を作ろうとした理由は、ランダムに生成した論理式の中から定理を見つけることができたら面白いのではないかと思ったからです。

概要
Haskellのrandom関数の説明
論理式をランダムに生成する方法
Haskellでの実装
実行例
まとめ
採用情報

概要

Haskellで、乱数を用いて論理式をランダムに生成する方法を紹介します。

Haskellのrandom関数の説明

Haskellでは、ランダムな値を求めるためのrandomという関数があります。この関数はSystem.Randomモジュールをインポートすると使えるようになります。 randomの仕様は、「乱数生成器」を渡すと「ランダムな値と新しい乱数生成器の組」が返されるというものです。以下に例を示します。

$ ghci
GHCi, version 8.0.1: http://www.haskell.org/ghc/  :? for help
Prelude> :m System.Random
Prelude System.Random> gen <- getStdGen  -- 実行するたびに異なる動作をするように時刻などから作った乱数生成器
Prelude System.Random> :t random
random :: (Random a, RandomGen g) => g -> (a, g)
Prelude System.Random> random gen :: (Int, StdGen)  -- Int型の値をランダムに取得する
(7260968050456281749,1017986665 2103410263)  -- ペアの左側がランダムに取得したInt、右側が新しい乱数生成器
Prelude System.Random> random gen :: (Double, StdGen)    -- Double型の値をランダムに取得する
(0.12939106841993697,1017986665 2103410263)  -- ペアの左側がランダムに取得したDouble、右側が新しい乱数生成器

論理式をランダムに生成する方法

上記のrandom関数を参考にして、論理式を生成するrandomProp関数を作ってみたいと思います。また、論理式を生成するためのパラメータを与えられるようにしてみたいと思います。

論理式の生成のために用意するパラメータは次の通りです。

パラメータ	説明
ra	$P$ の確率（Atom "P"と表現するため、aの文字を使っています）
rn	$\neg$ の確率
rc	$\wedge$ の確率
rd	$\vee$ の確率
ri	$\supset$ の確率

このパラメータを使って、ランダムな論理式を生成する関数randomPropを、次のような動作をするように作ります

パラメータで指定した確率にそって「P」「 $\neg$ 」「 $\wedge$ 」等のどれかを選ぶ
Pだった場合はPを返す。
$\neg$ だった場合は、randomProp関数を実行し、その結果に $\neg$ をつけて返す。
$\wedge$ 等だった場合は、randomProp関数を２回実行し、それらの結果を $\wedge$ 等でつなげて返す

Haskellでの実装

まず、論理式生成のパラメータを次のデータ型で表します。

data Param = Param {ra::Integer, rn::Integer, rc::Integer, rd::Integer, ri::Integer}

ランダムな論理式を生成する関数は、以下のようになります。

import qualified System.Random as R
import PropLang
import PropLangOps

data Param = Param {ra::Integer, rn::Integer, rc::Integer, rd::Integer, ri::Integer}

randomProp :: R.RandomGen g => Param -> g -> (PropLang, g)
randomProp p g = case R.randomR (0, sum - 1) g of
    (n, g')
        | n < ra p -> ope0 g' $ Atom "P"
        | n < ra p + rn p -> ope1 g' Not
        | n < ra p + rn p + rc p -> ope2 g' (∧)
        | n < ra p + rn p + rc p + rd p -> ope2 g' (∨)
        | n < ra p + rn p + rc p + rd p + ri p-> ope2 g' (⊃)
    where sum = ra p + rn p + rc p + rd p + ri p
          ope0 g0 c = (c, g0)
          ope1 g0 c = case randomProp p g0 of
                (f, g') -> ope0 g' $ c f
          ope2 g0 c = case randomProp p g0 of
                (f, g') -> ope1 g' $ c f

実行すると以下のようになります。

$ ghci
GHCi, version 8.0.1: http://www.haskell.org/ghc/  :? for help
Prelude> :l PropRandom.hs
[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> gen <- R.getStdGen
*Main> p = Param 3 1 1 1 1
*Main> randomProp p gen
(Atom "P" :∧ (Atom "P" :∧ Atom "P" :⊃ Atom "P"),1410794708 535353314)

ランダムに生成された論理式が表示されました。

実行例

ランダムな論理式を次々に生成できるように、次のrandomList関数を用意して、実行してみたいと思います。

randomList :: R.RandomGen g => (g -> (a,g)) -> g -> [a]
randomList r g0 = case r g0 of
    (n, g1) -> n:randomList r g1

実行例は以下の通りです。パラメータのうち、raを小さくすると論理式が長くなっていくことがわかります。

$ ghci
GHCi, version 8.0.1: http://www.haskell.org/ghc/  :? for help
Prelude> :l PropRandom.hs
[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> gen <- R.getStdGen
*Main> take 10 $ randomList (randomProp (Param 60 10 10 10 10)) gen
[Atom "P",Atom "P",Atom "P",Atom "P" :∧ Atom "P",Atom "P",Atom "P" :∧ Atom "P",Atom "P",N (Atom "P"),Atom "P",Atom "P"]
*Main> take 10 $ randomList (randomProp (Param 50 10 10 10 20)) gen
[Atom "P",Atom "P",Atom "P",Atom "P" :∨ N (Atom "P"),Atom "P" :∨ N (N (Atom "P" :∧ N (Atom "P"))),Atom "P",(Atom "P" :⊃ Atom "P") :∧ Atom "P",Atom "P",Atom "P",Atom "P"]
*Main> take 10 $ randomList (randomProp (Param 45 10 10 10 25)) gen
[Atom "P",Atom "P",Atom "P",Atom "P" :∨ Atom "P" :∧ (Atom "P" :⊃ N (N (Atom "P" :∧ (Atom "P" :∧ Atom "P")))),(Atom "P" :⊃ Atom "P") :∨ N (Atom "P"),Atom "P",Atom "P",Atom "P" :⊃ (Atom "P" :⊃ (Atom "P" :∧ ((Atom "P" :⊃ Atom "P") :∧ N (Atom "P") :∨ Atom "P") :⊃ (Atom "P" :⊃ Atom "P"))),Atom "P" :∧ Atom "P",Atom "P" :∨ Atom "P"]

まとめ

論理式をランダムに生成する関数を実装し、動作を確認しました。

採用情報

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