lection-15.tex

\documentclass[aspectratio=169]{beamer}
\usepackage[utf8]{inputenc}
\usepackage[english,russian]{babel}
\usepackage{cancel}
\usepackage{amssymb}
\usepackage{stmaryrd}
\usepackage{cmll}
\usepackage{graphicx}
\usepackage{amsthm}
\usepackage{tikz}
\usepackage{multicol}
\usetikzlibrary{patterns}
\usepackage{chronosys}
\usepackage{proof}
\usepackage{multirow}
\usepackage{comment}
\setbeamertemplate{navigation symbols}{}
%\usetheme{Warsaw}

\newtheorem{thm}{Теорема}[section]
\newtheorem{dfn}{Определение}[section]
\newtheorem{lmm}{Лемма}[section]
\newtheorem{exm}{Пример}[section]
\newtheorem{snote}{Пояснение}[section]

\newcommand{\divisible}%
{\mathrel{\lower.2ex%
\vbox{\baselineskip=0.7ex\lineskiplimit=0pt%
\kern6pt \hbox{.}\hbox{.}\hbox{.}}%
}}

\begin{document}

\newcommand\doubleplus{+\kern-1.3ex+\kern0.8ex}
\newcommand\mdoubleplus{\ensuremath{\mathbin{+\mkern-10mu+}}}

\begin{frame}{}
\begin{center}\Large Метод резолюций \end{center}
\end{frame}

\begin{frame}{Разрешимость исчислений}
\footnotesize{\flushright <<Извини, Теодор, но это ты очень странно рассуждаешь. Бессмыслица — искать решение, если оно и так есть. 
Речь идет о том, как поступить с задачей, которая решения не имеет. 
Это глубоко принципиальный вопрос, который, как я вижу, тебе, прикладнику, к сожалению, не доступен.>>

\vspace{0.3cm}
А. и Б. Стругацкие, <<Понедельник начинается в субботу>>}

\vspace{1cm}\pause

\normalsize


\begin{itemize}
\item Разрешимы: КИВ, ИИВ.
\item Неразрешимы: всё остальное (ИП, ФА, ZF(C), ...)
\end{itemize}

\pause

\vspace{0.5cm}
\noindent Однако, (1) разрешимости хочется \pause и (2) человек как-то умеет.

%Разрешимы & Неразрешимы\\\hline
%КИВ, ИИВ & всё остальное (ИП, ФА, ...)
%\end{tabular}\end{center}
\end{frame}

\begin{frame}{Ищем доказательство в исчислении предикатов: упрощение задачи}

\begin{itemize}
\item По теореме о полноте можем рассматривать $(\models)$ вместо $(\vdash)$. 
Напомним: $\models \alpha$, если для всех $M = \langle D, F, P, E \rangle$ выполнено $M \models \alpha$.\pause
\vspace{0.3cm}

\item Что мешает:
\begin{enumerate}
\item слишком сложные формулы --- кванторы по бесконечным множествам;
\item слишком большое разнообразие $D$, включая несчётные;
\item даже $D = \mathbb{N}$ в формальной арифметике представляет проблему.
\end{enumerate}\pause
\vspace{0.3cm}

\item Будем последовательно бороться:
\begin{enumerate}
\item упростим формулу (борьба с кванторами);
\item заменим произвольное $D$ на какое-то рекурсивно-перечислимое множество, устроенное некоторым фиксированным образом (борьба с разнообразием $D$);
\item устроим правильный перебор, позволяющий быстро находить решения, если они есть (борьба с бесконечностью $D$).
\end{enumerate}
\end{itemize}
\end{frame}


\begin{frame}{Упрощаем формулу $\alpha$. Сколемизация}
\begin{enumerate}
\item Предварённая форма (поверхностные кванторы) --- \emph{для примера} возьмём чередующиеся:
$$\beta := \forall x_1.\exists x_2.\forall x_3.\exists x_4\dots \forall x_{n-1}.\exists x_n.\varphi$$

