Skip to content

Commit 8c477f1

Browse files
gsvgitgsvgit
committed
Review of MCFG section.
1 parent abb1d8b commit 8c477f1

2 files changed

Lines changed: 57 additions & 20 deletions

File tree

‎tex/FormalLanguageConstrainedReachabilityLectureNotes.bib‎

Lines changed: 20 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1622,7 +1622,7 @@ @inproceedings{10.1145/3315454.3329962
16221622
}
16231623

16241624
@article{GEBHARDT202241,
1625-
title = {On is an n-MCFL},
1625+
title = {$O_n$ is an $n$-MCFL},
16261626
journal = {Journal of Computer and System Sciences},
16271627
volume = {127},
16281628
pages = {41-52},
@@ -2185,3 +2185,22 @@ @article{kanazawa2014failure
21852185
year = {2014},
21862186
doi = {10.1007/s00224-014-9534-z}
21872187
}
2188+
2189+
@article{10.1145/3704854,
2190+
author = {Conrado, Giovanna Kobus and Kjelstr\o{}m, Adam Husted and van de Pol, Jaco and Pavlogiannis, Andreas},
2191+
title = {Program Analysis via Multiple Context Free Language Reachability},
2192+
year = {2025},
2193+
issue_date = {January 2025},
2194+
publisher = {Association for Computing Machinery},
2195+
address = {New York, NY, USA},
2196+
volume = {9},
2197+
number = {POPL},
2198+
url = {https://doi.org/10.1145/3704854},
2199+
doi = {10.1145/3704854},
2200+
abstract = {Context-free language (CFL) reachability is a standard approach in static analyses, where the analysis question (e.g., is there a dataflow from x to y ?) is phrased as a language reachability problem on a graph G wrt a CFL L. However, CFLs lack the expressiveness needed for high analysis precision. On the other hand, common formalisms for context-sensitive languages are too expressive, in the sense that the corresponding reachability problem becomes undecidable. Are there useful context-sensitive language-reachability models for static analysis?In this paper, we introduce Multiple Context-Free Language (MCFL) reachability as an expressive yet tractable model for static program analysis. MCFLs form an infinite hierarchy of mildly context sensitive languages parameterized by a dimension d and a rank r. Larger d and r yield progressively more expressive MCFLs, offering tunable analysis precision. We showcase the utility of MCFL reachability by developing a family of MCFLs that approximate interleaved Dyck reachability, a common but undecidable static analysis problem.Given the increased expressiveness of MCFLs, one natural question pertains to their algorithmic complexity, i.e., how fast can MCFL reachability be computed? We show that the problem takes On2d+1 time on a graph of n nodes when r=1, and Ondr+1 time when r>1. Moreover, we show that when r=1, even the simpler membership problem has a lower bound of n2d based on the Strong Exponential Time Hypothesis, while reachability for d=1 has a lower bound of n3 based on the combinatorial Boolean Matrix Multiplication Hypothesis. Thus, for r=1, our algorithm is optimal within a factor n for all levels of the hierarchy based on the dimension d (and fully optimal for d=1).We implement our MCFL reachability algorithm and evaluate it by underapproximating interleaved Dyck reachability for a standard taint analysis for Android. When combined with existing overapproximate methods, MCFL reachability discovers all tainted information on 8 out of 11 benchmarks, while it has remarkable coverage (confirming 94.3\% of the reachable pairs reported by the overapproximation) on the remaining 3. To our knowledge, this is the first report of high and provable coverage for this challenging benchmark set.},
2201+
journal = {Proc. ACM Program. Lang.},
2202+
month = jan,
2203+
articleno = {18},
2204+
numpages = {30},
2205+
keywords = {static analysis, CFL reachability, Dyck reachability, context-sensitive languages}
2206+
}

‎tex/Multiple_Context-Free_Languages.tex‎

Lines changed: 37 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,25 @@ \chapter{Многокомпонентные контекстно-свободн
33
\label{MCFG}
44
\tikzsetfigurename{MCFG_}
55

6-
%!!!TODO!!!! Перепроверить все ссылки. Вообще весь раздел. Ну и дописать.
6+
%!!!TODO!!!!
7+
% Перепроверить все ссылки. Вообще весь раздел. Ну и дописать.
8+
%
9+
% Конкретные пункты для проверки:
10+
% 1. Нормальная форма (строки 124--147): соответствует ли определение из nakanishi1997efficient
11+
% описанной в тексте нормальной форме (условие чередования, отсутствие терминалов)?
12+
% 2. Лемма о накачке (строки 188--198): сверить точную формулировку разбиения
13+
% (u_1 v_1 w_1 s_1 ... u_m v_m w_m s_m u_{m+1}) с Seki1991.
14+
% 3. Свойство поглощения ранга (строки 261--262): проверить формулу
15+
% (m*(k-1))-MCFL(r-k) subset m-MCFL(r) по Seki1991 -- при k=1 даёт 0-MCFL(r-1), что не определено.
16+
% 4. Замкнутость относительно гомоморфизмов (строка 299--300): сверить по Rambow1999,
17+
% доказывается ли там замкнутость относительно всех трёх операций (гомоморфизм,
18+
% обратный гомоморфизм, подстановка) или только части.
19+
% 5. Определение well-nested (строки 90--93): соответствует ли формальное условие
20+
% (с регулярным выражением) стандартному определению из Seki1991 / Kanazawa2009.
21+
% 6. Доказательство незамкнутости (строки 312--324): конструкция языков L_1, L_2
22+
% нуждается в верификации по Seki1991; текущее определение может давать пустое пересечение.
23+
% 7. Ссылка nakanishi1997efficient: проверить, действительно ли в этой работе
24+
% (MOL5, proceedings) содержится доказательство теоремы о нормальной форме.
725

826
\textit{Многокомпонентные контекстно-свободные грамматики} (Multiple Context-Free Grammars, MCFG)~--- это расширение контекстно-свободных грамматик, в котором нетерминальные символы могут порождать кортежи строк, а не отдельные строки.
927
Данный класс грамматик был впервые предложен Поллардом~\sidecite{pollard1984generalized} для описания синтаксиса естественных языков, а затем систематически изучен Секи с соавторами~\sidecite{seki1991multiple}.
@@ -94,11 +112,11 @@ \section{Разновидности MCFG}
94112
\end{itemize}
95113

96114
\begin{example}
97-
Следующее правило является well-nested (переменные каждого нетерминала образуют непрерывные интервалы):
115+
Следующее правило является well-nested (несмотря на то, что переменные $B$ не идут подряд, никакие два различных нетерминала не содержат запрещённого паттерна чередования вида $B_j \ldots C_{j'} \ldots B_{j+1} \ldots C_{j'+1}$):
98116
\[
99117
A(x_1, z_1 z_2, x_2, y_1 y_2 y_3, x_3) \leftarrow B(x_1,x_2,x_3), C(y_1,y_2,y_3), D(z_1,z_2).
100118
\]
101-
Следующее правило \emph{не} является well-nested (переменные $B$ и $C$ перекрещиваются):
119+
Следующее правило \emph{не} является well-nested (переменные $B$ и $C$ перекрещиваются: чередование $B_1$ ($x_1$) \ldots $C_1$ ($y_1$) \ldots $B_2$ ($x_2$) \ldots $C_2$ ($y_2$) образует запрещённый паттерн):
102120
\[
103121
A(z_1, x_1, y_1, x_2, z_2, y_2, x_3, y_3) \leftarrow B(x_1,x_2,x_3), C(y_1,y_2,y_3), D(z_1,z_2).
104122
\]
@@ -151,15 +169,15 @@ \section{Разновидности MCFG}
151169

152170
\begin{example}
153171
Приведём к нормальной форме грамматику для языка
154-
$\{a^n b^m c^n d^m \mid n,m \in \mathbb{N}\}$.
172+
$\{a^n b^m c^n d^m \mid n,m \in \mathbb{N}^+\}$.
155173
Исходная грамматика $G_1$:\begin{align*}
156174
A(a, c) &\leftarrow \\
157175
A(a x_1, c x_2) &\leftarrow A(x_1, x_2) \\
158176
B(b, d) &\leftarrow \\
159177
B(b x_1, d x_2) &\leftarrow B(x_1, x_2) \\
160178
S(x_1 x_2 x_3 x_4) &\leftarrow A(x_1, x_3), B(x_2, x_4)
161179
\end{align*}
162-
180+
163181
Эквивалентная грамматика $G'_1$ в нормальной форме использует
164182
вспомогательные нетерминалы $A_1,B_1,C_1,D_1$ ранга~1 и
165183
$S_1,S_2,S_3,S_4$ ранга~2:\begin{align*}
@@ -247,7 +265,7 @@ \section{Иерархия}
247265

248266
\begin{theorem}[Общий случай~\sidecite{seki1991multiple,rambow1999independent}]
249267
\label{thm:hierarchy_r_general}
250-
Если $m > 2$ или $r > 2$, то $m$-MCFL($r$) $\subsetneq$ $m$-MCFL($r+1$).
268+
Если $m > 2$ и $r > 2$, то $m$-MCFL($r$) $\subsetneq$ $m$-MCFL($r+1$).
251269
\end{theorem}
252270

253271
\begin{marginfigure}
@@ -312,10 +330,11 @@ \section{Свойства замкнутости}
312330
\begin{proof}
313331
Для доказательства незамкнутости относительно пересечения рассмотрим языки Секи с соавторами~\sidecite{seki1991multiple}:
314332
\[
315-
L_1 = \{a_1^n b_1^n \cdots a_{m+1}^n b_{m+1}^n\}, \qquad
316-
L_2 = \{a_1^n b_1^n c_2^n \cdots\}.
333+
L_1 = \{\,a_1^n b_1^n a_2^n b_2^n \cdots a_{m+1}^n b_{m+1}^n \mid n \ge 0\,\}, \qquad
334+
L_2 = \{\,a_1^n a_2^n \cdots a_{m+1}^n b_1^n b_2^n \cdots b_{m+1}^n \mid n \ge 0\,\}.
317335
\]
318-
Оба языка являются MCFL, но их пересечение не является MCFL в силу иерархической теоремы~\ref{thm:hierarchy_m}.
336+
Язык $L_1$ является $(m+1)$-MCFL($1$) (теорема~\ref{thm:hierarchy_m}), язык $L_2$ является $2$-MCFL (строится парой $(a_1^n\cdots a_{m+1}^n,\; b_1^n\cdots b_{m+1}^n)$, каждый компонент которой является КС-языком).
337+
В~\cite{seki1991multiple} показано, что $L_1 \cap L_2$ не является MCFL: при надлежащем выборе $m$ ранг, требуемый для порождения пересечения, превосходит $m$, а конструкция допускает масштабирование на произвольно большие значения~--- таким образом, пересечение не принадлежит ни одному из классов $m$-MCFL.
319338

320339
Незамкнутость относительно дополнения следует из незамкнутости относительно пересечения по законам де Моргана:
321340
если бы MCFL были замкнуты относительно дополнения, то $L_1 \cap L_2 = \overline{\overline{L_1} \cup \overline{L_2}}$ также был бы MCFL, что неверно.
@@ -344,16 +363,15 @@ \section{Языки MIX и $O_n$}
344363
Другие важные представители MCFL:
345364

346365
\begin{itemize}
347-
\item \textbf{Многомерный язык Дика}: существует $2$-MCFG для трёхмерного языка Дика~\sidecite{10.1007/978-3-662-59620-3_5}\footnote{\url{https://link.springer.com/chapter/10.1007/978-3-662-59620-3_5}}.
348-
\item \textbf{Шафл языков Дика}: задача контекстно-зависимого анализа графа зависимостей может быть сведена к MCFL-достижимости с использованием шафла языков Дика~\sidecite{10.1145/3009837.3009848}\footnote{\url{https://dl.acm.org/doi/10.1145/3093333.3009848}}.
366+
\item \textbf{Многомерный язык Дика}: вопрос о существовании $2$-MCFG для трёхмерного языка Дика $D^3$ остаётся открытым, хотя и предпринимались попытки построения, использующие технику метаграмматик~\sidecite{10.1007/978-3-662-59620-3_5}.
367+
\item \textbf{Шафл языков Дика}: в качестве приближения задачи контекстно-зависимого межпроцедурного анализа кода может быть использована к MCFL-достижимости с использованием шафла языков Дика~\sidecite{10.1145/3704854}\footnote{\url{https://dl.acm.org/doi/10.1145/3704854}}.
349368
\end{itemize}
350369

351-
\section{Вопросы и задачи}
370+
%\section{Вопросы и задачи}
352371

353-
\begin{enumerate}
354-
\item Покажите, что язык $\{a^n b^n c^n \mid n \ge 0\}$ не является MCFL.
355-
\item Постройте MCFG для языка $\{a^n b^m c^n d^m \mid n,m \ge 0\}$.
356-
\item Является ли язык $\{a^n b^{n^2} \mid n \ge 0\}$ MCFL? Ответ обоснуйте.
357-
\item Покажите, что $2$-MCFG могут порождать язык копий $\{ww \mid w \in \{a,b\}^*\}$.
358-
\item Докажите, что $1$-MCFL($2$) строго шире $1$-MCFL($1$).
359-
\end{enumerate}
372+
%\begin{enumerate}
373+
% \item Покажите, что язык $\{a^n b^n c^n \mid n \ge 0\}$ не является MCFL.
374+
% \item Постройте MCFG для языка $\{a^n b^m c^n d^m \mid n,m \ge 0\}$.
375+
% \item Является ли язык $\{a^n b^{n^2} \mid n \ge 0\}$ MCFL? Ответ обоснуйте.
376+
% \item Покажите, что $2$-MCFG могут порождать язык копий $\{ww \mid w \in \{a,b\}^*\}$.
377+
%\end{enumerate}

0 commit comments

Comments
 (0)