10
правок
Изменения
Нет описания правки
По условию проблемы <tex>BH_{1N}\,\!</tex>, у нас есть недетерминированная машина Тьюринга <tex>m\,\!</tex>, причём можно считать, что её лента односторонняя и что машина не пишет на ленту пробелы, входное слово <tex>x\,\!</tex> и время <tex>t\,\!</tex>, заданное в унарной системе счисления. Нам же надо построить такую булеву формулу <tex>\phi\,\!</tex>, что она выполнима тогда, и только тогда, когда <tex>m\,\!</tex>, получив на вход <tex>x\,\!</tex>, делает не более <tex>t\,\!</tex> шагов и допускает это слово.
В любой момент времени мгновенное описание (МО) <tex>m\,\!</tex> есть строка <tex>z\#_qyb</tex>, где <tex>b\,\!</tex> — строка, состоящая из такого количества пробелов, чтобы длина всего МО была <tex>t + 1.\,\!</tex> Соответственно, начальное МО задаётся так : <tex>\#_sx_sxb\,\!</tex>(<tex>b\,\!</tex> может быть пустой). Если же <tex>|x| > t\,\!</tex>, то будем считать, что на ленту записаны лишь первые <tex>t\,\!</tex> символов, ведь <tex>m\,\!</tex> не может обработать большее количество символов за <tex>t\,\!</tex> шагов.
Также нам удобно считать, что все вычисления проходят ровно за <tex>t + 1\,\!</tex> шагов, даже если мы попали в допускающее состояние раньше. То есть, мы разрешим переход <tex>q \vdash q</tex>, если в МО <tex>q\,\!</tex> есть допускающее состояние, так что, чтобы проверить, допустила ли машина слово, надо лишь проверить наличие допускающего состояния в МО <tex>q_t\,\!</tex>.
