13.6: Перевірка представництва

Last updated
Save as PDF

Page ID: 52963

$ \newcommand{\vecs}[1]{\overset { \scriptstyle \rightharpoonup} {\mathbf{#1}} } $ $ \newcommand{\vecd}[1]{\overset{-\!-\!\rightharpoonup}{\vphantom{a}\smash {#1}}} $$\newcommand{\id}{\mathrm{id}}$ $ \newcommand{\Span}{\mathrm{span}}$ $ \newcommand{\kernel}{\mathrm{null}\,}$ $ \newcommand{\range}{\mathrm{range}\,}$ $ \newcommand{\RealPart}{\mathrm{Re}}$ $ \newcommand{\ImaginaryPart}{\mathrm{Im}}$ $ \newcommand{\Argument}{\mathrm{Arg}}$ $ \newcommand{\norm}[1]{\| #1 \|}$ $ \newcommand{\inner}[2]{\langle #1, #2 \rangle}$ $ \newcommand{\Span}{\mathrm{span}}$ $\newcommand{\id}{\mathrm{id}}$ $ \newcommand{\Span}{\mathrm{span}}$ $ \newcommand{\kernel}{\mathrm{null}\,}$ $ \newcommand{\range}{\mathrm{range}\,}$ $ \newcommand{\RealPart}{\mathrm{Re}}$ $ \newcommand{\ImaginaryPart}{\mathrm{Im}}$ $ \newcommand{\Argument}{\mathrm{Arg}}$ $ \newcommand{\norm}[1]{\| #1 \|}$ $ \newcommand{\inner}[2]{\langle #1, #2 \rangle}$ $ \newcommand{\Span}{\mathrm{span}}$

Template:MathJaxZach

Для того, щоб переконатися, що наше представництво працює, ми повинні довести дві речі. По-перше, ми повинні показати, що якщо$M$ зупиняється на вході$w$, то$T(M, w) \lif E(M, w)$ є дійсним. Потім, ми повинні показати зворотне, тобто, що якщо$T(M, w) \lif E(M, w)$ є дійсним, то$M$ насправді в кінцевому підсумку зупинити при запуску на вході$w$.

Стратегія доведення цього дуже різна. Для першого результату ми повинні показати, що речення логіки першого порядку (а саме,$T(M, w) \lif E(M, w)$) є дійсним. Найпростіший спосіб зробити це - дати деривацію. Наш доказ повинен працювати для всіх$w$,$M$ і, хоча, тому насправді немає жодного речення, для якого ми повинні дати похідну, але нескінченно багато. Тож найкраще, що ми можемо зробити, - це довести шляхом індукції, що, як би$M$ і не$w$ виглядало, і скільки б кроків не було потрібно$w$,$M$ щоб зупинити введення, буде виведення$T(M, w) \lif E(M, w)$.

Природно, наша індукція буде продовжувати кількість кроків, зроблених$M$ до того, як вона досягне конфігурації зупинки. У нашому індуктивному доказі ми встановимо, що для$n$ кожного кроку запуску$M$ на вході$w$$T(M, w) \Entails C(M, w, n)$, де$C(M, w, n)$ правильно описується конфігурація$M$ запуску на$w$ після$n$ кроків. Тепер, якщо$M$ зупиняється на вході$w$ після,$C(M, w, n)$ скажімо,$n$ кроків, опише конфігурацію зупинки. Ми також покажемо$C(M, w, n) \Entails E(M, w)$, що, всякий раз, коли$C(M, w, n)$ описує конфігурацію зупинки. Отже, якщо$M$ зупиняється на вході$w$, то для деяких$n$,$M$ буде в конфігурації зупинки після$n$ кроків. Отже,$T(M, w) \Entails C(M, w, n)$ де$C(M, w, n)$ описує зупинення конфігурації, і так як в цьому випадку$C(M, w, n) \Entails E(M, w)$, ми отримуємо$T(M, w) \Entails E(M, w)$, що, тобто, що$\Entails T(M, w) \lif E(M, w)$.

Стратегія для зворотного дуже різна. Тут ми припускаємо, що$\Entails T(M, w) \lif E(M, w)$ і повинні довести, що$M$ зупиняється на вході$w$. З гіпотези ми отримуємо$T(M, w) \Entails E(M, w)$, що,$E(M, w)$ тобто вірно в кожній структурі, в якій$T(M, w)$ вірно. Отже, ми опишемо структуру,$\Struct{M}$ в якій$T(M, w)$ вірно: її домен буде$\Nat$, а інтерпретація всіх$\Obj Q_q$ і$\Obj S_\sigma$ буде задаватися конфігураціями$M$ під час запуску на вході$w$. Так, наприклад,$\Sat{M}{\Obj Q_q(\num{m}, \num{n})}$ iff$T$, при запуску на вході$w$ для$n$ кроків, знаходиться в стані$q$ і сканування квадрат$m$. Тепер так як$T(M, w) \Entails E(M, w)$ гіпотезою, а так як$\Sat{M}{T(M, w)}$ конструкцією,$\Sat{M}{E(M, w)}$. Але$\Sat{M}{E(M, w)}$ якщо є деякі$n \in \Domain{M} = \Nat$ так$M$, що, запустити на вході$w$, знаходиться в зупинці конфігурації після$n$ кроків.

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

$C(M, w, n)$Дозволяти бути речення,\[\Obj Q_q(\num{m}, \num{n}) \land \Obj S_{\sigma_0}(\num{0}, \num{n}) \land \dots \land \Obj S_{\sigma_k}(\num{k}, \num{n}) \land \lforall{x}{(\num{k} < x \lif \Obj S_\TMblank(x, \num{n}))}\nonumber\] де$q$ є стан$M$ часу$n$,$M$ сканування квадрат$m$ в часі$n$, квадрат$i$ містить символ$\sigma_i$ на час$n$ для$0 \le i \le k$ і$k$ є крайнім правим непорожнім квадратом стрічки в той час$0$, або крайнім правим квадратом, який голова стрічки відвідала після$n$ кроків, залежно від того, що більше.

Лемма$\PageIndex{1}$

Якщо$M$ запустити на вході$w$ знаходиться в конфігурації зупинки після$n$ кроків, то$C(M, w, n) \Entails E(M, w)$.

Доказ. Припустимо, що$M$ зупиняється для введення$w$ після$n$ кроків. Існує певний стан$q$, квадрат і символ$\sigma$ такі$m$, що:

Після$n$ кроків,$M$ знаходиться в стані$q$ сканування квадрат,$m$ на якому$\sigma$ з'являється.
Функція переходу$\delta(q, \sigma)$ невизначена.

$C(M, w, n)$є описом цієї конфігурації і буде включати пункти$\Obj Q_{q}(\num{m}, \num{n})$ і$\Obj S_{\sigma}(\num{m}, \num{n})$. Ці пункти разом мають на увазі$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\] оскільки$\Obj Q_{q'}(\num{m}, \num{n}) \land S_{\sigma'}(\num{m}, \num{n}) \Entails \bigvee_{\tuple{q, \sigma} \in X} (\Obj Q_q(\num{m}, \num{n}) \land \Obj S_{\sigma}(\num{m}, \num{n}))$, як$\tuple{q',\sigma'} \in X$. ◻

Так що якщо$M$ зупинки для введення$w$, то є деякі$n$ такі, що$C(M, w, n) \Entails E(M,w)$. Зараз ми покажемо, що на будь-який час$n$,$T(M, w) \Entails C(M, w, n)$.

Лемма$\PageIndex{2}$

Для кожного$n$, якщо не$M$ зупинився після$n$ кроків,$T(M, w) \Entails C(M, w, n)$.

Доказ. Індукційна основа: Якщо$n = 0$, то кон'юнкти$C(M, w, 0)$ є також кон'юнктами з$T(M, w)$, так що тягне за собою.

Індуктивна гіпотеза: Якщо не$M$ зупинилася перед тим$n$ кроком, то$T(M,w) \Entails C(M, w, n)$. Ми повинні показати, що (якщо не$C(M, w, n)$ описує конфігурацію зупинки),$T(M, w) \Entails C(M, w, n+1)$.

Припустимо,$n > 0$ і після$n$ кроків,$M$ запущений на$w$ знаходиться в стані$q$ сканування квадрат$m$. Оскільки$M$ не зупиняється після$n$ кроків, у програмі повинна бути інструкція однієї з наступних трьох форм$M$:

$\delta(q, \sigma) = \tuple{q', \sigma', \TMright}$
$\delta(q, \sigma) = \tuple{q', \sigma', \TMleft}$
$\delta(q, \sigma) = \tuple{q', \sigma', \TMstay}$

Кожен з цих трьох випадків ми розглянемо по черзі.

Припустимо, є інструкція форми (1). За визначенням 13.5.1 (3a) це означає, що

\ [\ почати {вирівняний}
&\ lforall {x} {\ lforall {y} {((\ Obj Q_ {q} (x, y)\ земля\ Obj S_\ сигма (x, y))\ lif {}}}\\
&\ qquad (\ Obj Q_ {q'} (x ', y')\ земля\ Obj S_\ сигма} (x, y)\ земля A (x, y))
\ end {вирівняний}\]

є кон'юнктом$T(M,w)$. Це тягне за собою наступне речення (універсальний екземпляр,$\num{m}$ for$x$ і$\num{n}$ for$y$):

\ [\ почати {вирівняний}
& (\ Obj Q_ {q} (\ нум {м},\ нум {n})\ земля\ Obj S_ {\ сигма} (\ num {m},\ num {n})\ lif {}\
&\ qquad (\ Obj Q_ {q'} (\ num {m} ',\ num {n}')\ земля\ Obj S_ {\ сигма} (\ num {m},\ num {n} ')\ земля A (\ num {m},\ num {n})).
\ end {вирівняний}\]

За індукційною гіпотезою$T(M, w) \Entails C(M, w, n)$, тобто

\[\Obj Q_q(\num{m}, \num{n}) \land \Obj S_{\sigma_0}(\num{0}, \num{n}) \land \dots \land \Obj S_{\sigma_k}(\num{k}, \num{n}) \land \lforall{x}{(\num{k} < x \lif \Obj S_\TMblank(x, \num{n}))}\nonumber\]

Так як після$n$ кроків стрічка квадрат$m$ містить$\sigma$, відповідний кон'юнкт є$\Obj S_\sigma(\num{m}, \num{n})$, тому це тягне за собою:

\[\Obj Q_{q}(\num{m}, \num{n}) \land \Obj S_{\sigma}(\num{m}, \num{n})) \nonumber\]

Ми тепер отримуємо

\ [\ почати {вирівняний}
&\ Obj Q_ {q'} (\ нум {м} ',\ нум {n}')\ земля\ Obj S_ {\ сигма '} (\ num {m},\ num {n}')\ земля {\
&\ qquad\ Obj S_ {\ sigma_0} (\ num {0},\ num {n})\ земля\ точки\ земля\ Obj S_ {\ sigma_k} (\ нум {k},\ num {n} ')\ земля {}\
&\ qquad\ lforall {x} {(\ num {k} < х\ lif\ Obj S_\ tmБланк (x,\ num {n} '))}
\ кінець {вирівняний}\]

наступним чином: Перший рядок походить безпосередньо від наслідку попереднього умовного, modus ponens. Кожен кон'юнкт у середній лінії, який виключає$S_{\sigma_m}(\num{m},\num{n}')$ - випливає з відповідного кон'юнкту$C(M, w, n)$ разом з$A(\num{m}, \num{n})$.

Якщо$m < k$,$T(M,w) \Proves \num{m} < \num {k}$ (Пропозиція 13.5.1) і за транзитивністю$<$, ми маємо$\lforall{x}{(\num{k} < x \lif \num{m} < x)}$. Якщо$m = k$, то$\lforall{x}{(\num{k} < x \lif \num{m} < x)}$ по логіці поодинці. Останній рядок потім випливає з відповідного кон'юнкту в$C(M, w, n)$$\lforall{x}{(\num{k} < x \lif \num{m} < x)}$, і$A(\num{m}, \num{n})$. Якщо$m<k$, це вже є$C(M, w, n+1)$.

Тепер припустимо$m=k$. У такому випадку після$n+1$ кроків головка стрічки також відвідала квадрат$k+1$, який зараз є найправішим квадратом, який відвідується. Так$C(M, w, n+1)$ має новий кон'юнкт$\Obj S_\TMblank(\num{k}',\num{n}')$, і останній кон'юкт є$\lforall{x}{(\num{k}' < x \lif \Obj S_\TMblank(x, \num{n}'))}$. Ми повинні переконатися, що ці два речення також маються на увазі.

У нас вже є$\lforall{x}{(\num{k} < x \lif \Obj S_\TMblank(x, \num{n}'))}$. Зокрема, це дає нам$\num{k} < \num{k}' \lif \Obj S_\TMblank(\num{k}', \num{n}')$. З$\lforall{x}{x < x'}$ аксіоми отримуємо$\num{k} < \num{k}'$. За модусом ponens,$\Obj S_\TMblank(\num{k}',\num{n}')$ слід.

Крім того, оскільки$T(M,w) \Proves \num{k} < \num{k}'$, аксіома для транзитивності$<$ дає нам$\lforall{x}{(\num{k}' < x \lif \Obj S_\TMblank(x, \num{n}'))}$. (Ми залишаємо перевірку цього як вправу.)
Припустимо, є інструкція форми (2). Тоді, за визначенням 13.5.1 (3b)

\ [\ почати {вирівняний}
&\ lforall {x} {\ lforall {y} {((\ Obj Q_ {q} (x ', y)\ земля\ Obj S_ {\ сигма} (x', y))\ lif {}}\\
&\ qquad (\ Obj Q_ {q'} (x, y)\ земля\ Obj S_ _ {\ сигма} (x ', y')\ земля A (x, y))\ земля {}\
&\ lforall {y} {(\ Obj Q_ {q_i} (\ Obj 0, y)\ земля\ Obj S _ {\ сигма} (\ Obj 0, y))\ lif {}}\\
&\ qquad (\ Obj Q_ {q_j} (\ Obj 0, y')\ земля\ Obj S_ {\ сигма} (\ Obj 0, y)\ земля A (\ Obj 0, y)))
\ кінець {вирівняний}\]

є кон'юнктом$T(M,w)$. Якщо$m>0$, то нехай$l = m - 1$ (тобто$m = l+1$). Перший сполучник вищевказаного речення тягне за собою наступне:

\ [\ почати {вирівняний}
& (\ Obj Q_ {q} (\ нум {л} ',\ нум {n})\ земля\ Obj S_ {\ сигма} (\ num {l}',\ num {n})\ lif {}\
&\ qquad (\ Obj Q_ {q'}} (\ num {l},\ num {n}\\ n} ') земля\ Obj S_ {\ сигма} (\ num {l}',\ num {n} ')\ земля A (\ num {l},\ num {n}))
\ кінець {вирівняний}\]

В іншому випадку нехай$l = m = 0$ і розглянемо наступне речення, яке тягне за собою другий кон'юнкт:

\ [\ почати {вирівняний}
& (\ Obj Q_ {q_i} (\ Obj 0,\ нум {n})\ земля\ Obj S_ {\ сигма} (\ Obj 0,\ нум {n})\ lif {}\
&\ qquad (\ Obj Q_ {q_j} (\ Obj 0,\ num {n} ')\ земля\ Obj S_ {\ сигма} (\ Obj 0,\ нум {n}')\ земля A (\ Obj 0,\ num {n}))
\ end {вирівняний}\]

Будь-яке речення має на увазі

\ [\ почати {вирівняний}
&\ Obj Q_ {q'} (\ нум {л},\ нум {n} ')\ земля\ Obj S_ {\ сигма'} (\ num {m},\ num {n} ')\ земля {\
&\ qquad\ Obj S_ {\ sigma_0} (\ num {0},\ num {n}')\ земля\ точки\ земля\ Obj S_ {\ sigma_k} (\ нум {k},\ нум {n} ')\ земля {}\\
&\ qquad\ lforall {x} {(\ num {k} < х\ lif\ Obj S_\ tmБланк (x,\ num {n} '))}
\ кінець {вирівняний}\]

як і раніше. (Зверніть увагу, що і в першому випадку,$\num{l}' \ident \num{l+1} \ident \num{m}$ і в другому випадку$\num{l} \ident \Obj 0$.) Але це якраз і є$C(M, w, n+1)$.
Справа (3) залишають як вправу.

Ми показали, що для будь-якого$n$,$T(M, w) \Entails C(M, w, n)$. ◻

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

Повний випадок (3) доказу Лемми$\PageIndex{2}$.

Проблема$\PageIndex{2}$

Дайте похідні$\Obj S_{\sigma_i}(\num{i}, \num{n}')$ від$\Obj S_{\sigma_i}(\num{i}, \num{n})$ і$A(m, n)$ (припускаючи$i \neq m$, тобто або$i < m$ або$m < i$).

Проблема$\PageIndex{3}$

Дайте похідні$\lforall{x}{(\num{k}' < x \lif \Obj S_\TMblank(x, \num{n}'))}$ від$\lforall{x}{(\num{k} < x \lif \Obj S_\TMblank(x, \num{n}'))}$$\lforall{x}{x < x'}$, і$\lforall{x}{\lforall{y}{\lforall{z}{ ((x < y \land y < z) \lif x < z)}}}$.)

Лемма$\PageIndex{3}$

Якщо$M$ зупиняється на вході$w$, то$T(M, w) \lif E(M, w)$ є дійсним.

Доказ. За Леммою$\PageIndex{2}$ ми знаємо, що для будь-якого часу$n$ опис$C(M, w, n)$ конфігурації$M$ часу тягне за$n$ собою$T(M, w)$. Припустимо$M$ зупинки після$k$ кроків. Це буде сканування квадрата$m$, скажімо. Потім$C(M, w, k)$ описує конфігурацію зупинки$M$, тобто вона містить як сполучники як, так$\Obj Q_q(\num{m}, \num{k})$ і$\Obj S_\sigma(\num{m}, \num{k})$ з$\delta(q,\sigma)$ undefined. Таким чином, Лемма$\PageIndex{1}$,$C(M, w, k) \Entails E(M, w)$. Але з тих пір$T(M, w) \Entails C(M, w, k)$, у нас$T(M, w) \lif E(M, w)$ є$T(M, w) \Entails E(M, w)$ і тому діє. ◻

Щоб завершити перевірку нашої претензії, ми також повинні встановити зворотний напрямок: якщо$T(M, w) \lif E(M, w)$ дійсний, то фактично$M$ зупиняється при запуску на вході$m$.

Лемма$\PageIndex{4}$

Якщо$\Entails T(M, w) \lif E(M, w)$, то$M$ зупиняється на вході$w$.

Доказ. Розглянемо$\Lang L_M$ -структуру$\Struct M$ з доменом$0$,$\Nat$ яка$\Obj 0$ інтерпретує$'$ як функцію наступника, і$<$ як відношення менше ніж, і предикати $\Obj Q_q$і$\Obj S_\sigma$ наступним чином:\[\begin{aligned} \Assign{\Obj Q_q}{M} & = \Setabs{\tuple{m, n}}{\begin{array}{ll}\text{started on $w$, after $n$ steps,}\\ \text{$M$ is in state $q$ scanning square $m$}\end{array}} \\ \Assign{\Obj S_\sigma}{M} & = \Setabs{\tuple{m, n}}{\begin{array}{ll} \text{started on $w$, after $n$ steps,}\\ \text{square $m$ of $M$ contains symbol $\sigma$}\end{array}}\end{aligned}\] Іншими словами, ми будуємо структуру$\Struct{M}$ так, щоб вона описувала те, що$M$ почалося на вході$w$ насправді робить, крок за кроком. Зрозуміло,$\Sat{M}{T(M, w)}$. Якщо$\Entails T(M, w) \lif E(M, w)$, то також$\Sat{M}{E(M, w)}$, тобто,\[\Sat{M}{\lexists{x}{\lexists{y}{(\bigvee_{\tuple{q, \sigma} \in X}(\Obj Q_q(x, y) \land \Obj S_\sigma(x, y)))}}}.\nonumber\] як$\Domain{M} = \Nat$, там повинно бути$m$,$n \in \Nat$ щоб$\Sat{M}{\Obj Q_q(\num{m}, \num{n}) \land \Obj S_\sigma(\num{m}, \num{n})}$ для деяких$q$ і$\sigma$ таких що $\delta(q, \sigma)$не визначено. За визначенням$\Struct M$, це означає, що$M$ запущений на вході$w$ після$n$ кроків знаходиться в стані$q$ і читає символ$\sigma$, а функція переходу undefined, тобто $M$зупинився. ◻