ジュニア算数オリンピックにおけるユークリッド幾何学の問題の解答の自動化を模索している。まず三角形定理ループを回し、回答できなかったら1ステップの作図を試していって、それらで回答できるか探る。それでも駄目だったら2ステップ、3ステップと増やしていく。交点の確認はこの方法を使う。
『図の四角形ABCDはAB=BC=CDで、角B=168度、角C=108度です。角Dの大きさを求めなさい。
』
前回の続きで2ステップ目だけど、クラスタの外から作図した時にどうなるかを見てみたい。なので、1ステップ目はABをB側に延長して、それから2ステップ目をいろいろ試していく。
以下5種類の作図をしていく。直接作図したもの以外に三角形や、あるいは正四角形や正五角形ができていたら、次の定理ループで角度が明らかになる可能性がある。
じゃあ、初期状態。
graph := [ "A" : [ [["B"], []], [["D"], []] ] , "B" : [ [["A"], []], [["C"], []] ] , "C" : [ [["B"], []], [["D"], []] ] , "D" : [ [["A"], []], [["C"], []] ] ]; triangle_lst := [ ]; cluster_lst := [ #shape_lst? [["A", "B", "C", "D"], ["BAD_p", "AB", "ABC_p", "BC", "BCD_p", "CD", "ADC_p", "DA"]] ]; always { "ABC_p" == 168; "BCD_p" == 108; "AB" == "BC" == "CD"; "ABC_p" + "ABC_n" == 360; "BCD_p" + "BCD_n" == 360; "BAD_p" + "BAD_n" == 360; "ADC_p" + "ADC_n" == 360; }
じゃあABと同じ長さをB側に作図。新しい点はE。
graph := [ A : [ [[B, E], []], [[D], []] ] , B : [ [[A], [E]], [[C], []] ] , C : [ [[B], []], [[D], []] ] , D : [ [[A], []], [[C], []] ] , E : [ [[A, B], []] ] ]; triangle_lst := [ ]; cluster_lst := [ [[A, B, C, D], [BAD_p, AB, ABC_p, BC, BCD_p, CD, ADC_p, DA]] ]; always { ABC_p == 168; BCD_p == 108; AB == BC == CD; ABC_p + ABC_n == 360; BCD_p + BCD_n == 360; BAD_p + BAD_n == 360; ADC_p + ADC_n == 360; AB == BE; CBE_p + ABE_h == ABC_n; ABE_h == 180; CBE_p + CBE_n == 360; CBE_p + ABC_p == ABE_h; ABE_h + ABC_p == CBE_n; }
hっていうのを導入した。ハーフ。pとnの反転がよくあるけど、180だったら意味無いんで、仮に。
これ、あらかじめ、「~~~_p < 180」で、「~~~_p + ~~~_n == 360」で、っていうのをalwaysの上の方に定義できないかな。いちいち入れてった方が良いのかな。
あと今気付いたけど、「"AB" == "BE"」とかで無く、「AB == BE」では?文字列の比較になっていて、これマズいよな。直した。まあ元々、集合とか存在の類だし、こちらの方が意味的には純化したと言えるだろう。名前も参照できるようにしよう。
じゃあ、2ステップ目の作図。
まず、点と点を繋げる作図。新しく作ったEと他の点を繋げる。CとDで迷うが、Cは予測がつくので、Dにしよう。
graphを更新。
で、新しく作ったDEと他の辺、例えばBCが交点を持つかだけど、これは三角関数?が無いと分からないんじゃないか。
その辺とその辺自体が属する点とで交点を持つことは無いとして、AとBとCに属する辺を1つずつ調べていけば良いと思うけど。DとEのどちらにも属してない辺は無いんで、これ自体は難しく無いだろう。
三角形自体は自ずと面というかクラスタなんで、四角形の中に耐震構造のバッテンみたいに三角形を4つ見い出せば(いや四角錐じゃなくて、底辺を共有する三角形を、更に底辺がバッテンになるように重ねたような)、それは流石にクラスタと言えると思うが。
面で無く、平面という概念を導入したとして、グラフで繋がっていれば内角が合計360°、と言えるわけでは無いと思うんだよな。辺が重なるように置くことはできるわけだし。
交点が発生しない(発生するか分からない)ので、結果新しい三角形は無し。新しい三角形が発生しないので、この作図はこのステップでは意味が無かった。
graph := [ A : [ [[B, E], []], [[D], []] ] , B : [ [[A], [E]], [[C], []] ] , C : [ [[B], []], [[D], []] ] , D : [ [[A], []], [[C], []], [[E], []] ] , E : [ [[A, B], []], [[D], []] ] ]; triangle_lst := [ ]; cluster_lst := [ [[A, B, C, D], [BAD_p, AB, ABC_p, BC, BCD_p, CD, ADC_p, DA]] ]; always { ABC_p == 168; BCD_p == 108; AB == BC == CD; ABC_p + ABC_n == 360; BCD_p + BCD_n == 360; BAD_p + BAD_n == 360; ADC_p + ADC_n == 360; AB == BE; CBE_p + ABE_h == ABC_n; ABE_h == 180; CBE_p + CBE_n == 360; CBE_p + ABC_p == ABE_h; ABE_h + ABC_p == CBE_n; }
次は「点と点の分だけ線を延長」なんだが、1ステップ目のBEが絡んで欲しいんで、CDをC側に延長してみる。新しい点はF。
って、これも交点分からないじゃん。スルー。
じゃあその次は、「2点と、その間の垂直線とどこか1辺の交点による、二等辺三角形の作図」。当然、二等分する辺はBE。
ABやBCは、一旦CEとかを作図して三角形にして、底辺の角度を見て判断すれば良い。そういうのはもうやったことがあると思う。
問題は、CDやADと交わるかどうかの判断。これはBECDとかでクラスタを作らないと、分からないのではないか。
理想としては、辺BCを共有した三角形BCEとBCD、辺DEを共有したCDEとBDE。前者のセットで共有していないDとEの角が、後者のセットのDやEの角の和になっていて、後者のセットで共有していないCとBの角が、前者のセットのCやBの角の和になっている。そうなると流石にそれは面なのではないか。
ちょうど三角形もできるしな。じゃあBECDの全部の点を結んで、うーん、どうしようかな。そういう作図は既にあるんだけど、4ステップ後になってしまう。そもそも、例えばBEとBEの垂直二等分線とADの交点で二等辺三角形を作って、何なんだ?例え導入するにしても、そういうのが必要な問題が出てきてからで良くないか。それなら、BやEに登録してある辺だけ調べれば良くなるわけだし。そうしようか。
だとしたら、Aは無いとして、EとCを結ぶことになるだろうな。
いやでも、このCEの作図がもったいないというか、例えばBCと交わらないと分かったら、CEと交わると分かるわけだし。これは待つのもありなんじゃないかなあ、1ステップだし。
だとしたら、cluster_lstを調べていって、その辺だけ調べていけば良いんじゃないかなあ。具体的にどういう風に手順を組み立てるかは分からないけど、そういう方針で行くという話で。BE関係無いし。
次は、「ある1辺と同じ長さの辺を別の辺に落とすことによる二等辺三角形の作図」。BEをBCに落とすことにする。
俺は見落としていたのだけど、これは落とす方の辺が長かったら、垂線を落とせない可能性があるのだな。
だとしたら、この作図も、すでに判明している三角形に限るべきかもしれない。両方の角が90°以下の時に、垂線と底辺の半分への辺を作図して、昨日みたいに条件式にかける。
今日はここまでで良いか。