-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathdiploma.tex
321 lines (293 loc) · 33.7 KB
/
diploma.tex
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
% Тут используется класс, установленный на сервере Papeeria. На случай, если
% текст понадобится редактировать где-то в другом месте, рядом лежит файл matmex-diploma-custom.cls
% который в момент своего создания был идентичен классу, установленному на сервере.
% Для того, чтобы им воспользоваться, замените matmex-diploma на matmex-diploma-custom
% Если вы работаете исключительно в Papeeria то мы настоятельно рекомендуем пользоваться
% классом matmex-diploma, поскольку он будет автоматически обновляться по мере внесения корректив
%
% По умолчанию используется шрифт 14 размера. Если нужен 12-й шрифт, уберите опцию [14pt]
\documentclass[14pt]{matmex-diploma}
\usepackage{algorithm}
\usepackage[noend]{algpseudocode}
\usepackage{amsthm}
\usepackage{amssymb}
\usepackage{amsmath}
\usepackage{hyperref}% http://ctan.org/pkg/hyperref
\usepackage{cleveref}% http://ctan.org/pkg/cleveref
%\documentclass[14pt]{matmex-diploma-custom}
\theoremstyle{definition}
\floatname{algorithm}{Алгоритм}
\newtheorem{definition}{Определение}
\newtheorem{theorem}{Теорема}
\newtheorem{lemma}{Лемма}
\newtheorem{corollary}{Следствие}
\crefname{lemma}{Лемме}{Леммы}
\newcommand{\overtext}[2]{\ensuremath{\stackrel{\mathrm{#1}}{\mathrm{#2}}}}
%\newtheorem{proof}{Доказательсво}
\begin{document}
% Год, город, название университета и факультета предопределены,
% но можно и поменять.
% Если англоязычная титульная страница не нужна, то ее можно просто удалить.
\filltitle{ru}{
chair = {Кафедра системного программирования},
title = {Поиск кратчайшего пути с контекстно-свободными ограничениями в помеченном графе},
% Здесь указывается тип работы. Возможные значения:
% coursework - Курсовая работа
% diploma - Диплом специалиста
% master - Диплом магистра
% bachelor - Диплом бакалавра
type = {coursework},
position = {студента},
group = 344,
author = {Антополь Валерий Алексеевич},
supervisorPosition = {ст. преп.\,к. ф.-м. н.},
supervisor = {Григорьев С.\,В.},
%reviewerPosition = {ст. преп.},
%reviewer = {Привалов А.\,И.},
%chairHeadPosition = {д.\,ф.-м.\,н., профессор},
%chairHead = {Хунта К.\,Х.},
% university = {Санкт-Петербургский Государственный Университет},
% faculty = {Математико-механический факультет},
% city = {Санкт-Петербург},
% year = {2013}
}
%\filltitle{en}{
% chair = {The Meaning of Life \\ Uselessness of Everything},
% title = {Empty subset as closed set},
% author = {Edelweis Mashkin},
% supervisorPosition = {professor},
% supervisor = {Amvrosy Vibegallo},
% reviewerPosition = {assistant},
% reviewer = {Alexander Privalov},
% chairHeadPosition = {professor},
% chairHead = {Christobal Junta},
%}
\maketitle
\tableofcontents
% У введения нет номера главы
\section*{Введение}
Структуры данных на основе графов часто используются в различных областях, например, в биоинформатике, логистике, графовых базах данных, в языках программирования. Одна из таких структур --- это граф, каждому ребру которого сопоставляется символ из некоторого конечного алфавита $\Sigma$. Такой граф называется помеченным.
Для того, чтобы получить информацию из графа, нужно выполнять запросы, задающие класс путей в графе. Пути рассматриваются в виде строки из меток на ребрах. Такие запросы удобно представлять в виде грамматики: путь удовлетворяет запросу, если он принадлежит языку, который порождает заданная грамматика. Часто результатом запроса должно являться отношение на вершинах графа: если (n, m) принадледжит отношению, то существует путь из n в m, который распознается грамматикой. Это называется задачей достижимости с контекстно-свободными ограниениями.
В некоторых областях, например, в логистике, недостаточно найти какой-либо путь (или его существование) между парой вершин, нужно найти кратчайший (или его длину). Существуют различные алгоритмы поиска кратчайшего пути в графе с контекстно-свободными ограничениями. Но некоторые из них требуют отсутствия отрицательных весов~\cite{Barrett} или ацикличности графа~\cite{p2pdyck}.
В 2017 году был предложен алгоритм решения задачи достижимости в произвольном помеченном графе с контекстно-свободными ограничениями~\cite{DBLP:journals/corr/AzimovG17}. Его особенность в том, что большая часть необходимих вычислений - это перемножение матриц, поэтому он легко параллелится на GPGPU~(General-Purpose computing on
Graphics Processing Units).
В данной работе описывается модификация этого алгоритма для решения задачи поиска кратчайшйх путей между каждой парой вершин с контекстно-свободными ограничениями. В отличие от других алгоритов, эта модификация имеет слабые ограничения: единственное условие на граф --- отсутствие циклов отрицательного веса.
%Помеченный граф - это граф, каждому ребру которого сопоставляется символ из некоторого алфавита $\Sigma$.
%\theoremstyle{definition}
%\begin{definition}
% $(min, +)$-произведение двух числовых матриц $A$, $B$ - это %числовая матрица C, такая что $C_{i,j} = min_k\{A_{i,k} %+ B_{k,j}\}$
%\end{definition}
\section{Постановка задачи}
Целью данной работы является модификация алгоритма решения задачи достижимости с контекстно-свободными ограничениями в помеченном графе~\cite{DBLP:journals/corr/AzimovG17} для решения задачи поиска кратчайшйх путей между каждой парой вершин с контекстно-свободными ограничениями. Для достижения данной цели были поставлены следующие задачи:
\begin{itemize}
\item создать модификацию алгоритма;
\begin{itemize}
\item доказать корректность;
\item дать оценку времени работы;
\end{itemize}
\item провести экспериментальное исследование модифицированного алгоритма.
\end{itemize}
\section{Обзор}
\subsection{Fast-BJM}
Алгоритм использует методы динамического программирования и очередь с приоритетами, за счет этого достигается время работы $O(|V|^3|N||P|)$, где $V$ --- множество ребер в графе, $N$ --- множество нетерминалов в грамматике, $P$ - множество правил вывода в грамматике. Не работает с ребрами отрицательного веса, также в графе не должно быть петель.
Существует модификация этого алгоритма, позволяющая распараллеливание~\cite{D-Fast-BJM}. При распараллеливании на $|V|$ узлов каждый узел завершит работу за время $O(|V|^2|N||P|)$.
Также существует модификация, имеющая ту же временную сложность, что и оригинальный алгоритм, но позволяющая работать с ребрами отрицательного веса~\cite{Johnson-Fast-BJM}.
\subsection{Fast Bounded-Difference Min-Plus Product}
Этот алгоритм решает задачу, близкую к задаче поиска кратчайших путей с контекстно-свободными ограничениями.
Отличие состоит в том, что вес есть не у ребер графа, а у правил вывода в грамматике~\cite{DBLP:journals/corr/BringmannGSW17}.
Он состоит из построения транзитивного замыкания графа с помощью произведения матриц~\cite{VALIANT1975308}, в котором операции над элементами матрицы взяты из $(min, +)$-произведения.
За счет введения дополнительных ограничений на элементы перемножаемых матриц получается достичь $O(|V|^{2.8603})$ времени работы.
\subsection{Context-Free Path Querying by Matrix Multiplication}
В этой статье предложили алгоритм решения задачи достижимости с контекстно-свободными ограничениями с использованием транзитивного замыкания графа~\cite{VALIANT1975308}. Также в этой статье модифицировали алгоритм построения транзитивного замыкания, уменьшив объем вычислений. Именно этот алгоритм решения задачи достижимости и будет модифицироваться в данной работе.
\section{Модификация}
\subsection{Исходный алгоритм}
Пусть $(S, N,T,P)$ --- контекстно-свободная грамматика в нормальной форме Хомского, где $N$ --- множество нетерминалов, $T$ --- множество терминалов, $P$ --- множество правил вывода, $S$ --- стартовый нетерминал.\\
Пусть $(V,E)$ --- помеченный ориентированный мультиграф, где $V$ --- множество вершин, $E \subset V \times T \times V$ --- множество рёбер.\\
Алгоритм состоит в построении транзитивного замыкания матрицы смежности графа, определяемой специальным образом.
Элементами такой матрицы являются подмножества $N$. Пусть $a$ --- матрица смежности графа. Тогда если $A\in a_{i,j}$, то существует $i\pi j$ такой, что $w(\pi)\in~L(G_A)$, где $i\pi j$ --- путь в графе из вершины $i$ в вершину $j$, $w(\pi)$ --- слово, образуемое метками на пути $\pi$, $L(G)$ --- язык порожденный грамматикой $G$, $G_A$ --- грамматика, получающаяся из $G$ заменой стартового нетерминала на $A$.
Введем операции на $N_1$ и $N_2$ --- произвольных подмножествах $N$:
\begin{equation*}
N_1 \times N_2 = \{A~|~\exists B \in N_1,~\exists C \in N_2 : A \rightarrow BC \in P\}
\end{equation*}
\begin{equation*}
N_1 + N_2 = N_1 \cup N_2
\end{equation*}
Транзитивное замыкание матрицы $a$ определяется как $a^{cf} = \sum\limits_{i=1}^\infty a^{(i)}$,
где
\begin{equation*}
a^{(i)} =
\begin{cases}
a, & i=1\\
a^{(i-1)} + a^{(i-1)}\times a^{(i-1)}, & i>1
\end{cases}
\end{equation*}
Для транзитивного замыкания матрицы $a$ доказано~\cite{DBLP:journals/corr/AzimovG17} следующее:\\
$A\in~a^{cf}_{i,j}$ тогда и только тогда, когда существует $i\pi j$ такой, что $w(\pi)\in~L(G_A)$.
\begin{algorithm}[H]
\begin{algorithmic}[1]
\caption{Решение задачи достижимости}
\label{alg:graphParse}
\Function{contextFreePathQuerying}{D - граф, G - грамматика}
\State{$n \gets$ количество вершин в $D$}
\State{$E \gets$ множество ребер в $D$}
\State{$P \gets$ множество правил вывода в $G$}
\State{$T \gets$ матрица размера $n \times n$, в которой каждый элемент равен $\varnothing$}
\ForAll{$(i,x,j) \in E$}
\Comment{Инициализация матрицы}
\State{$T_{i,j} \gets T_{i,j} \cup \{A~|~(A \rightarrow x) \in P \}$}
\EndFor
\While{матрица $T$ меняется}
\State{$T \gets T \cup (T \times T)$}
\Comment{Вычисление транзитивного замыкания $T$}
\EndWhile
\State \Return $T$
\EndFunction
\end{algorithmic}
\end{algorithm}
\subsection{Модифицированный алгоритм}
Множество ребер графа теперь является подмножеством $V \times T \times V \times \mathbb{R}$ --- у ребер появляется вес. Элементами используемой матрицы являются функции такого типа: $a_{i,j}: N\rightarrow\mathbb{R}\cup\{\infty\}$.\\
Элементами используемой матрицы являются подмножества: $N\times(\mathbb{R}\cup\{\infty\})$.\\
На элементах матрицы водятся следующие операции:
\begin{equation*}
(N_1 \times N_2)(A) = \min\{N_1(B) + N_2(C)~|~A \rightarrow BC \in P\}
\end{equation*}
\begin{equation*}
(N_1 + N_2)(A) = \min\{N_1(A), N_2(A)\}
\end{equation*}
Это в точности $(min, +)$-произведение.
$a^i$ и $a^{cf}$ определяются как в исходном алгоритме, но с новыми операциями $(+)$ и $(\times)$.
\begin{algorithm}[H]
\begin{algorithmic}[1]
\caption{Решение задачи поиска кратчайших путей}
\label{alg:graphParseShortest}
\Function{contextFreePathQuerying}{D - граф, G - грамматика}
\State{$n \gets$ количество вершин в $D$}
\State{$E \gets$ множество ребер в $D$}
\State{$P \gets$ множество правил вывода в $G$}
\State{$T \gets$ матрица размера $n \times n$, $T_{i,j}(A) = \infty$}
\ForAll{$(i,x,j,w) \in E$}
\Comment{Инициализация матрицы}
\ForAll{$A~|~(A\rightarrow x) \in P$}
\State{$T_{i,j}(A) \gets \min{(T_{i,j}(A),w})$}
\EndFor
\EndFor
\While{матрица $T$ меняется}
\State{$T \gets T + (T \times T)$}
\Comment{Вычисление транзитивного замыкания $T$ и поиск кратчайших путей}
\EndWhile
\State \Return $T$
\EndFunction
\end{algorithmic}
\end{algorithm}
\subsection{Доказательство корректности}
\subsubsection{Используемые обозначения}
Запись $i\pi j$ означает, что $\pi$ --- это путь в графе от вершины $i$ к вершине $j$.\\
$l(\pi)$ --- слово, образуемое конкатенацией меток на ребрах, входящих в путь $\pi$ в порядке прохождения.\\
$w(\pi)$ --- длина пути $\pi$, то есть сумма весов входящих в него ребер.
Путь $\pi$ называется подходящим для пары (A, k), если cуществует дерево вывода высоты $h\le k$ для строки $l(\pi)$ в $G_A=(N,\Sigma, P, A)$. Заметим, что если $\pi$ подходящий для пары $(A, k)$ то он также подходящий для пары $(A, n)$, где $n > k$.
\begin{lemma}
\label{le_any}
Пусть $D=(V,E)$ --- граф, $G=(N,\Sigma, P, S)$ --- контекстно-свободная грамматика в нормальной форме Хомского. Тогда, для любых $i$, $j$, $k$ и нетерминала $A\in N$
верно следующее: $a^k_{i,j}(A) \le w(\pi)$ для любого пути $i\pi j$ подходящего для пары $(A, k)$.
\end{lemma}
\begin{proof}
По индукции.\\
\textbf{База:} по построению $a^1$ = $a$. Все деревья вывода высоты 1 соотвествуют каждое своему ребру.\\
\textbf{Переход:} Пусть p > 1. Предположим, что утверждение леммы выполняется для $k < p$. Рассмотрим $a^p_{i,j}(A)$.По определениям операций $(\times)$, $(+)$ и умножения матриц:
\begin{equation}\label{apply_plus}
a^p_{i,j}(A) = min(a^{p-1}_{i,j}(A), (a^{p-1}\times a^{p-1})_{i,j}(A))
\end{equation}
\begin{equation}\label{apply_times}
(a^{p-1}\times a^{p-1})_{ij}(A) = \min_{r,A,B}\{a^{p-1}_{ir}(B) + a^{p-1}_{rj}(C)~|~\exists A\rightarrow BC \in P\}
\end{equation}
По индукционному предположению $a^{p-1}_{i,j}(A) \le w(\pi)$ для всех подходящих паре $(A, p-1)$ путей $i\pi j$. Из этого и \eqref{apply_plus} следует, что $a^p_{i,j}(A) \le w(\pi)$ для всех $i\pi j$, подходящих $(A, p-1)$.
Далее необходимо показать, что неравенство верно также и для путей, подходящих $(A, p)$, но не подходящих $(A, p-1)$. Рассмотрим такой путь $i\pi j$ и дерево вывода $l(\pi)$ в $G_A$ высоты $h=p$. Так как грамматика в нормальной форме Хомского, у корня есть ровно 2 ребенка. Они являются корнями подеревьев, являющихся по определению деревьями вывода некоторых строк $l_{left}$ в $G_B$ и $l_{right}$ в $G_C$ соответственно. Так как конкатенация $l_{left}$ и $l_{right}$ это $l(\pi)$, $i\pi j$ можно разбить на $i\pi_{left} r$ и $r\pi_{right} j$ так, чтобы выполнялось $l(\pi_{left}) = l_{left}$ и $l(\pi_{right}) = l_{right}$.
Из индукционного предположения:
\begin{equation*}
a^{p-1}_{ir}(B) \le w(\pi_{left})
\end{equation*}
\begin{equation*}
a^{p-1}_{rj}(C) \le w(\pi_{right})
\end{equation*}
Из этого и \eqref{apply_times}:
\begin{equation*}
(a^{p-1}\times a^{p-1})_{ij}(A) \le a^{p-1}_{ir}(B) + a^{p-1}_{rj}(C) \le w(\pi_{left}) + w(\pi_{right}) = w(\pi)
\end{equation*}
Таким образом:
\begin{align*}
a^p_{i,j}(A) &\le a^{p-1}_{ij}(A) &\le w(\pi) & \text{для}~i\pi j~\text{подходящих}~(A, p-1)\\
a^p_{i,j}(A) &\le (a^{p-1}\times a^{p-1})_{ij}(A) &\le w(\pi) & \text{для}~i\pi j~\text{подходящих}~(A, p)~\text{, но не}~(A, p-1)
\end{align*}
Cледовательно:
\begin{equation*}
a^p_{i,j}(A) \le w(\pi)~\text{для}~i\pi j~\text{подходящих}~(A, p)
\end{equation*}
Лемма доказана.
\end{proof}
\begin{lemma}
\label{eq_some}
Пусть $D=(V,E)$ --- граф, $G=(N,\Sigma, P, S)$ --- контекстно-свободная грамматика в нормальной форме Хомского. Тогда, для любых $i$, $j$, $k$ и нетерминала $A\in N$
верно следующее: либо существует путь $i\pi j$ подходящий для пары $(A, k)$, такой что $a^k_{ij}(A) = w(\pi)$, либо не существует путей подходящих для пары $(A, k)$ и $a^k_{ij}(A) = \infty$.
\end{lemma}
\begin{proof}
По индукции.\\
\textbf{База:} по построению $a^1$ = $a$. Все деревья вывода высоты 1 соотвествуют каждое своему ребру.\\
\textbf{Переход:} Пусть p > 1. Предположим, что утверждение леммы выполняется для $k < p$. Рассмотрим $a^p_{i,j}(A)$. Из \eqref{apply_plus} следует, что выполняется как минимум одно из следующих выражений:
Рассмотрим случаи:\\
\begin{equation*}
a^p_{i,j}(A) = a^{p-1}_{i,j}(A) < \infty
\end{equation*}
По индукционнному предположению $a^{p-1}_{i,j}(A) < \infty$ тогда и только тогда, когда существует путь $i\pi j$ полходящий для пары $(A, p-1)$, он такжн будет подходящим для пары $(A, p)$.
\begin{equation*}
a^p_{i,j}(A) = (a^{p-1}\times a^{p-1})_{i,j}(A) < \infty
\end{equation*}
Из \eqref{apply_times} следует, что $(a^{p-1}\times a^{p-1})_{i,j}(A) < \infty$ тогда и только тогда, когда существуют такие $r$, $B$ и $C$, что $a^{p-1}_{ir}(B) < \infty$, $a^{p-1}_{rj}(C) < \infty$ и $A~\rightarrow~BC~\in~P$. Также, для некоторых таких $r$, $B$ и $C$ выполняется $a^{p}_{ij}(A) = a^{p-1}_{ir}(B) + a^{p-1}_{rj}(C)$. По индукционному предположению существуют пути $i\pi_1 r$ и $r\pi_2 j$ подходящие для $(B, p-1)$ и $(C, p-1)$ соответственно, а следовательно и $T_B$ --- дерево вывода $l(\pi_1)$ в $G_B$ и $T_C$ --- дерево вывода $l(\pi_2)$ в $G_C$ соответственно. Конкатенация $i\pi_1 r$ и $r\pi_2 j$ образует путь $i\pi j$, такой что $l(\pi)$ это конкатенция $l(\pi_1)$ и $l(\pi_2)$. При этом дерево, где в корне A, левое поддерево это $T_B$, а правое --- $T_C$, будет является деревом вывода $l(pi)$ в $G_A$б так как $A\rightarrow BC \in P$. Следовательно $i\pi j$ подходящий для пары $(A, k)$ и верно следующее:
\begin{align*}
a^{p}_{i,j}(A) &=\\
&= (a^{p-1}\times a^{p-1})_{i,j}(A)\\
&= a^{p-1}_{ir}(B) + a^{p-1}_{rj}(C)\\
&= w(\pi_1) + w(\pi_2)\\
&= w(\pi)
\end{align*}
В этом случае индукционный переход также выполняется.
\begin{equation*}
a^p_{i,j}(A) = a^{p-1}_{i,j}(A) = (a^{p-1}\times a^{p-1})_{i,j}(A) = \infty
\end{equation*}
По индукционному предположению не существует $i\pi j$ подходящего для $(A, p-1)$. Предположим, что существует путь $i\pi j$ подходящий для $(A, p)$ и неподходящий для $(A, p-1)$. Рассмотрим дерево вывода $l(\pi)$ в $G_A$ высоты $h=p$. Так как грамматика в нормальной форме Хомского, у корня есть ровно 2 ребенка. Они являются корнями подеревьев, являющихся по определению деревьями вывода некоторых строк $l_{left}$ в $G_B$ и $l_{right}$ в $G_C$ соответственно, высота каждого из этих деревьев строго меньше $p$, Так как конкатенация $l_{left}$ и $l_{right}$ это $l(\pi)$, $i\pi j$ можно разбить на $i\pi_{left} r$ и $r\pi_{right} j$ так, чтобы выполнялось $l(\pi_{left}) = l_{left}$ и $l(\pi_{right}) = l_{right}$. Таким образом, $i\pi_{left} r$ походящий для $(B, p-1)$, а $r\pi{_right} j$ подходящий для $(C, p-1)$. Следовательно, по индукционному предположению, $a^{p-1}_{ir}(B) < \infty$ и $a^{p-1}_{rj}(C) < \infty$. Так как $A\rightarrow BC \in P$, по определению $(\times)$, $a^p_{i,j}(A) \le a^{p-1}_{ir}(B) + a^{p-1}_{rj}(C) < \infty$. Это противоречит предположениюо условю $a^p_{i,j}(A) = \infty$, таким образом предположение о существовании пути $i\pi j$ подходящего для $(A, p)$ и неподходящего для $(A, p-1)$, неверно.
Таким образом утверждение леммы выполняетнся при p, если оно выполняется при k < p. Лемма доказана.
\end{proof}
\begin{theorem}
\label{th_correctness}
Пусть $D=(V,E)$ --- граф без циклов отрицательного веса, $G=(N,\Sigma, P, S)$ --- контекстно-свободная грамматика в нормальной форме Хомского. Тогда $a^{cf}_{ij}(A) = \infty$ если не существует пути $i\pi j$ такого, что существует дерево вывода строки $l(\pi)$ в $G_A$, и минимальной длине среди всех таких путей в противном случае.
\end{theorem}
\begin{proof}
Предположим что не существует пути $i\pi j$ такого, что существует дерево вывода строки $l(\pi)$ в $G_A$. Тогда по~\cref{eq_some} для любого p $a^p_{ij}(A) = \infty$, следовательно $a^{cf}_{ij}(A) = \infty$.
Предположим cуществует $i\pi j$ такой, что существует дерево вывода строки $l(\pi)$ в $G_A$. Так как в графе нет циклов отрицательного веса, найдется путь $i\pi_m j$ такой, что существует дерево вывода cтроки $l(\pi_m)$ в $G_A$ и при этом $w(\pi_m) \le w(\pi)$ для любого пути $i\pi j$ такого, что существует дерево вывода строки $l(\pi)$ в $G_A$. Пусть h --- высота некоторого дерева вывода строки $l(\pi_m)$ в $G_A$. По~\cref{le_any} $a^p_{ij}(A) \le w(\pi_m)$ для $p \ge h$, а по~\cref{eq_some} $a^p_{ij}(A) = w(\pi)$ для некоторого $i\pi j$ подходящего для $(A, p)$. По выбору $\pi_m$
$w(\pi_m) \le w(\pi)$. Следовательно $w(\pi_m) \le a^p_{ij}(A) \le w(\pi_m)$, а значит $a^p_{ij}(A) = w(\pi_m)$ для $p \ge h$, следовательно $a^{cf}_{ij}(A) = w(\pi_m)$. Теорема доказана.
\end{proof}
\begin{theorem}
\label{th_finiteness}
Пусть $D=(V,E)$ --- граф без циклов отрицательного веса, $G=(N,\Sigma, P, S)$ --- контекстно-свободная грамматика в нормальной форме Хомского. Тогда $a^{cf}_{ij}(A) = a^p_{ij}(A)$ начиная с некоторого p.
\end{theorem}
\begin{proof}
Для каждых $i$, $j$, $A$ построим множество путей $i\pi j$ таких что $w(\pi) = a^{cf}_{ij}(A)$ и существует дерево вывода $l(\pi)$ в $G_A$. Из каждого такого множества, кроме пустых выберем представителя и обозначим высоту некоторого соответствующего дерева вывода за $h^A_{ij} > 0$, а если множество пустое, то пусть $h^A_{ij} = 0$. Пусть $h_{max} = \max_{i, j, A}(h^A_{ij})$. Если $h_{max} = 0$, то в графе нет ни одного соответствующего пути и $a^1_{i,j}(A) = a^{cf}_{i,j}(A) = \infty$. Иначе, по~\cref{le_any}, $a^{h_{max}}_{ij}(A) \le a^{cf}_{ij}(A)$, а следовательно по определению $a^{cf}$ $a^{h_{max}}_{ij}(A) = a^{cf}_{ij}(A)$. Теорема доказана.
\end{proof}
\subsection{Оценка времени работы}
Оценка $O(|V|^5|N|^3)$. Умножение матриц в алгоритме выполняется за $O(|V|^3 * |N|^2)$. Оценка на количество итераций, $|V|^2|N|$, исходит из того что каждую итерацию в матрице будет фиксироваться одно значение. Рассуждения следует основывать на минимальных по высоте деревьях вывода кратчайших путей. !ДОПИСАТЬ ДОКАЗАТЕЛЬСТВО!
\section{Экспериментальное исследование}
!РЕАЛИЗОВАТЬ АЛГОРИТМ И ЗАТЕСТИТЬ, ОПИСАТЬ ЭТО!
%У заключения нет номера главы
\section*{Заключение}
В данной работе модифицирован алгоритм поиска пути с контекстно-свободными %ограничениями в помеченном графе\cite{DBLP:journals/corr/AzimovG17} для поиска %кратчайшего пути. Для достижения данной цели были решены следующие задачи:
\begin{itemize}
\item алгоритм модифицирован с помощью $(min, +)$-произведения;
\begin{itemize}
\item доказана корректность;
\item дана оценка времени работы: $O(|V|^5|N|^3)$;
\end{itemize}
\item проведено экспериментальное исследование модифицированного алгоритма;
\end{itemize}
\setmonofont[Mapping=tex-text]{CMU Typewriter Text}
\bibliographystyle{ugost2008ls}
\bibliography{diploma.bib}
\end{document}