述語論理でケーキのレシピを書いてみる
ケーキのレシピを述語論理で書いてみようと思う。
ケーキのレシピを調べてはみたものの、作ったこともないし、述語論理で書きやすいように変えているから、本当にケーキを作る人からみたら、これはケーキのレシピではないと言われるだろう。
こういうものを述語論理で書くとこんなふうになるかなという好奇心で書いていることを暖かく見守ってほしい。
料理のレシピは、アルゴリズムのようでアルゴリズムではない。なにかもっとふんわりとして、詳細は調理する人間に任されている何かだと思う。
そういうものを述語論理で書こうというのだから、間違った方向に進んでいるように思われるかもしれないが、私はこういうものを書こうとするとどこまでできるのか、に興味がある。
以前の例では、目盛の上にある石を認識して、その色と位置をclause/リテラル化するセンサーがあると考えた。
レシピの場合は、調理台を観測するセンサーと、レシピに言われた通りの作業をする人間/ロボットがいると考える。
何か作業をすると調理台に何かができるので、それをセンサーが検知して、新しいFactとしてのclauseを生成する。
そして、そのclauseを元にレシピに従って次になすべき作業がわかる。
作業の目的は述語で書かれ、それに従ってまた人間/ロボットが作業をするというサイクルになる。
この調理作業を指示するclauseのリテラルは、センサーと逆の働きをして、人間またはロボットにそのclauseが真になるように働け、と言っているわけだ。
というような具合でシステムを想定する。
レシピとしてΣ0というclause集合を作り、材料や調理作業の中間制作物は、その都度Factとしてclauseが登録され、Σ1, Σ2,...というようにclause集合が変化していくと考える。
[観測対象]
まず、調理台がある。
調理台を観測するセンサーがあって、次のような状態をみつけたらfactのclauseを生成する。
このFactは次のようなものがある。
・材料の準備ができて、調理台に置かれた。
・調理の工程から何かが作られた。
[初期 材料]
材料が調理台に置かれると、センサーがそれを検知し、対応する状態を次のようなclauseで表すことにする。述語と材料を示す定数も含めて、次の通りである。
2* +SUGARP(SUGAR) 述語は「砂糖がある」。定数は「砂糖」を示す。
3* +EGGWHITE(WHITE) 述語は「卵の白身がある」。定数は「卵の白身」を示す。
4* +EGGYELLOW(YELLOW) 述語は「卵の黄身がある」。定数は「卵の黄身」を示す。
5* +SIFTED(RICEFLAUR) 述語は「篩にかけた小麦粉がある」。
定数は「篩にかけた小麦粉」を示す。
6* +MILKP(MILK) 述語は「牛乳がある」。定数は「牛乳」を示す。
材料はなんらかの容器に入れられているはずだが、そこは省略している。
調理台にこれらの材料が置かれた時、それぞれのclauseがFactとして作られるのであり、最初から提示されるわけではない。それをclauseの番号に*をつけて示している。
[生産物]
次に、調理作業によって生産されるものは次のようなものがある。変数xで表しているのは、調理によってできるものを次に使うので、変数を用いている。説得力はないかもしれない。
Mix1(x) 卵の黄身と砂糖を混ぜたもの
Melenge(x) メレンゲ
Dough(x) 生地
D1(x) 生地になる前の第一段階
D2(x) 生地になる前の第二段階
Cake(x) ケーキ
補足
Mix1(x): 卵の黄身と砂糖を混ぜたものについて、調べたレシピでは名前がなかったので、このように名付けた。
D1とD2: 生地になる前段階と前前段階のなにかの名前。調べたレシピでは名前がついていなかったので、このように名付けた。
ケーキは焼いただけのものである。クリームを塗ったりする作業は省略した。
[調理作業]
人間の行える作業は、材料を混ぜる、焼く、の2つである。
1) X, Yを混ぜたものがZである。
+Mixpr1(x,y) 黄身と砂糖をまぜる(1)
+Mixpr2(x,y) 白身と砂糖をまぜる(2)
+Mixpr3(x,y) (1)と篩にかけた小麦粉をまぜる。これがD1になる(3)
+Mixpr4(x,y) D1に牛乳を混ぜる。これがD2になる
+Mixpr5(x,y) D2にメレンゲを混ぜる。これが生地になる。
もしもセンサーが優秀で、混ぜ合わされたものを見るだけで、その素材が判定できるのなら、これらの述語の1とか2の数字をとって、Mixprだけでよいと思う。
人間は、一目でわかりそうだし、これらの混ぜ合わせたものをいくつも調理台に並べることはなさそうだ。それはたぶん、調理台の上でおこなわれる作業とその結果を認識(経過、履歴を認識)しているからだろうと思う。そのような区別は、このように述語を分けるのと同じことなのではないだろうか。
2) Xをオーブンで焼いたものがYである。
+Bakepr(x)
これらの述語を真にするために、人間/ロボットが何かをすることを強制される。
そしてその調理行動によって、前に書いた生産物が発生し、センサーがそれを検出する。
材料のFactや調理中に出現する生産物のFact、それらをつなぐレシピのclause/記述から次のconjecture
+Cake(z)
となるzを求めることができれば、レシピに基づいたケーキ作成の証明/反証ができたと考える。
その様子を確かめるために、レシピをこのように書く。
以下のレシピに書いているclauseがΣ0になる。ただし、clauseにつけた番号に*がついているものは除く。
というのもここまでに登場した、「材料」や「生産物」はΣ0には含めない。センサーも人間/ロボットはこのレシピの外の世界の存在なので、レシピのclause集合Σ0だけでは証明/反証は作れない。このパン号に*をつけたclauseは、Σiから証明/反証を作れるようにするための補助的なclauseになる。
レシピのclause集合が、矛盾していないとか、意図した通りに動けばレシピの想定している手順になっているとかいうことを、デバッグ/トレースするための仕掛けになっている。あるいは、センサーや人間/ロボットがこれらのclauseを成り立たせることが、外の世界に求められているという意味でもある。
[レシピ]
具体的に、どのような材料や生産物から、次に何をすべきかを示すのがレシピである、と考える。
1) 卵の黄身と砂糖を混ぜる
まず、卵の黄身と砂糖をボウルに入れて、それを混ぜる。
8 ∀X.150 Y.151 [-EGGYELLOW(X.150) -SUGARP(Y.151) +MIXPR1(X.150,Y.151)]
ボウル自体はここに書いていない。ケーキの調理では、生地を作るときの作業は全部ボウルの中で行い、どこでまぜているかは気にしなくてはいいのではないかと思う。パンのように、生地をテーブルの上でこねるような場合は、区別したほうがいいかもしれない。
まぜたものはセンサーによって識別されると、MIX1という述語を真にする。それをこのように書く。
9* ∀X.152 Y.153 [-MIXPR1(X.152,Y.153) +MIX1(MX1(X.152,Y.153))]
9*のように*をつけたclauseは、材料のclauseと同じように、作業の生産物が発生するとセンサーによって導出されると考えるので、実際にはこのようなclauseは必要ない。
MIXPR1によって人間/ロボットが調理行動をすると、9*の左リテラルが消滅して+Mix1(x)という述語が真になる。もしもセンサーが機能していれば、このclauseはセンサーによって検知されたものになるだろう。
2) メレンゲを作る。
卵の白身に砂糖を加えて、混ぜる。
10 ∀X.154 Y.155 Z.156 W.157 [-EGGWHITE(X.154) -SUGARP(Y.155) +MIXPR2(X.154,Y.155)]
混ぜ終わるとメレンゲができる。
11* ∀X.158 Y.159 [-MIXPR2(X.158,Y.159) +MELENGE(MEL(X.158,Y.159))]
3) D1を作る。
黄身に篩をかけた小麦粉を加えて混ぜる。
12 ∀X.160 Y.161 [-MIX1(X.160) -SIFTED(Y.161) +MIXPR3(X.160,Y.161)]
混ぜ終わると、できたものを見てセンサーがD1を真にする。
13* ∀X.162 Y.163 [-MIXPR3(X.162,Y.163) +D1(DO1(X.162,Y.163))]
4) D2を作る。
D1に牛乳を混ぜる。
14 ∀X.164 Y.165 [-D1(X.164) -MILKP(Y.165) +MIXPR4(X.164,Y.165)]
混ぜ終わると、できたものを見てセンサーがD2を真にする。
15* ∀X.166 Y.167 [-MIXPR4(X.166,Y.167) +D2(DO2(X.166,Y.167))]
5) 生地ができる。
・D2にメレンゲを混ぜる。
16 ∀X.168 Y.169 [-D2(X.168) -MELENGE(Y.169) +MIXPR5(X.168,Y.169)]
混ぜ終わると、できたものを見てセンサーが生地(Dough)であるという。
17* ∀X.170 Y.171 [-MIXPR5(X.170,Y.171) +DOUGH(DOU(X.170,Y.171))]
6) 生地を焼いてケーキを作る
生地を焼く
18 ∀X.172 [-DOUGH(X.172) +BAKEPR(X.172)]
生地を焼いたものがケーキになる。
7 ∀X.149 [-BAKEPR(X.149) +CAKE(OVEN(X.149))]
7は人間の作業でもあるが、オーブンの仕事が主なのでセンサーの活躍は省略してみた。
これも*つきのclauseにして、センサーでケーキの完成を監視するというストーリーでもよさそうに思う。
次に、証明/反証をどうやるかを考えてみる。
まず、¬conjは次のようにCakeの否定になる。ケーキができないと仮定して、矛盾を導く決意である。
1 ∀Z.148 -CAKE(Z.148)
これで全体がつながった。
補足
・上のclauseには関数が登場していた。
たとえば、17の+DOUGH(DOU(X.170,Y.171))の部分では、D2とメレンゲをまぜたものを引数としてとるDouという関数でできたものが生地だと言っている。
clause全体として出てくる変数には、定数や定数引数の関数形のtermしか出てこないので、変数を使う必要もない気がするが、作業を一般的に書いてみている。それで、素材と生産物の関係を表す意味で関数を使った。
・想定しているシステムではレシピ全体での証明は目的になっておらず、全体の作業の流れを確かめるのが目的になってしまっている。調理作業の生産物をセンサーで検知して次の作業を導くところは、証明と機械学習が協力する場面なので、もうすこし時間をかけて考えたい。
・ケーキを作るという手順はこれだけではなく、たとえばケーキにデコレーションするといった作業もあるが、どう書けばいいのかわからなかったので触れていない。そういう「どう書けばいいのかわからない」という部分もいろいろある。
・アルゴリズムではないけれど、あいまいな部分はセンサーと作業の命令部分に配置してしまっているので、レシピの部分はアルゴリズムを書くのと大差ないようにも思える。
・アルゴリズムを書くのならば、Prologという論理プログラミング用の言語がある。ここに書いたものも、Prologと似たようなものだ。何かそれとは違う書き方を考えたかったのだが、うまくできていない。
・センサーが材料や、生産物を認識しているという前提になっているが、そんなことが可能なのかどうかはむずかしい。実現できない物を前提としているかも。
また、人間/ロボットに命令するリテラルというものを考えたが、「リテラルを真にする」という動機で何かをさせようとするのはどれほど実現加能なのかはわからない。
・このような問題で、述語の意味は、最終的にセンサーやロボットの実装によって決まってくると思う。だとすると、現実のそういう仕組みがどのような述語に対応するのかを定義したり、実装と述語が正しく対応しているかをどうやって確認するのかなど、考える必要があるだろう。
これは数学と違うところなので、述語論理の記述対象にならないことを書こうとしているのだろう。