%\item Для упрощения предполагаем, что кванторы чередуются.
%Это не сильно уменьшает общность. Например, если $D = \mathbb{N}$,
%то $(\forall x.\forall y.\varphi(x,y)) \leftrightarrow (\forall p.\varphi(\text{plog}_2(p),\text{plog}_3(p))$

\item Убрать кванторы существования: заменим $x_{2k}$ функциями Сколема $e_{2k}(x_1,x_2,\dots,x_{2k-1})$.
Получим: $$\gamma := \forall x_1.\forall x_3\dots\forall x_{n-1}.\varphi[x_2:=e_2(x_1), x_4:=e_4(x_1,x_3), \dots, x_n := e_n(x_1,x_3,\dots,x_{n-1})]$$


\item КНФ ($c$ конъюнктов, в каждом $d(c)$ дизъюнктов):
$$\delta := \forall x_1.\forall x_3\dots\forall x_{n-1}.\bigwedge_c\left(\bigvee_{i = \overline{1,d(c)}} (\neg)P_i(\theta_i)\right)$$

\item $\vdash\alpha$ эквивалентно $\models\alpha$ и эквивалентно выполнимости $\delta$ при всех $D$ 
(найдутся $e_i$, что $\llbracket\delta\rrbracket = \text{И}$).

\end{enumerate}
\end{frame}

\begin{frame}{Шаги рассуждения}
\begin{enumerate}
\item \color{gray}Упростим формулу --- поверхностные кванторы всеобщности, сколемизация.
\item \color{black}Заменяем $D$.
\item \color{gray}Правильный перебор
\end{enumerate}
\end{frame}


\begin{frame}{Эрбранов универсум.}
\begin{dfn}$H_0(\varphi)$ --- все константы в формуле $\varphi$ (либо особая константа $a$, если констант в $\varphi$ нет)\\
$H_{k+1}(\varphi)$ --- $H_k(\varphi)$ и все функции от значений $H_k(\varphi)$ (как строки)\\

$H = \cup H_n(\varphi)$ --- основные термы.
\end{dfn}

\begin{exm}$P(a)\vee Q(f(b))$: \\
$H_0 = \{a,b\}$\\
$H_1 = \{a,b,f(a),f(b)\}$\\
$H_2 = \{a,b,f(a),f(b),f(f(a)),f(f(b))\}$\\
$\dots$\\
$H = \{f^{(n)}(x)\ |\ n \in \mathbb{N}_0, x \in \{a,b\}\}$\end{exm}
\end{frame}

\begin{frame}{Выполнимость не теряется. Заменяем $D$ на $H$}
\begin{thm}Формула выполнима тогда и только тогда, когда она выполнима на Эрбрановом универсуме.\end{thm}
\begin{proof}
$(\Rightarrow)$ Пусть $M \models\forall \overline{x}.\varphi$. Тогда построим отображение $\text{eval}: H \rightarrow M$
(смысл названия вдохновлён языками программирования: $\text{eval}(``f(f(b))``)$ перейдёт в $f(f(b))$, где $f$ и $b$ --- из $M$).

Предикатам дадим согласованную оценку:
$P_H(t_1,\dots,t_n) = P_M(h(t_1),\dots,h(t_n))$. Очевидно, любая формула сохранит своё значение, кванторы всеобщности
по меньшему множеству также останутся истинными.

$(\Leftarrow)$ Очевидно.
\end{proof}\end{frame}

\begin{frame}{Противоречивость системы дизъюнктов}
\begin{dfn}Система дизъюнктов $\{\delta_1,\dots,\delta_n\}$ противоречива,
если для каждой интерпретации $M$ найдётся $\delta_k$ и такой набор $d_1\dots d_v$,
что $\llbracket\delta_k\rrbracket^{x_1 := d_1, \dots, x_v := d_v} = \text{Л}$.\end{dfn}
\begin{thm}Система дизъюнктов противоречива, если она невыполнима на Эрбрановом универсуме.\end{thm}
\begin{proof}Контрапозиция теоремы о выполнимости + разбор определения.
\end{proof}
\end{frame}


\begin{frame}{Основные примеры.}
\begin{dfn}
Дизъюнкт с подставленными основными термами вместо переменных называется основным примером.
Системой основных примеров $\mathcal{E}$ назовём множество основных примеров.

А именно, рассмотрим $\delta_1\with\delta_2\with\dots\with\delta_n$. 
$$\mathcal{E} = \{ \text{ все возможные основные примеры }\delta_k\ |\ \mathcal{M} \not\models \delta_k, \mathcal{M}\text{ из H }\}$$
\end{dfn}\vspace{-0.5cm}
\begin{thm}Система дизъюнктов $S$ противоречива тогда и только тогда, когда система всевозможных
основных примеров $\mathcal{E}$ противоречива\end{thm}
\begin{proof}Для некоторой эрбрановой интерпретации дизъюнкт $\delta_k$
опровергается тогда и только тогда, когда соответствующая ему подстановка в $\mathcal{E}$ опровергается.
\end{proof}\end{frame}

\begin{comment}
\begin{frame}{Компактность}
\begin{dfn} 
Пространство $X$ компактно, если из любого его открытого покрытия $U$ можно выделить конечное подпокрытие:

$X = \cup U$, существует $V \subseteq U$, что $|V| < \aleph_0$ и $X = \cup V$.
\end{dfn}

\begin{exm}
$(0,1)$ не компактен. Например, $U = \{(\varepsilon/2,\varepsilon)\ |\ \varepsilon\in(0,1)\}$.
Пусть $V \subset U$ и $|V| < \aleph_0$. Тогда $\min \{ a\ |\ (a,b) \in V \} > 0$.
\end{exm}

\begin{exm}
$[0,1]$ компактен. Выберем $U$ и покажем, что в нём есть подпокрытие.
Рассмотрим все подотрезки вида $[a,x]$ где $a < x$, имеющие конечное покрытие.
Несложно показать, что $\max x = 1$.
\end{exm}
\end{frame}
\end{comment}

\begin{frame}{Теорема Гёделя о компактности}
\begin{thm}Если $\Gamma$ --- некоторое семейство бескванторных формул, то $\Gamma$ имеет модель
тогда и только тогда, когда любое его конечное подмножество имеет модель.\end{thm}
\begin{proof}
$(\Rightarrow)$: очевидно

$(\Leftarrow)$: пусть каждое конечное подмножество имеет модель. Тогда $\Gamma$ непротиворечиво:

{\footnotesize Иначе, для любой $\sigma$ выполнено $\Gamma\vdash\sigma$. В частности, для $\gamma\in\Gamma$
выполнено $\Gamma\vdash\neg\gamma$. Доказательство имеет конечную длину, и использует конечное
количество формул $\gamma_1,\dots,\gamma_n\in\Gamma$. Тогда рассмотрим $\Sigma = \{\gamma,\gamma_1,\dots,\gamma_n\}$, 
и модель $\mathcal{S}$ для неё. Тогда:
\begin{enumerate}
\item $\models_{S}\gamma$ (определение модели)
\item $\models_{S}\neg\gamma$ (теорема о корректности: $\Sigma\vdash\neg\gamma$, значит $\Sigma\models\neg\gamma$ в любой модели)
\end{enumerate}}

Значит, $\Gamma$ имеет модель (вспомогательная теорема к теореме Гёделя о полноте).
\end{proof}
\end{frame}

\begin{frame}{Теорема Эрбрана}
\begin{thm}[Эрбрана]Система дизъюнктов $S$ противоречива тогда и только тогда, когда существует
конечное противоречивое множество основных примеров системы дизъюнктов $S$\end{thm}
\begin{proof}$(\Leftarrow)$ 
Пусть $\delta_1[\overline{x} := \overline{\theta}],\dots,\delta_k[\overline{x} := \overline{\theta}]$ 
--- противоречивое множество примеров дизъюнктов. Тогда интерпретация $\overline{\theta}$
опровергает хотя бы один из $\delta_k$ и система противоречива.

$(\Rightarrow)$ Если $S$ противоречива, то значит, множество основных примеров $S$
противоречиво (по теореме о выполнимости Эрбранова универсума). Тогда по теореме компактности
в нём найдётся конечное противоречивое подмножество.
\end{proof}
\end{frame}

\begin{frame}{Шаги рассуждения}
\begin{enumerate}
\item \color{gray}Упростим формулу --- поверхностные кванторы всеобщности, сколемизация.
\item Упрощаем $D$ --- заменили на $H$, свели к перебору основных примеров.
\item \color{black}Правильный перебор.
\end{enumerate}
\end{frame}

\begin{frame}{Пример: как проверяем выполнимость формулы?}
Допустим, формула: $(\forall x.P(x)\with P(x')) \with \exists x.\neg P(x'''')$

\begin{enumerate}
\item Поверхностные кванторы, сколемизация, ДНФ: $(\forall x.P(x)) \with (\forall x.P(x')) \with (\neg P(e))$
\item Строим Эрбранов универсум: $H = \{e, e', e'', e''', \dots \}$
\item Если есть противоречие, то среди основных примеров:
$$\mathcal{E} = \{ P(e), P(e'), P(e''), P(e'''), P(e''''), \neg P(e''''), \dots \}$$
\end{enumerate}

Напомним, $\mathcal{E}$ --- подстановки элементов $H$ вместо переменных под кванторами.
Причём, либо $\models\bigwith E$, либо противоречие достигается на конечном подмножестве (т. Эрбрана).

Добавляем по примеру и проверяем.
$P(e)$ при $\llbracket P(e) \rrbracket  = \text{И}$.

$P(e')$ при $\llbracket P(e') \rrbracket = \text{И}$.

...

$P(e'''')$ при $\llbracket P(e'''') \rrbracket = \text{И}$.

$\neg P(e'''')$ при $\llbracket P(e'''') \rrbracket = \text{Л}$. Противоречие.

\end{frame}

\begin{frame}{Правило резолюции (исчисление высказываний)}
Пусть даны два дизъюнкта, $\alpha_1 \vee \beta$ и $\alpha_2 \vee \neg \beta$.
Тогда следующее правило вывода называется правилом резолюции:

$$\infer{\alpha_1\vee \alpha_2}{\alpha_1\vee \beta\quad\quad \alpha_2\vee\neg \beta}$$

\begin{thm}Система дизъюнктов противоречива, если в процессе всевозможного применения
правила резолюции будет построено явное противоречие,
т.е. найдено два противоречивых дизъюнкта: $\beta$ и $\neg\beta$.
\end{thm}
\end{frame}

\begin{frame}{Расширение правила резолюции на исчисление предикатов}
Заметим, что правило резолюции для исчисления высказываний не подойдёт для исчисления предикатов.

$$S = \{ P(x), \neg P(0)\}$$

Здесь $P(x)$ противоречит $\neg P(0)$, но правило резолюции для исчисления высказываний здесь неприменимо, потому
что $x$ можно заменять, это не константа:
%$\beta \equiv P(x)$, тогда $\neg \beta \not\equiv \neg P(0)$.

$$\infer{???}{P({\color{red}x})\quad\quad\neg P({\color{red}0})}$$

Нужно заменять $P(x)$ на основные примеры, и искать среди них. Модифицируем правило резолюции для этого.

\end{frame}

\begin{frame}{Алгебраические термы}
	\begin{dfn}Алгебраический терм $$\theta := x\:|\:(f(\theta_1,\ldots,\theta_n))$$ 
где $x-$переменная, $f(\theta_1,\ldots,\theta_n)-$применение функции. Напомним, что константы --- нульместные
функциональные символы, собственно переменные будем обозначать последними буквами латинского алфавита. \end{dfn}
	%\subsection{Уравнение в алгебраических термах $\theta_1=\theta_2$\\Система уравнений в алгебраических термах}
	\begin{dfn}Система уравнений в алгебраических термах
	$
		\begin{cases}
			\theta_1=\sigma_1&\\
			\vdots&\\
			\theta_n=\sigma_n&\\
		\end{cases}
	$\par где $\theta_i \text{ и } \sigma_i-\text{термы}$\par
\end{dfn}
\end{frame}
\begin{frame}{Уравнение в алгебраических термах}
	\begin{dfn}$\{x_i\}=X-$множество переменных, $\{\theta_i\}=T-$множество термов.\end{dfn}
	\begin{dfn}Подстановка$-$отображение вида: $\pi_0:X\to T$, тождественное почти везде.
        \par $\pi_0(x)$ может быть либо $\pi_0(x)=\theta_i\text{, либо }\pi_0(x)=x$.\end{dfn} 
	Доопределим $\pi:T\to T$, где \begin{enumerate}
		\item $\pi(x)=\pi_0(x)$
		\item $\pi(f(\theta_1, \ldots, \theta_k))=f(\pi(\theta_1), \ldots, \pi(\theta_k))$
	\end{enumerate}
	
	\begin{dfn}Решить уравнение в алгебраических термах$-$найти такую наиболее общую подстановку $\pi$, 
        что $\pi(\theta_1)=\pi(\theta_2)$.
Наиболее общая подстановка --- такая, для которой другие подстановки являются её частными случаями.\end{dfn} 
\end{frame}

\begin{frame}{Задача унификации}
\begin{dfn}
Пусть даны формулы $\alpha$ и $\beta$. Тогда решением задачи унификации
будет такая наиболее общая подстановка $\pi = \mathcal{U}\big[\alpha,\beta\big]$, что $\pi(\alpha) = \pi(\beta)$.

%Будем писать $\Sigma = \mathcal{U}\[\alpha,\beta\]$, если $\Sigma(\alpha) = \Sigma(\beta) = \eta$ и $\Sigma$ --- наиболее общая.
Также, $\eta$ назовём наиболее общим унификатором.
\end{dfn}

\begin{exm}
\begin{itemize}
%\item $\mathcal{U}\[ P(x,g(b)),P(f(a),y) \] = [ x := f(a), y := f(b) ]$ 
%и $P(f(a),g(b))$ --- унификатор.
\item Формулы $P(a,g(b))$ и $P(c,d)$ не имеют унификатора (мы считаем, что $a,b,c,d$ --- нульместные функции, а
$f$ --- одноместная функция).

\item Проверим формулу на соответствие 11 схеме аксиом: $$(\forall x.P(x))\rightarrow P(f(t,g(t),y))$$
Пусть $\pi = \mathcal{U}\big[P(x),P(f(t,g(t),y))\big]$, тогда $\pi(x) = f(t,g(t),y)$.
\end{itemize}
\end{exm}
\end{frame}

\begin{frame}{Правило резолюции для исчисления предикатов}
\begin{dfn}
Пусть $\sigma_1$ и $\sigma_2$ --- подстановки, заменяющие переменные в формуле на свежие. 
Тогда правило резолюции выглядит так:

$$\infer[{\pi = \mathcal{U}\big[\sigma_1(\beta_1),\sigma_2(\beta_2)\big]}]
        {\pi(\sigma_1(\alpha_1)\vee \sigma_2(\alpha_2))}
        {\alpha_1\vee \beta_1\quad\quad\alpha_2\vee\neg \beta_2}$$
\end{dfn}

$\sigma_1$ и $\sigma_2$ разделяют переменные у дизъюнктов, чтобы $\pi$ не осуществила лишние
замены, ведь $\vdash(\forall x.P(x) \with Q(x)) \leftrightarrow (\forall x.P(x))\with(\forall x.Q(x))$, но
$\not\vdash (\forall x.P(x) \vee Q(x)) \rightarrow (\forall x.P(x))\vee(\forall x.Q(x))$.

\begin{exm}\vspace{-0.5cm}
$$\infer[\text{ подстановки: } \sigma_1(x) = x', \sigma_2(x) = x'', \pi(x')=a]{Q(a)\vee T(x'')}{Q(x)\vee P(x) \quad \neg P(a)\vee T(x)}$$
\end{exm}
\end{frame}

\begin{frame}{Метод резолюции}
Ищем $\vdash\alpha$.

\begin{enumerate}
\item будем искать опровержение $\neg\alpha$.
\item перестроим $\neg\alpha$ в ДНФ.
\item будем применять правило резолюции, пока получаем новые дизъюнкты и пока 
не найдём явное противоречие (дизъюнкты вида $\beta$ и $\neg\beta$).
\end{enumerate}

Если противоречие нашлось, значит, $\vdash\neg\neg\alpha$. Если нет --- значит, $\vdash\neg\alpha$.
Процесс может не закончиться.
\end{frame}

\begin{frame}{SMT-решатели}

Обычно требуется не логическое исчисление само по себе, а теория первого порядка.
То есть, <<Satisfability Modulo Theory>>, <<выполнимость в теории>> --- вместо SAT, выполнимости.
\begin{itemize}
\item Иногда можно вложить теорию в логическое исчисление, 
даже в исчисление высказываний: $\overline{S_2S_1S_0} = \overline{A_1A_0}+\overline{B_1B_0}$
$$\begin{array}{ll}
S_0 = A_0 \oplus B_0 & C_0 = A_0 \with B_0\\
S_1 = A_1 \oplus B_1 \oplus C_0 & C_1 = (A_1 \with B_1) \vee (A_1 \with C_0) \vee (B_1 \with C_0) \\
S_2 = C_1\end{array}$$

\item А можно что-то добавить прямо на уровень унификации / резолюции:
Например, можем зафиксировать арифметические функции --- и производить вычисления
в правиле резолюции вместе с унификацией.

Тогда противоречие в $\{x = 1+3+1,\neg x = 5\}$ можно найти за один шаг.
\end{itemize}
\end{frame}

\begin{frame}[fragile]{Уточнённые типы (Refinement types), LiquidHaskell}
\begin{dfn}(Неформальное) Уточнённый тип --- тип вида $\{\tau(x)\ |\ P(x)\}$, где $P$ --- некоторый предикат.\end{dfn}

Пример на LiquidHaskell:
\begin{verbatim}
data [a] <p :: a -> a -> Prop> where
   | []  :: [a] <p>
   | (:) :: h:a -> [a<p h>]<p> -> [a]<p>
\end{verbatim}
\begin{itemize}
\item \verb!h:a! --- голова ($h$) имеет тип $a$\\
\item \verb![a<p h>]<p>! --- хвост состоит из значений типа $a$, уточнённых $p$ --- $\{ t : a\ |\ p\ h\ t\}$ (карринг: \verb!a <p h>!).
\end{itemize}

\begin{verbatim}
{-@ type IncrList a = [a] <{\xi xj -> xi <= xj}> @-}
{-@ insertSort    :: (Ord a) => xs:[a] -> (IncrList a) @-}
insertSort []     = []
insertSort (x:xs) = insert x (insertSort xs) 
\end{verbatim}
\end{frame}


\end{document}