editor
177
правок
Изменения
м
→Теорема Сэвича
Рассмотрим вспомогательную функцию <tex>Reach(I, J, k)</tex>, вычисляющую возможность перехода из конфигурации <tex>I</tex> в конфигурацию <tex>J</tex> за не более, чем <tex>2^k</tex> переходов:
'''Reach''' (I, J, k):
'''if''' (k = 0)
'''return''' (I <tex>\vdash</tex> J) or (I = J); // запись (I <tex>\vdash</tex> J) означает возможность перехода МТ из конфигурации I в конфигурацию J за один шаг
'''else'''
'''for''' (Y) // перебор промежуточных конфигураций
'''if''' Reach(I, Y, k-1) and Reach(Y, J, k-1)
'''return''' true; '''return''' false;
Эта функция имеет глубину рекурсии <tex>O(k)</tex>, на каждом уровне рекурсии использует <tex>O(f(n))</tex> памяти для хранения текущих конфигураций.
Рассмотрим функцию, которая по заданному слову <tex>x</tex> проверяет его принадлежность к языку <tex>L</tex>:
'''Check''' (x, L):
'''for''' (T) // перебор конфигураций, которые содержат допускающие состояния
'''if''' Reach(S, T, <tex>\log \left(2^{df(n)}\right)</tex>)
'''return''' true; '''return''' false;
Если слово принадлежит языку, то оно будет допущено, так как будут рассмотрены все возможные пути допуска. Это обеспечивается указанной нам глубиной рекурсии для функции <tex>Reach</tex>. И если слово не допускается за <tex>2^{df(n)}</tex> шагов (количество всех возможных конфигураций), то оно уже гарантированно не может быть допущено.
