日々の流転

λ. Alloyでラクトース代謝モデル (AlloyでALP?)

先日、Alloyで知識論理を使って論理パズルを解くで Alloy Analyzer を使ってみて面白かったので、また遊んでみた。 今回の題材は“ProLogICA: a practical system for Abductive Logic Programming”(20080128#p01)に載っていた、大腸菌 E. Coli*1 のラクトース代謝モデルと、それを用いた発想推論。

まず、Alloyによる記述は以下のようになる。

-- 遺伝子 (ラクトースオペロン)
abstract sig Gene { }
abstract sig LactoseOperon extends Gene {
   code : set Enzyme, -- コード化している酵素
}
one sig lacY extends LactoseOperon { }
one sig lacZ extends LactoseOperon { }
fact {
   lacY.code = Permease
   lacZ.code = Galactosidase
}

-- 酵素
abstract sig Enzyme { }
one sig Permease extends Enzyme { }
one sig Galactosidase extends Enzyme { }

-- 糖
abstract sig Sugar {
   amount : lone Amount, -- 現在存在する量
}
one sig Glucose extends Sugar { } -- グルコース
one sig Lactose extends Sugar { } -- ラクトース

-- 量
abstract sig Amount { }
one sig Low extends Amount { }
one sig Medium extends Amount { }
one sig Hi extends Amount { }

-- 大腸菌 E. Coli
one sig EColi {
   feed : set Sugar,   -- 食べている糖
   make : set Enzyme,  -- 作られている酵素
   express : set Gene, -- 発現している遺伝子
}

fact {
   -- ラクトースオペロンはラクトースが存在しグルコースが不足したとき発現
   all g : LactoseOperon |
     g in EColi.express iff
       (Glucose.amount=Low && Lactose.amount=Hi) ||
       (Glucose.amount=Medium && Lactose.amount=Medium)

   -- 酵素はそれをコード化している遺伝子が発現しているときに作られる
   all e : Enzyme |
     e in EColi.make iff
      (some g : LactoseOperon | e in g.code && g in EColi.express)

   -- ラクトースを食べるのは二つの酵素が生産されているとき
   Lactose in EColi.feed iff
     Permease in EColi.make && Galactosidase in EColi.make

   -- グルコースが食べられるためのルールはない
   not (Glucose in EColi.feed)
}

なお、ここではabducibleな述語(amount)以外の述語に関しては、ルール以外で真にならないようにモデル化している。つまり、abducibleでない論理式Aについて、Aを導く規則が A←B と A←C だったら、AlloyがB,Cに関係なくAを真にすることを防ぐために、A⇔(B∨C) という論理式として記述する*2。 というのも、ルールに関係なく真にされてしまうと、「発想推論」にはならないので。

で、E. Coli がラクトースを食べていることを「説明」する仮説を求めるために、そのモデルを作ってみる。

pred goal() { Lactose in EColi.feed }
run goal

結果は以下のようになり、これはabducibleな述語amountを使った仮説 Glucose.amount=Lactose.amount=Medium が得られたことに相当する。 Nextボタンを押すと、Glucose.amount=Low, Lactose.amount=Hi な仮説も得られる。

ALP用のシステムと比較すると、ルールにないものは成り立たないということを明示的に記述せねばならず面倒。また、ALPの望ましい性質である仮説の極小性の保証はない。ただ、ALPのシステムの中には充足可能性のソルバを内部で利用するものもあり、ここではAlloyを使って同様のことをやってみたということで。