%%
%% A.L.Semenov
%% version 10.12.2002
%%
%% codepage 866
%% Russified LaTeX2e, based on LaTeX2e 2001/06/01
%% Document Class: article 2001/04/21 v1.4e
%% Package: amsthm 2000/10/26 v2.08
%% Package: russcorr 1996/03/24 (by S.Lvovski)
%%

\documentclass[12pt,draft]{article}

\usepackage{amsmath,amsthm}
\usepackage[indentheadings]{russcorr}

\hfuzz=0.5pt
\tolerance=400

\newtheorem*{main_lem}{Основная лемма}
\renewcommand{\proofname}{Доказательство}

\newcommand{\clos}{\mathbf{C}}
\newcommand{\bas}{\mathbf{BC}}
\newcommand*{\vct}[1]{\mathbf{#1}}


\title{%
Упрощ\"енное доказательство
теоремы Тарского о разрешимости
элементарной теории поля
действительных чисел\thanks{
        Институт новых технологий,
        109004, Москва, ул. Нижняя Радищевская, 10.
        Работа выполнена при частичной
        финансовой поддержке Совета поддержки научных школ
        при президенте РФ и гранта N~01-01-00505
        Российского Фонда Фундаментальных Исследований.}
}

\author{Алексей Семенов\thanks{
        \mbox{E-mail}: alsemenov@mtu-net.ru,
        fax:~(095)915-69-63.}
        \and
        Андрей Мучник\thanks{
        \mbox{E-mail}: muchnik@lpcs.math.msu.ru,
        fax:~(095)915-69-63.}
}
\date{}

\begin{document}
\maketitle

Вопрос о существовании алгоритма,
позволяющего среди всех предложений
какого-нибудь формального языка
выделять истинные,
является одним из центральных вопросов
математической логики с самого е\"е возникновения
в начале XX века.
Уже в 10-е и 20-е годы были построены
разрешающие алгоритмы для важных логических теорий.
В дальнейшем наиболее значительными достижениями
в этой области явились
теорема Тарского о разрешимости элементарной теории
поля действительных чисел
и теорема Рабина
о разрешимости монадической теории
бинарного дерева.

Естествен практический интерес
к построению разрешающих алгоритмов.
Были предприняты попытки
запрограммировать эти алгоритмы на ЭВМ.
Это закономерно, так как логические языки
являются гибким и естественным средством формализации
самых различных задач, не сводящихся к прямым числовым
вычислениям.
Однако указанные попытки привели к программам,
работающим слишком долго
даже на очень коротких примерах.
Это явление оказалось не случайным,
в 70-е годы было обнаружено,
что для задач разрешения обычно рассматриваемых
логических теорий
в принципе не может существовать алгоритмов,
недолго работающих на всех исходных данных.

Тем не менее нам кажется, что в этой области
имеются некоторые основания
для оптимистической точки зрения.
Дело в том, что
при практическом использовании алгоритма
его и не нужно будет применять ко \emph{всем}
исходным данным.
Исходные данные всегда будут браться
из некоторого \glqq осмысленного\grqq{}
класса, на котором алгоритм может работать
приемлемое время.

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

\bigskip

Дадим необходимые определения.

Формулы элементарного языка
строятся индуктивно:
\begin{enumerate}
\item Атомная формула~--- формула.
(Для поля действительных чисел
атомные формулы имеют вид
$\tau < \rho$, $\tau > \rho$, $\tau=\rho$,
где $\tau$, $\rho$~--- термы.
Термы~--- это многочлены от нескольких переменных
с рациональными коэффициентами.)
\item Если $A$, $B$~--- формулы, то
$(A\lor B)$, $(A\land B)$, $(A\to B)$, $\neg A$,
$\exists x A$, $\forall x A$~--- формулы.
\end{enumerate}
\emph{Элементарной теорией} некоторой структуры
называется множество всех формул элементарного языка,
истинных в данной структуре.

Наиболее широко применимым видом
разрешающих алгоритмов
яв\-ля\-ют\-ся алгоритмы элиминации кванторов.
Поясним неформально идею элиминации.
Естественная идея, возникающая при построении
алгоритма разрешения логической теории, состоит в том,
что работа такого алгоритма должна определяться
индукцией по построению формулы.
Попытаемся реализовать эту идею.
Пусть, например, $A$ и $B$~--- предложения,
тогда истинность предложения $(A\lor B)$
тривиально определяется истинностью $A$, $B$.
Таким образом, если алгоритм уже наш\"ел
истинностные значения $A$ и $B$,
то не составляет труда определить
истинностное значение $(A\lor B)$.
Трудность возникает при рассмотрении
формулы $\exists x A$.
Чтобы проверить е\"е истинность
нужно рассмотреть, вообще говоря,
бесконечную дизъюнкцию
подстановок в $A$
всевозможных конкретных значений $x$.
Формула $A$ может содержать
свободную переменную $x$.
При дальнейшем разложении формулы на подформулы
могут появиться другие свободные переменные.
Иногда формуле $\exists x A$,
где $A$ может содержать помимо $x$
и другие свободные переменные,
уда\"ется поставить в соответствие
эквивалентную ей бескванторную формулу.
Эта операция и называется \emph{элиминацией квантора}.
Конечно, е\"е можно осуществить не всегда.
Но когда она возможна для всех формул
и осуществляется алгоритмически,
а сама структура конструктивна,
то мы получаем алгоритм разрешения
элементарной теории.
Если формулам $A$ и $B$
уже сопоставлены эквивалентные им
бескванторные формулы, то
формуле $(A\lor B)$ сопоставлятся
дизъюнкция этих бескванторных формул.
Аналогично поступаем
с остальными пропозициональными связками.
Заметим, что специальной конструкции для элиминации
квантора $\forall$ не нужно, так как $\forall x A$
эквивалентно $\neg\exists x\neg A$.

\bigskip

Результат об элиминации кванторов
в элементарной теории действительных чисел
со сложением, умножением и порядком
принадлежит А.~Тарскому (\cite{tar}).
При этом время работы алгоритма,
разрешающего указанную теорию,
было неэлементарным.
Таким же было время работы алгоритма,
применяющего методы алгебраической геометрии,
который был предложен в~\cite{seiden}.
В дальнейшем был найден
более сложный (в смысле описания) алгоритм,
работающий на экспоненциальной зоне
(\cite{best}).
То, что всякий алгоритм разрешения
рассматриваемой теории на бесконечно
многих входах работает экспоненциальное время,
было доказано в~\cite{rabin}.
Целью нашей статьи является
максимальное упрощение конструкции алгоритма
и обоснования е\"е корректности.
С точки же зрения сложности вычисления
предлагаемая разрешающая процедура
не экономнее, чем была у Тарского.
Сообщение о нашей работе
появилось в~\cite{sem}.
Простейшим из ранее известных
было доказательство П.~Коэна
из~\cite{cohen1}.

Прежде чем описывать процедуру элиминации,
введ\"ем некоторые дополнительные определения.

Фиксируем переменную $x$ и определим четыре операции
над термами нашей теории, рассматриваемыми
как многочлены от $x$, коэффициенты которых~---
многочлены от остальных переменных.
Эти операции будут применяться только к многочленам
ненулевой по $x$ степени.
\begin{enumerate}
\item \emph{Взятие производной}:\label{oper:1}\\
      $a_nx^n+a_{n-1}x^{n-1}+\cdots+a_0\mapsto
       na_nx^{n-1}+(n-1)a_{n-1}x^{n-2}+\ldots+a_1$.
\item \emph{Модифицированный остаток}:\label{oper:2}
       применяется к двум многочленам
       $p(x)=a_nx^n+a_{n-1}x^{n-1}+\ldots+a_0$ и
       $q(x)=b_mx^m+b_{m-1}x^{m-1}+\ldots+b_0$
       таким, что $m\leqslant n$ и $b_m\ne 0$,
       и да\"ет такой многочлен $r(x)$, что
       $$
         b_m^{n-m+1}p(x)=q(x)h(x)+r(x)\,,
       $$
       где $\deg r(x) < \deg q(x)$ и
       $h(x)$~--- некоторый многочлен.

\item  \emph{Взятие старшего коэффициента}:\\
       $a_nx^n+a_{n-1}x^{n-1}+\cdots+a_0\mapsto a_n$.
\item  \emph{Отбрасывание старшего члена}:\\
       $a_nx^n+a_{n-1}x^{n-1}+\cdots+a_0\mapsto
        a_{n-1}x^{n-1}+\cdots+a_0$.
       \label{oper:4}
\end{enumerate}

При всяком натуральном $k \geqslant 1$
будем называть
\emph{столбцами (высоты $k$)}
элементы множества
$\underbrace{\{0,+,-\}\times\ldots\times\{0,+,-\}}_k$.
Столбцы будем записывать по вертикали, например:
$$
\begin{array}{|c|}
\hline
\hspace{1em}0\hspace{1em}\\
\hline
+\\
\hline
\end{array}
\qquad\qquad
\begin{array}{|c|}
\hline
\hspace{1em}-\hspace{1em}\\
\hline
+\\
\hline
-\\
\hline
0\\
\hline
\end{array}
$$
Всякое слово в алфавите столбцов высоты $k$
будем называть \emph{диаграммой высоты $k$}.
В диаграммах естественно выделяются
\emph{строки}~--- слова в алфавите $\{0,+,-\}$.

Пусть задан список из $k$ многочленов
от одной переменной с действительными коэффициентами.
Сейчас мы сопоставим с ним диаграмму высоты $k$.
Для этого сначала отметим на числовой прямой
корни всех ненулевых многочленов списка.
Пусть это $\xi_1,\ldots,\xi_n$.
Назов\"ем \emph{сегментом}
каждое из $2n+1$ множеств
$(-\infty,\xi_0)$, $\{\xi_0\}$, $(\xi_0,\xi_1)$,
$\ldots, \{\xi_n\}$, $(\xi_n,+\infty)$.
Возьм\"ем $i$-ый многочлен списка и выпишем
последовательно
его знаки на каждом из сегментов
(ясно, что внутри сегмента знак многочлена
из списка не меняется).
Полученное слово в алфавите $\{0,+,-\}$
и будет $i$-ой строкой
строящейся диаграммы.

Для произвольного списка $L$
многочленов от нескольких переменных
(с выделенной переменной $x$) определено понятие
\emph{замыкания} $\clos L$
этого списка относительно указанных
выше четыр\"ех операций.
Так как степень по $x$ результата применения
каждой операции строго меньше степеней по $x$
аргументов этой операции, то список,
являющийся замыканием конечного списка~--- конечен.
Назов\"ем \emph{основой} $\bas L$
замкнутого списка многочленов подсписок
этого списка,
образованный многочленами
нулевой степени по $x$.
Ясно, что по списку $L$ можно
эффективно построить $\clos L$ и
$\bas L$.
Будем обозначать длину списка $L$
через $\delta(L)$.

Для списка многочленов от переменных
$x$, $y_1,\ldots,y_l$
очевидно определяется понятие
диаграммы в точке $c_1,\ldots,c_l$:
полагаем
$y_1=c_1$, \ldots, $y_l=c_l$ и рассматриваем
диаграмму получающегося семейства многочленов
от $x$ с действительными коэффициентами.

Если список состоит из многочленов нулевой
по $x$ степени,
то его диаграмма в любой точке
имеет длину $1$.

\begin{main_lem}
Существует алгоритм, который
по произвольному списку $L$ многочленов от
$x$, $y_1,\ldots,y_l$
строит такое отображение,
перерабатывающее некоторый диаграммы
высоты $\delta(\bas L)$ и длины $1$
в диаграммы высоты $\delta(L)$,
что диаграмма $L$ в любой точке
$\vct c=(c_1,\ldots,c_l)$
есть образ при построенном
отображении диаграммы
$\bas L$ в точке $\vct c$.
\end{main_lem}
\begin{proof}
Прежде всего по списку многочленов $L$
построим его замыкание $\clos L$
и выделим в н\"ем $\bas L$.
Будем теперь по диаграмме для $\bas L$
(имея в виду, что это диаграмма
в некоторой неизвестной нам точке $\vct c$)
строить диаграмму для $\clos L$;
диаграмма для $L$ получится тривиально.

Построение будем вести постепенно,
в последовательности, обратной к построению замыкания,
то есть добавляя к списку многочлен
после того, как все многочлены из
замыкания, имеющие меньшую степень,
уже добавлены.

Итак, пусть диаграмма для списка $U$ уже
построена; как е\"е расширить до диаграммы списка $pU$?
Диаграмма списка $pU$ будет иметь
дополнительную строку внизу. Кроме того,
она будет содержать дополнительные столбцы,
по два на каждый корень многочлена $p$,
не являющийся корнем никаких многочленов из $U$
(которые в $\vct c$ не равны нулю тождественно по $x$).

Мы опишем лишь построение диаграммы.
Доказательство правильности предлагаемого
алгоритма элементарно. Заметим, что в списке $U$
содержится старший коэффициент многочлена $p$.
Пусть отвечающая ему строка диаграммы нулевая.
Тогда диаграмма для $pU$ получается из диаграммы
для $U$ приписыванием снизу строки,
отвечающей многочлену, получаемому из $p$
отбрасыванием старшего члена
(такая строка уже была где-то в диаграмме).

Далее будем предполагать, что старший коэффициент
многочлена $p$~--- ненулевой
(и нам известен его знак).
Начн\"ем с того, что добавим в диаграмму
снизу одну строку и заполним в ней клетки,
отвечающие одноточечным сегментам,
то есть найд\"ем знаки $p$ в корнях
многочленов из $U$. Это,
конечно, сделать нетрудно, используя операцию
модифицированного остатка, а именно,
деля многочлен $p$ на многочлен,
имеющий в данной точке корень.

Ключевыми соображениями теперь будут:
\begin{enumerate}
\item
строго между двумя корнями многочлена
имеется корень его производной;
\item
корень многочлена $p$, в котором $p$ не меняет знак,
является корнем его производной;
\item
между точками, в которых многочлен $p$ имеет знаки
$+$ и $-$, есть корень $p$.
\end{enumerate}
Исходя из этих соображений,
легко построить нужную процедуру,
но мы вс\"е же выпишем е\"е полностью.
Если в последней строке таблицы
оказалась пустая клетка, с которой соседствует
с одной стороны $+$,
а с другой стороны $+$ или $0$,
то ставим в эту клетку $+$.
Аналогично для $-$.
Зная знак старшего коэффициента $p$
и ч\"етность степени $p$,
находим знаки $p$ в $-\infty$ и $+\infty$.
Если крайний справа из поставленных знаков
в нижней строке есть $0$ или совпадает
со знаком $p$ в $+\infty$,
то заполняем последнюю клетку
нижней строки знаком $p$ в $+\infty$.
В противном случае заполняем эту клетку
тем же знаком, что и предыдущую,
и добавляем к диаграмме справа два столбца.
Эти столбцы, если отбросить в них
самый нижний элемент, совпадают
с последним стобцом в диаграмме для $U$.
В нижнюю строку этих столбцов заносим
слева $0$ и справа знак $p$ в $+\infty$.
Совершенно аналогично поступаем с
левым краем диаграммы
(который соответствует $-\infty$).

Почти так же добавляем столбцы внутрь диаграммы.
Именно, если в каком-то столбце $\gamma$
внизу стоит пустая клетка,
а по соседству с ней стоят
с одной стороны $+$,
а с другой стороны $-$,
то этот столбец заменяется на три.
Все элементы, кроме нижнего,
в этих столбцах те же, что у $\gamma$.
В нижней строке этих столбцов
среднюю клетку заполняем нул\"ем,
а каждую из крайних~--- тем знаком,
с которым она соседствует.
Лемма доказана.
\end{proof}

Объясним теперь, как проводить
элиминацию кванторов в рассматриваемой теории.
Пусть дана формула $\exists x\Phi$
(где $\Phi$~--- бескванторная).
Будем считать, что в $\Phi$
все атомные формулы приведены к одному из видов
$p>0$, $p=0$ или $p<0$.
Образуем список $L$ всех многочленов,
входящих в $\Phi$.
Заметим, что,
зная диаграмму списка $L$
в некоторой точке $\vct c$
и ничего больше не зная об этой точке,
мы можем сказать, истинна ли формула
$\exists x\Phi$ в этой точке.

Образуем замыкание $\clos L$,
найд\"ем основу $\bas L$.
Согласно лемме достаточно знать
диаграмму $\bas L$ в некоторой точке,
чтобы найти диаграмму $L$ в этой точке
(и, следовательно, определить,
истинна ли формула в ней).
Таким образом, истинность формулы $\exists x\Phi$
в точке $\vct c$ определяется знаками
некоторых многочленов, не содержащих $x$,
а именно, многочленов из $\bas L$.
Это позволяет заменить $\exists x\Phi$
эквивалентной бескванторной формулой.
Элиминируемость кванторов доказана.

\begin{thebibliography}{9}

\bibitem{tar}
A.~Tarsky.
A decision method for
elementary algebra and geometry.
Univ. of Calif. Press, Berkeley, 1948.

\bibitem{seiden}
A.~A.~Seidenberg.
A new decision method
for elementary algebra.
{\it Annals of Mathematics},
v.~60, 1954, pp.~365\nobreakdash--374.

\bibitem{cohen1}
P.~J.~Cohen.
Decision procedures for real and $p$-adic fields.
{\it Communications on Pure and Applied Mathematics},
v.~22, N~2, 1969, pp.~131\nobreakdash--151.

\bibitem{rabin}
M.~J.~Fischer, M.~O.~Rabin.
Super-exponential complexity
of Presburger arithmetic.
{\it Proc. AMS Symp. on Complexity
of Real  Computational Processes},
v.~7, 1974.

\bibitem{best}
M.~Ben-Or, D.~Kozen, J.~Reif.
The complexity of elementary algebra and geometry.
{\it Journal of Computer and System Sciences},
v.~32, 1986, pp.~251\nobreakdash--265.

\bibitem{sem}
А.~Л.~Семенов.
Разрешающие алгоритмы для логических теорий.
В сборнике:
{\it Кибернетика и вычислительная техника},
М., 1986, вып.~2, с.~134\nobreakdash--146.


\end{thebibliography}

\end{document}

