научная статья по теме О МЕХАНИЧЕСКОМ ДОКАЗАТЕЛЬСТВЕ ПЛАНИМЕТРИЧЕСКИХ ТЕОРЕМ РАЦИОНАЛЬНОГО ТИПА Математика

Текст научной статьи на тему «О МЕХАНИЧЕСКОМ ДОКАЗАТЕЛЬСТВЕ ПЛАНИМЕТРИЧЕСКИХ ТЕОРЕМ РАЦИОНАЛЬНОГО ТИПА»

ПРОГРАММИРОВАНИЕ, 2014, No 2, с. 41-50

КОМПЬЮТЕРНАЯ АЛГЕБРА

У V 004.92+004.94

О МЕХАНИЧЕСКОМ ДОКАЗАТЕЛЬСТВЕ ПЛАНИМЕТРИЧЕСКИХ ТЕОРЕМ РАЦИОНАЛЬНОГО ТИПА

© 2014 г. H.H. Осипов

Институт космических и информационных технологий СФУ 660074 Красноярск, ул. Киренского, 26 E-mail: nnosipov@rambler.ru Поступила в редакцию 01.09.2013

В статье предлагается элементарный подход к механическому доказательству планиметрических теорем рационального типа. Этот подход реализован в виде программных модулей geom и его модифицированной версии geom^zeta, созданных в системе компьютерной алгебры Maple. Приводятся примеры механических доказательств сложных теорем планиметрии (как хорошо известных, так и сравнительно новых) на основе удобных рациональных параметризаций.

1. ВВЕДЕНИЕ

Механический мет,од доказательства геометрических теорем известен уже сравнительно давно (например, [1]). Он стал возможен благодаря двум обстоятельствам: во-первых, появлению и совершенствованию алгоритмов решения систем полиномиальных уравнений и, во-вторых, бурному развитию как вычислительной техники, так и систем компьютерной алгебры, что способствовало эффективной практической реализации этих алгоритмов. Наиболее часто для механического доказательства теорем элементарной геометрии применяются алгоритм, базисов Грёбнера и метод Ву (например [2, гл. 6]).

Между тем существует довольно много содержательных геометрических теорем так называемого рационального типа, при механическом доказательстве которых можно обойтись вполне элементарными средствами и тем самым избежать применения "тяжёлой артиллерии коммутативной алгебры" (В.И. Арнольд). В настоящей статье предлагается элементарный подход к механическому доказательству теорем рационального типа в планиметрии.

Этот подход основан на применении алгебры комплексных чисел и сводится к конечной последовательности вычислений, непосредственно вытекающей из формулировки теоремы. Вычис-

ления с комплексными числами как метод доказательства теорем планиметрии применяются давно (например, [3, гл. III]); с появлением компьютеров и систем компьютерной алгебры этот метод получил новые возможности.

В данном случае под вычислениями понимаются обычные алгебраические операции в поле рациональных дробей

F (z i,... , zn, щ1, ... , um),

где F — поле рациональных чисел Q или какое-нибудь его конечное расширение. Все переменные Zk предполагаются комплексными и удовлетворяющими условию |zfc | = 1, а все переменные щ - вещественными. Предлагается некоторый набор стандартных вычислительных процедур и проверочных тестов, оформленный в виде модуля geom и его расширенной версии geom_zeta в системе компьютерной алгебры Maple.

Статья организована следующим образом.

В разделе 2 приводятся правила перевода наиболее употребительных геометрических условий (терминов) на язык алгебры комплексных чисел и затем вводится понятие планиметрической теоремы рационального типа.

Раздел 3 содержит довольно подробное описание модулей geom, geom_zeta и особенностей их программной реализации.

В разделе 4 предлагаются удобные рациональные параметризации различных элементов треугольника, позволяющие снимать внешние условия и тем самым избегать применения таких затратных процедур, как вычисление базисов Грёбнера и упрощение вложенных радикальных выражений. При этом эксплуатируется только возможность эффективной реализации обычных алгебраических операций в кольце многочленов F[zi,..., zn, ui,..., um] и операции нахождения НОД (или, как вариант, операции факторизации).

