東ロボくんのこと（４）答案の論理式

公開された東ロボくんの答案の論理式についての解説にもニーズがありそうなので今日はそれを書くことにします．

まずは問題

http://livedoor.blogimg.jp/hyonko1007/imgs/0/4/04cec153-s.jpg

書き写すと

aを正の定数とする．実数x,yが1/2≦x≦1,a≦y≦2aを満たすとき，F=(x/y)+(y/x)-xyの最小値を求めよ．

というものです．

Fだけ見ると対称式で論じたくなりますが，定義域が一般には非対称なので，人間の受験生としての模範解答は上の画像の方のように変数を固定して扱うものだと思います．また人間がコードを書いてMathematicaのビルトイン関数Minimizeを用いるなら

のようになります．

一方，今回の東ロボくんの答案（の一部）は．．．

http://pc.watch.impress.co.jp/img/pcw/docs/624/993/html/01.jpg.html

日本語の部分はQEの問題に対して予め用意された定形とのことなので，項と論理式の部分について説明します．

まずは自由変数

　

を導入し，これがFの最小値に等しくなる条件を関数の最小値の定義（と等価な性質），つまり，一般に

　mは定義域Dの実数値関数fの最小値に等しい　≡　(∃x.(x∈D ∧ f(x)=m)) ∧ (∀x.(x∈D → m≦f(x)))

となることを用いて式にしています．具体的には

　∃x00 ( ∃y00 (1/2 ≦x00 ∧ x00≦1 ∧ a≦y00 ∧ y00≦2a ∧ y00(-x00) + y00/x00 + x00/y00 = xgen12 ) )

の変数を分離した

　∃x00 ( ∃y00 (a≦y00 ∧ y00≦2a ∧ y00(-x00) + y00/x00 + x00/y00 = xgen12 ) ∧ 1/2 ≦x00 ∧ x00≦1 )　…　A

と

　∀y0 ( ∀x0 ( (1/2 ≦x0 ∧ x0≦1 ∧ a≦y0 ∧ y0≦2a) → xgen12 ≦ y0(-x0) + y0/x0 + x0/y0 ) )

なのですが，後者のような含意 P→Q のままではQEに乗せられないので，(¬P)∨Q に直して

　∀y0 ( ∀x0 ( ¬(1/2 ≦x0 ∧ x0≦1 ∧ a≦y0 ∧ y0≦2a) ∨ xgen12 ≦ y0(-x0) + y0/x0 + x0/y0 ) )

さらに¬Pをドモルガン則で展開し，不等号の性質を適用して ¬(s≦t) を s＞t のように書き直し

　∀y0 ( ∀x0 ( 1/2＞x0 ∨ x0＞1 ∨ a＞y0 ∨ y0＞2a ∨ xgen12 ≦ y0(-x0)+ y0/x0 + x0/y0 ) )

変数を分離した

　∀y0 ( ∀x0 ( 1/2＞x0 ∨ x0＞1 ∨ xgen12 ≦ y0(-x0) + y0/x0 + x0/y0 ) ∨ a＞y0 ∨ y0＞2a )　…　B

との連言ということです．なお実際は B の前に 0＜a，括弧内の最後には0≧aが付いていますが，これらは

　0＜a ∧ (0＜a → B)

として生成されたものでしょう．

そして，この A および B をそれぞれQEすると

となります（見辛いので添字は略しています）．これと量化のスコープの外にあったa,yの式とを合わせたのが，東ロボくんの答案にあるQE後の式，すなわち

であり，これをgについて陽な形に整理したのが，最後の

です．

ここまで書けばお気付きのように，東ロボくんは定義域の条件のうちaの出現を含んだa≦y≦2aをaについての仮定として扱い，答にまで含めてしまっています．これは言語理解のミスなのですが，a≦y≦2aは定義域の条件の一部としても正しく理解されているので，やや不思議な気配を感じます．

．．．と，批判めいたことを書きましたが，今回の言語処理の結果からは恐るべき能力が見て取れます．

例えば，問題文では，関数を定義するのにF=…といった「論理式」が使われていますが，ここは単に右辺の関数値だけ，つまり「項」で与えられることもある訳で，彼はこうした違いを当然クリアしている筈です．より根源的な部分では，aの扱いです．すなわち，定義域を表す式はそれ自体紛れもなく３変数であり，式だけを追うならFも３変数関数と捉えてしまうかも知れないところを，彼は問題文の「aを…定数とする」の部分，および，「実数x,yが…を満たす」の部分から，aを自由変数，x,yを束縛変数として扱う判断を下している訳です．何でもないことのようですが，入試問題文の表現の多様性（というか，いい加減さ）を鑑みればこれは大変な構えだと思います．