Я также искал формального профессора и не смог его найти. Не уверен, что ниже приведен формальный проф, но это может дать вам некоторое представление.
Лемма: Для каждого линейного контекста свободных языков L существует n> 0, так что для каждого w в L с | w |> n мы можем написать w как uvxyz такой, что | vy |> 0, | uvyz |<= n и uv ^ ixy ^ iz для каждого i> = 0 в L.
«Доказательство»: представьте дерево разбора для некоторой длинной строки w в L с начальным символом S. Также давайте предположим, чтодерево не содержит бесполезных узлов.Если w достаточно длинный, будет хотя бы один нетерминал, повторяющийся более одного раза.Давайте назовем первый повторяющийся нетерминал, идущий вниз по дереву X, его первое вхождение (сверху) как X [1] и его второе вхождение как X [2]. Пусть x будет строкой в w, сгенерированной X [2],vxy - строка, сгенерированная X [1], и uvxyz - полная строка w, сгенерированная S. Поскольку при переходе от X [1] к X [2] генерируется v, y, теоретически мы можем сгенерировать новое дерево, в котором мы повторяем это перемещение несколько раз.перед переходом от X [1] вниз. Это доказывает, что uv ^ ixy ^ iz для каждого i> = 0 находится в L. Поскольку наше дерево не содержит бесполезных узлов, перемещение из X [1] в X [2] должно генерировать некоторые терминалыи это доказывает, что | vy |> 0.L является линейным, что означает, что на каждом уровне дерева у нас есть один нетерминальный символ.Каждый узел в дереве покрывает некоторую подстроку в w, длина которой ограничена линейной функцией высоты узла.Переход от S к X [2] охватывает uv и yz от w, и количество пройденных уровней дерева ограничено (2 * количество нетерминальных символов + 1).Поскольку количество пройденных уровней ограничено, а дерево линейно, оно также ограничивает выход движения от S к X [2], что означает, | uvyz |<= n для некоторого n> = 0.
Примечание: имейте в виду, что мы строим X [1], X [2] сверху вниз, в отличие от того, как мы доказываем «регулярную» лемму прокачки для контекстабесплатная грамматика в целом.В «правильной» лемме о накачке есть ограничение на высоту X [1] и, следовательно, ограничение на | vxy |. В нашем случае нет ограничения на высоту X [1], и оно может быть таким же высоким, кактребуется длина w. Однако существует ограничение на число уровней дерева от S до X [2]. Это мало что значит, если грамматика не является линейной, так как вывод идет от S к X [2]все еще ограничен только максимумом S (который не ограничен). Но в линейном случае этот выход ограничен и поэтому | uvyz | <= n </p>