Существует ли расширение регулярных выражений, которое фиксирует языки без контекста?

Во многих работах с использованием контекстно-свободных грамматик (CFG) примеры таких грамматик, представленные там, часто допускают простую характеристику языка, который они генерируют. Например:

$S \to a a S b$
$S \to$

генерирует $\{ a^{2i} b^i | i \geq 0\}$ ,

$S \to a S b$
$S \to a a S b$
$S \to$

генерирует $\{ a^i b^j \mid i \geq j \geq 0 \}$ и

$S \to a S a$
$S \to b S b$
$S \to$

генерирует $\{ w w^R \mid w \in (a|b)^* \}$ или эквивалентно $\{ ((a|b)^*)_1 ((a|b)^*)_2 \mid p_1 = p_2^R \}$ (где $p_1$ обозначает к той части , захваченной $(...)_1$ ).

Приведенные выше примеры могут быть сгенерированы путем добавления индексов ( $a^i$ ), простых ограничений на эти индексы ( $i > j$ ) и сопоставления с образцом для регулярных выражений. Это заставляет меня задуматься о том, могут ли все контекстно-свободные языки генерироваться каким-либо расширением регулярных выражений.

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

Да, есть. Определите выражение без контекста как термин, сгенерированный следующей грамматикой:

$$\begin{array}{lcll} g & ::= & \epsilon & \mbox{Empty string}\\ & | & c & \mbox{Character $c$ in alphabet $\Sigma$} \\ & | & g \cdot g & \mbox{Concatenation} \\ & | & \bot & \mbox{Failing pattern} \\ & | & g \vee g & \mbox{Disjunction}\\ & | & \mu \alpha.\; g & \mbox{Recursive grammar expression} \\ & | & \alpha & \mbox{Variable expression} \end{array}$$

Это все конструкторы для регулярных языков, за исключением звезды Клини, которая заменяется общим оператором с фиксированной точкой $\mu \alpha.\;g$$g\ast \triangleq \mu \alpha.\;\epsilon \vee g\cdot\alpha$

Интерпретация выражения без контекста требует учета интерпретации свободных переменных. Поэтому определите окружение которое будет отображаться из переменных в языки (то есть подмножества ), и пусть будет функцией, которая ведет себя как на всех входах, кроме и который возвращает язык для .$\rho$$\Sigma^*$$[\rho|\alpha:L]$$\rho$$\alpha$$L$$\alpha$

Теперь определим интерпретацию выражения без контекста следующим образом:

$$\newcommand{\interp}[2]{[\![{#1}]\!]\;{#2}} \newcommand{\setof}[1]{\left\{#1\right\}} \newcommand{\comprehend}[2]{\setof{{#1}\;\mid|\;{#2}}} \begin{array}{lcl} \interp{\epsilon}{\rho} & = & \setof{\epsilon} \\ \interp{c}{\rho} & = & \setof{c} \\ \interp{g_1\cdot g_2}{\rho} & = & \comprehend{w_1 \cdot w_2}{w_1 \in \interp{g_1}{\rho} \land w_2 \in \interp{g_2}{\rho}} \\ \interp{\bot}{\rho} & = & \emptyset \\ \interp{g_1 \vee g_2}{\rho} & = & \interp{g_1}{\rho} \cup \interp{g_2}{\rho} \\ \interp{\alpha}{\rho} & = & \rho(\alpha) \\ \interp{\mu \alpha.\; g}{\rho} & = & \bigcup_{n \in \mathbb{N}} L_n \\ \mbox{where} & & \\ L_0 & = & \emptyset \\ L_{n+1} & = & L_n \cup \interp{g}{[\rho|\alpha:L_n]} \end{array}$$

Используя теорему Кнастера-Тарского, легко увидеть, что интерпретация является наименее фиксированной из выражения.$\mu \alpha.g$

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

РЕДАКТИРОВАТЬ: Нет, я не знаю стандартную ссылку для этого: я разработал его для своих собственных интересов. Тем не менее, это достаточно очевидная конструкция, которая, я уверен, была изобретена ранее. Некоторые случайные поиски в Google показывают Joost Winter, недавнюю статью Marcello Bonsangue и Jan Rutten Context-Free Languages, Coalgebraically , где они дают вариант этого определения (требующий защиты всех фиксированных точек), который они также называют выражениями без контекста.

На MathOverflow был тесно связанный вопрос (и несколько ответов) о языках, производящие функции которых голономны .

Интересно, что определение Нилом семантики выше точно соответствует (конструктивному) доказательству существования видовых решений рекурсивных уравнений вида через неявную теорему о видах. К сожалению, его схема доказательства также должна содержать тонкую ошибку, так как есть случаи, когда дела идут «бесконечно». Другими словами, на якобиане существует условие преобразования, определяемого грамматикой, чтобы оно было неособым, что необходимо. Вероятно, именно поэтому Бонсанге-Руттен требует, чтобы фиксированные точки были защищены, как один из способов обеспечить это условие на якобиане.$\mu$

Недавно мы опубликовали наброски структуры, которая будет делать именно это. Посмотрите в comp.compilers , куда я отправил уведомление вместе с некоторыми ссылками.

Новые разработки основаны на теореме Хомского-Шютценбергера и могут рассматриваться как завершение этого результата. Сам Хомский был проинформирован о событиях и указывает на желание «наверстать упущенное».

Наряду с этим развитием мы также устанавливаем эквивалентность двух отдельных формулировок для выражений без контекста - одна, которая является расширением / дополнением формы мю-исчисления с «наименьшей фиксированной точкой» (первоначально Gruska, Yntema и McWhirter) - который получил окончательный вид сортов в 2014 году, а другой опубликован в 2008 году.