13.5: Представлення машин Тьюринга

Template:MathJaxZach

Для того, щоб представити машини Тьюринга та їх поведінку реченням логіки першого порядку, ми повинні визначити відповідну мову. Мова складається з двох частин: присудкових символів для опису конфігурацій машини, і виразів для нумерації кроків виконання («моментів») і позицій на стрічці.

Ми вводимо два види символів предикатів, обидва вони 2-місні: Для кожного стану\(q\) символ присудка\(\Obj Q_q\), а для кожного символу стрічки - символ\(\sigma\) предиката\(\Obj S_\sigma\). Перші дозволяють описати стан\(M\) і положення його стрічкової головки, другі дозволяють описати вміст стрічки.

Для того щоб висловити положення головки стрічки і кількість виконаних кроків, нам потрібен спосіб вираження чисел. Це робиться за допомогою постійного символу\(\Obj 0\) та функції\(1\) -place\(\prime\), функції-наступника. За умовністю вона пишеться після його аргументу (і ми залишаємо поза дужками). Так\(\Obj 0\) називає крайню ліву позицію на стрічці, а також час до першого кроку виконання (початкова конфігурація),\(\Obj 0'\) називає квадрат праворуч від крайнього лівого квадрата та час після першого кроку виконання тощо. Ми також вводимо символ присудка\(<\) для вираження як впорядкування позицій стрічки (коли воно означає «зліва від»), так і кроків виконання (тоді це означає «перед»).

Після того, як ми маємо мову на місці, ми перераховуємо «аксіоми»\(T(M, w)\), тобто речення, які разом описують поведінку\(M\) при запуску на вході\(w\). Будуть речення, які викладають умови на\(\Obj 0\), і\(\prime\), речення\(<\), які описують вхідну конфігурацію, і речення, які описують, що конфігурація\(M\) є після того, як вона виконує певну інструкцію.

Визначення\(\PageIndex{1}\)

З огляду на машину Тьюринга\(M = \tuple{Q, \Sigma, q_0, \delta}\), мова\(\Lang L_M\) складається з:

1. Двомісне предикат символ\(\Obj Q_q(x, y)\) для кожного стану\(q \in Q\). Інтуїтивно\(\Obj Q_q(\num{m}, \num{n})\) висловлює «після\(n\) кроків,\(M\) знаходиться в стані\(q\) сканування\(m\) го квадрата».

2. Двомісне предикат символ\(\Obj S_\sigma(x, y)\) для кожного символу\(\sigma\in \Sigma\). Інтуїтивно\(\Obj S_\sigma(\num{m}, \num{n})\) висловлює «після\(n\) кроків, той\(m\) квадрат містить символ»\(\sigma\).

3. Постійний символ\(\Obj 0\)

4. Символ функції в одному місці\(\prime\)

5. Символ присудка з двох місць\(<\)

Для кожного числа\(n\) існує канонічний термін\(\num{n}\), числівник для\(n\), який представляє його в\(\Lang L_M\). \(\num{0}\)є\(\Obj 0\),\(\num{1}\) є\(\Obj 0'\)\(\Obj 0''\),\(\num{2}\) є і так далі. Більш формально:\[\begin{aligned} \num{0} & = \Obj 0 \\ \num{n+1} &= \num{n}'\end{aligned}\]

Речення, що описують роботу машини Тьюринга\(M\) на вході,\(w = \sigma_{i_1}\dots\sigma_{i_k}\) такі:

1. Аксіоми, що описують числа:

   1. Речення, яке говорить про те, що функція наступника є ін'єкційною:\[\lforall{x}{\lforall{y}{ (\eq[x'][y'] \lif \eq[x][y])}}\nonumber\]

   2. Речення, яке говорить про те, що кожне число менше, ніж його наступник:\[\lforall{x}{x < x'}\nonumber\]

   3. Речення, яке гарантує, що\(<\) це є перехідним:\[\lforall{x}{\lforall{y}{\lforall{z}{ ((x < y \land y < z) \lif x < z)}}}\nonumber\]

   4. Речення, яке з'єднує\(<\) і\(=\):\[\lforall{x}{\lforall{y}{(x < y \lif \eqN[x][y])}}\nonumber\]

2. Аксіоми, що описують вхідну конфігурацію:

   1. Після\(0\) кроків - перед запуском машини -\(M\) знаходиться в початковому стані\(q_0\), сканування квадрат\(1\):\[\Obj Q_{q_0}(\num{1}, \num{0})\nonumber\]

   2. Перші\(k+1\) квадрати містять символи\(\TMendtape\),\(\sigma_{i_1}\),...,\(\sigma_{i_k}\):\[\Obj S_\TMendtape(\num{0}, \num{0}) \land \Obj S_{\sigma_{i_1}}(\num{1}, \num{0}) \land \dots \land \Obj S_{\sigma_{i_k}}(\num{k}, \num{0})\nonumber\]

   3. В іншому випадку стрічка порожня:\[\lforall{x}{(\num{k} < x \lif \Obj S_\TMblank(x, \num{0}))}\nonumber\]

3. Аксіоми, що описують перехід від однієї конфігурації до наступної:

   Для наступного, нехай\(A(x, y)\) буде сполучність всіх пропозицій виду\[\lforall{z}{ (((z < x \lor x < z) \land \Obj S_\sigma(z, y)) \lif \Obj S_\sigma(z, y'))}\nonumber\] де\(\sigma \in \Sigma\). Ми використовуємо\(A(\num{m},\num{n})\) для вираження «крім квадрата\(m\), стрічка після\(n+1\) кроків така ж, як і після\(n\) кроків».

   1. Для кожної інструкції\(\delta(q_i, \sigma) = \tuple{q_j, \sigma', \TMright}\) речення:\[\begin{aligned} & \lforall{x}{\lforall{y}{( (\Obj Q_{q_i}(x, y) \land \Obj S_{\sigma}(x, y)) \lif {}}} \\ &\qquad (\Obj Q_{q_j}(x', y') \land \Obj S_{\sigma'}(x, y') \land A(x, y)))\end{aligned}\] Це говорить, що якщо після\(y\) кроків машина знаходиться в стані\(q_i\) сканування квадрат,\(x\) який містить символ\(\sigma\), то після \(y+1\)кроки сканування квадрат\(x+1\), знаходиться в стані\(q_j\), квадрат\(x\) тепер містить\(\sigma'\), і кожен квадрат, крім\(x\) містить той же символ, що і після\(y\) сходинки.

   2. Для кожної інструкції речення:\[\begin{aligned} & \lforall{x}{\lforall{y}{ ((\Obj Q_{q_i}(x', y) \land \Obj S_{\sigma}(x', y)) \lif {}}}\\ & \qquad (\Obj Q_{q_j}(x, y') \land \Obj S_{\sigma'}(x', y') \land A(x, y))) \land {}\\ & \lforall{y}{((\Obj Q_{q_i}(\Obj 0, y) \land \Obj S_{\sigma}(\Obj 0, y)) \lif {}}\\ & \qquad (\Obj Q_{q_j}(\Obj 0, y') \land \Obj S_{\sigma'}(\Obj 0, y') \land A(\Obj 0, y)))\end{aligned}\] Знайдіть хвилинку\(\delta(q_i, \sigma) = \tuple{q_j, \sigma', \TMleft}\), щоб подумати про те, як це працює: тепер ми починаємо не з «якщо сканувати квадрат\(x\)...», а: «якщо сканувати квадрат\(x+1\)...» Рух вліво означає, що на наступному кроці машина сканує квадрат\(x\). Але квадрат, на якому написано, є\(x+1\). Ми робимо це таким чином, оскільки у нас немає віднімання або функції попередника.

      Зверніть увагу, що номери форми\(x+1\) є\(1\),\(2\),..., тобто це не охоплює випадок, коли машина сканує квадрат\(0\) і повинен рухатися вліво (що, звичайно, не може - він просто залишається поставленим). Цей особливий випадок охоплюється другим сполучником: він говорить, що якщо після\(y\) кроків машина сканує квадрат\(0\) у стані,\(q_i\) а квадрат\(0\) містить символ\(\sigma\), то після \(y+1\)кроки він все ще сканує квадрат\(0\), тепер у стані\(q_j\), символ на квадраті\(0\) є\(\sigma'\), а квадрати, крім квадратів,\(0\) містять ті самі символи, які вони містили ofter \(y\)сходинки.

   3. Для кожної інструкції\(\delta(q_i, \sigma) = \tuple{q_j, \sigma', \TMstay}\) речення:\[\begin{aligned} & \lforall{x}{\lforall{y}{( (\Obj Q_{q_i}(x, y) \land \Obj S_{\sigma}(x, y)) \lif {}}} \\ &\qquad (\Obj Q_{q_j}(x, y') \land \Obj S_{\sigma'}(x, y') \land A(x, y)))\end{aligned}\]

\(T(M, w)\)Дозволяти бути сполучником всіх перерахованих вище речень для машини Тьюринга\(M\) і введення\(w\).

Для того, щоб висловити, що\(M\) врешті-решт зупиняється, ми повинні знайти речення, яке говорить «після деякої кількості кроків функція переходу буде невизначена». \(X\)Дозволяти бути набір всіх пар\(\tuple{q, \sigma}\) таких,\(\delta(q, \sigma)\) що не визначено. Нехай\(E(M, w)\) тоді буде речення\[\lexists{x}{\lexists{y}{(\bigvee_{\tuple{q, \sigma} \in X}(\Obj Q_q(x, y) \land \Obj S_\sigma(x, y)))}}\nonumber\]

Якщо ми використовуємо машину Тьюринга з позначеним станом зупинки\(h\), то це ще простіше: тоді речення\(E(M, w)\)\[\lexists{x}{\lexists{y}{\Obj Q_h(x, y)}}\nonumber\] висловлює, що машина з часом зупиняється.

Пропозиція\(\PageIndex{1}\)

Якщо\(m < k\), то\(T(M, w) \Entails \num{m} < \num{k}\)

Доказ. Вправа. ◻

Проблема\(\PageIndex{1}\)

Доведіть пропозицію\(\PageIndex{1}\). (Підказка: використовуйте індукцію\(k-m\) ввімкнено).