Redlog 使ってみた - 現実と数学の区別が付かない

Quantifier Elimination (QE，限量子消去) を解いてくれるREDUCEのパッケージRedlogを使って大学の入試問題を解いてみます．

東工大 1969前期
実数 $a,b,c,x,y,z,p$ が次の次の4条件を満たしている： $a^2-b^2-c^2>0, ax+by+cz=p, ap<0, x>0,$ このとき $x^2-y^2-z^2$ の符号を調べよ．

名古屋大 1963前期
正方形 $ABCD$ とその内部の $1$ 点 $P$ がある．線分 $AP,BP,CP,$ の長さがそれぞれ $7,5,1$ であるとき，この正方形の面積を求めよ．

Quantifier Elimination (QE，限量子消去) とは

実数の理論において\begin{align}(a\neq0) \wedge\bigl( \forall x (ax^2+bx+c>0)\bigr)\end{align} は次の論理式と同値です．\begin{align} (a>0) \wedge (b^2-4ac<0)\end{align} 上の論理式は ∀(任意記号) とそれに縛られた束縛変数 $x$ がありますが，下の論理式は自由変数 $a,b,c$ だけの式になっています．∃ (存在記号) と ∀(任意記号) をあわせて限量子 (quantifier) と呼びます．このように論理式を，限量子が含まない同値な論理式に変形することをQuantifier Elimination (QE，限量子消去) と呼びます．実数の理論では，代数的な一階述語論理式を限量子が含まない同値な論理式に変形するアルゴリズムが存在することが知られています（タルスキの定理）．特に閉論理式（自由変数を含まない論理式）は，真か偽かをアルゴリズムで判定できます．

Redlog の使い方

REDUCE を Obtaining REDUCE から入手してインストールしましょう．
REDUCE を起動して，Redlog（reduce logic system）パッケージが読み込まれていないならロードしておきます．

load_package "redlog";

次にQEのためのおまじないをします（実数体 $\mathbb{R}$ の理論ですという宣言）．

rlset r$

Redlog には QE 用の関数 rlqe (Virtual Substitution)，rlcad (Cylindrical Algebraic Decomposition) などが用意されています．論理式は次の表くらいが分かっていればとりあえずは十分でしょう．

記号論理	Redlog
$\neq, \le, \ge$	<>,<=, >=
[式1] $\wedge$ [式2]	[式1] and [式2]
[式1] $\vee$ [式2]	[式1] or [式2]
[式1] $\rightarrow$ [式2]	[式1] impl [式2]
$\lnot$ [式]	not [式]
$\forall x_1,\forall x_2,\dots, \forall x_n$ [述語]	all({ $x_1,x_2,\dots,x_n$ }, [述語])
$\exists x_1,\exists x_2,\dots, \exists x_n$ [述語]	ex({ $x_1,x_2,\dots,x_n$ }, [述語])

問題をQEに翻訳

東工大 1969前期
実数 $a,b,c,x,y,z,p$ が次の次の4条件を満たしている： $a^2-b^2-c^2>0, ax+by+cz=p, ap<0, x>0,$ このとき $x^2-y^2-z^2$ の符号を調べよ．

次の論理式を考えてみましょう．\begin{align}\exists a\exists b\exists c\exists x\exists y\exists z\exists p\bigl(&(a^2-b^2-c^2>0)\wedge (ax+by+cz=p)\\&\wedge (ap<0)\wedge (x>0) \wedge (r=x^2-y^2-z^2)\bigr) \end{align}これと同値な自由変数 $r$ だけに関する論理式が，条件 \begin{align} a^2-b^2-c^2>0, ax+by+cz=p, ap<0, x>0\end{align}のもとでの $r:=x^2-y^2-z^2$ の取りうる値の条件となります．

名古屋大 1963前期
正方形 $ABCD$ とその内部の $1$ 点 $P$ がある．線分 $AP,BP,CP,$ の長さがそれぞれ $7,5,1$ であるとき，この正方形の面積を求めよ．

$xy$ -平面上で $A=(0,a), B=(0,0), C=(a,0), P=(b,c)$ とおくと条件は \begin{align} b^2+(a-c)^2=7^2, b^2+c^2=5^2, (a-b)^2+c^2=1^2, a > b > 0, a > c > 0 \end{align} と書けます．この条件のもとでの $a^2$ の値を求めたいので \begin{align}\exists a\exists b\exists c\bigl(&(b^2+(a-c)^2=7^2)\wedge (b^2+c^2=5^2)\wedge ((a-b)^2+c^2=1^2) \\ &\wedge (a > b)\wedge(b > 0) \wedge (a > c) \wedge(c > 0)\wedge (s=a^2)\bigr) \end{align} から限量子を消去して， $s:=a^2$ の取りうる値を求めればよいことになります．

Redlogで解いてみる

Redlog の QE 用の関数 rlqe，rlcad を使って実際に解いてみましょう．showtime で直前の計算でどれくらい時間がかかったのかを表示できます．

f:id:egory_cat:20201109023040p:plain
というわけで東工大の問題の答えは「負」，名古屋大の問題の答えは「 $32$ 」となります．