В завершающем разделе 5 собраны наиболее содержательные примеры механического доказательства планиметрических теорем рационального типа (как классических, так и недавно открытых) на основе предложенных рациональных параметризаций. В конце раздела демонстрируется одна интересная особенность механического доказательства на основе вычислений с рациональными дробями над некоторым круговым полем: наличие у этого поля нетривиальных автоморфизмов приводит к тому, что оказываются доказанными сразу несколько схожих геометрических теорем.

2. ТЕОРЕМЫ РАЦИОНАЛЬНОГО ТИПА

Чтобы сформулировать, что мы понимаем под планиметрической "теоремой рационального типа", предварительно укажем перевод на язык комплексных чисел некоторых стандартных геометрических величин, построений и условий.

Введём обозначения: l(P,v) — прямая, проходящая через точку P в направлении вектора v; c(O, P) — окружность с центром в точке O, про-

P

социированное с точкой (вектором) евклидовой плоскости, будем обозначать той же буквой, что и саму точку (вектор); черта сверху обозначает комплексное сопряжение.

1. Квадрат расстояния между точками P и Q равен

|P - Ql2 = (P - Q)(P - Q).

2. (Ориентированная) площадь треугольника ABC равна

(B - A)(C - A) - (B - A)(C - A) 4i .

3. Вектор, полученный из вектора v поворотом на угол а в положительном направлении, равен w = zv, где z = cos а + i sin а.

4. Точка пересечения непараллельных прямых l(P,v) и l(Q,w) есть

v(Qw — Qw) — w(Pv — Pv) vw — vw '

5. Центр окружности, проходящей через не-коллинеарные точки P, Q, R, есть

(IQI2 — |P l2)(P — R) — (IRI2 -|P l2)(P — Q)

(P — Q)(P — R) — (P — Q)(P — R) '

6. Ортогональная проекция точки Z на прямую l(P,v) есть

Zv + Zv + Pv — Pv Z

прямой l(P,v), есть

Zv + Pv — Pv v

Z

точки O, есть 2O — Z.

9. Точка Z лежит на окружности c(O, P) тогда и только тогда, когда

|Z — O|2 = |P — O|2.

Z

чале координат и радиусом 1 (единичная окружность) тогда и только тогда, когда Z = Z-1. vw

тогда, когда

vw — vw = 0.

vw ко тогда, когда

vw + vw = 0.

12. Неколлинеарные точки P, Q, R, S лежат на одной окружности тогда и только тогда, когда

P — R P — S = P — R P — S Q — R ' Q — S = Q — R ' Q — S.

13. Треугольники ABC и PQR подобны и одинаково ориентированы (подобие 1-го рода) тогда и только тогда, когда

AQ + BR + CP = BP + CQ + AR

(здесь Ад и т. д. — это произведение комплексных чисел А и Q).

14. Треугольники АБС и PQR подобны и противоположно ориентированы (подобие 2-го рода) тогда и только тогда, когда

Ад + вR + сР = вР + сд + ая.

15. Прямая 1(Р, V) и окружность е(0,0) касаются в точке Т тогда и только тогда, когда |Т - 0|2 = |д - 0|2, где

Т _ Оу + Оу + Ру - Ру

_ 2У .

16. Окружности с(Р, 2) и с(д, Ш) с разными

Т

гда, когда |Т — Р|2 _ |2 — Р|2, где

Т _

|212 -1ш|2 - 2Р - 2р + шд + Шд - Рд + рд

2(д - р ) '

Предположим, что некоторым элементам Аь ..., А5 (это могут быть точки, углы, векторы и т. п.) данной в условии теоремы геометрической конфигурации сопоставлены некоторые (вообще говоря, комплекснозначные) параметры ¿1, ..., при этом все остальные элементы конфигурации Б^, ..., Бг в переводе на язык комплексных чисел представляют собой рациональные выражения:

Б3 _ /(¿1,...,и з _ 1,...,г.

(Коротко говоря, данная конфигурация допускает рациональную параметризацию.) Если, кроме того, заключение теоремы — некоторое условие С(А1,..., А3, Б1,..., Бг) — равносильно проверке тождества

R(tl, /1(^1, ...,ts),..., /г (¿1, . . . , ts)) _ 0,

где R — некоторая рациональная функция своих аргументов, то такую теорему мы будем называть теоремой рационального типа.

Довольно типичной является ситуация, когда элементы конфигурации последовательно получаются из "стартовых" элементов А1, ..., А3 при помощи стандартных построений пп. 3 — 8, а заключение теоремы состоит в проверке одного из условий, указанных в пп. 9 —16. Отметим, что

примерами теорем рационального типа являются большинство классических теорем планиметрии (например, [4]). Список геометрических построений и условий рационального типа можно было бы пополнить (например, добавив условие равенства двух ориентированных углов), однако представляется целесообразным делать это в процессе доказательства конкретных теорем.

3. МОДУЛИ GEOM И GEOM ZETA

Модуль geom и его модифицированный вариант geom_zeta созданы на базе системы компьютерной алгебры Maple и содержат в текущих версиях следующий набор функций и тестов, применяемых при механическом доказательстве планиметрических теорем рационального типа.

• Collinear(a,b) — тест на коллинеарность векторов a и b;

чение прямых l(P,a), l(Q,b), l(R,c) в одной точке;

ность точек P, Q, R, S одной окружности;

PQ RS; лярность векторов a и b; 1-го рода треугольников ABC и PQR;

ABC PQR; l(P, a) и окружности c(Q, R); окружностей c(P, Q) и c(R, S);

ABC;

P Q R;

ABC;

• conjugate(X) — выражение, комплексно сопряжённое к выражению X;

ния прямых l(P, а) и l(Q, b);

• X;

высот треугольника ABC;

ция точки Z на прямую l(P, а);

мой PR и радикальной оси окружностей c(P,Q)rn c(R, S);

точке Z относительно прямой l(P,a); чения прямой l(P, а) с окружностью c(Q, P);

ке Z относительно точки P.

В модуле geom все вычисления выполняются в поле рациональных дробей над полем коэффициентов F = Q(i). Поскольку в условии теоремы отдельные элементы геометрических фигур могут быть конкретизированы (так, некоторые углы могут иметь фиксированные величины, соизмеримые с 180°), при вычислениях могут возникнуть рациональные дроби над каким-нибудь другим полем алгебраических чисел. В модуле geom_zeta в качестве поля коэффициентов рассматривается F = Q(i, Z), где Z — корень из единицы некоторой степени.

Функция conjugate задействована (явно или неявно) во всех других тестах и функциях, поэтому необходимо пояснить, как она работает. Предполагается, что поступающее на вход этой функции рациональное выражение зависит от специальных переменных Zk, к = 1,... ,n (и = 6 по умолчанию), значения которых считаются по модулю равными 1, и, возможно, некоторых других переменных щ, l = 1,... ,m, которые считаются вещественнозначными. Для модуля geom сопряжение данного выражения состоит в замене всех Zk на z—1 и замене мнимой единицы i на —i. В случае модуля geom_zeta происходит

такая же замена специальных переменных и замена специальной константы п на г/-1. По определению, п обозначает такой корень из единицы,

Q(i, Z ) = Q(n),

где Z — корень из единицы, который предполагается использовать в вычислениях. Нетрудно видеть, что

deg п = НОК (deg Z, deg i) = НОК (deg Z, 4).

Для кор

Для дальнейшего прочтения статьи необходимо приобрести полный текст. Статьи высылаются в формате PDF на указанную при оплате почту. Время доставки составляет менее 10 минут. Стоимость одной статьи — 150 рублей.

Показать целиком