13.6: Verificación de la Representación

Última actualización
Guardar como PDF

Page ID: 103670

$ \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}}$$\newcommand{\AA}{\unicode[.8,0]{x212B}}$

Template:MathJaxZach

Para verificar que nuestra representación funcione, tenemos que probar dos cosas. Primero, tenemos que demostrar que si se$M$ detiene en la entrada$w$, entonces$T(M, w) \lif E(M, w)$ es válido. Entonces, tenemos que mostrar lo contrario, es decir, que si$T(M, w) \lif E(M, w)$ es válido, entonces$M$ de hecho finalmente se detiene cuando se ejecuta en la entrada$w$.

La estrategia para demostrarlos es muy diferente. Para el primer resultado, tenemos que demostrar que una frase de lógica de primer orden (es decir,$T(M, w) \lif E(M, w)$) es válida. La forma más fácil de hacerlo es dar una derivación. Se supone que nuestra prueba funciona para todos$M$ y$w$, sin embargo, así que en realidad no hay una sola oración para la que tengamos que dar una derivación, sino infinitamente muchas. Entonces lo mejor que podemos hacer es demostrar por inducción que, lo que sea$M$ y$w$ parezca, y por muchos pasos que tome$M$ para detenernos en la entrada$w$, habrá una derivación de$T(M, w) \lif E(M, w)$.

Naturalmente, nuestra inducción procederá en el número de pasos que$M$ toma antes de que alcance una configuración de detención. En nuestra prueba inductiva, estableceremos que para cada paso$n$ de la ejecución de$M$ on input$w$,$T(M, w) \Entails C(M, w, n)$, donde describe$C(M, w, n)$ correctamente la configuración de$M$ run on$w$ después de$n$ los pasos. Ahora bien, si$M$ se detiene en la entrada$w$ después de, digamos,$n$ pasos,$C(M, w, n)$ se describirá una configuración de detención. También mostraremos eso$C(M, w, n) \Entails E(M, w)$, siempre que$C(M, w, n)$ describa una configuración de detención. Entonces, si$M$ se detiene en la entrada$w$, entonces para algunos$n$,$M$ estará en una configuración de detención después de$n$ los pasos. De ahí,$T(M, w) \Entails C(M, w, n)$ donde$C(M, w, n)$ describe una configuración de detención, y ya que en ese caso$C(M, w, n) \Entails E(M, w)$, obtenemos eso$T(M, w) \Entails E(M, w)$, es decir, eso$\Entails T(M, w) \lif E(M, w)$.

La estrategia para lo contrario es muy diferente. Aquí asumimos eso$\Entails T(M, w) \lif E(M, w)$ y tenemos que demostrar que se$M$ detiene en la entrada$w$. De la hipótesis obtenemos que$T(M, w) \Entails E(M, w)$, es decir,$E(M, w)$ es cierto en toda estructura en la que$T(M, w)$ es verdadera. Entonces describiremos una estructura$\Struct{M}$ en la que$T(M, w)$ es verdadera: su dominio será$\Nat$, y la interpretación de todos los$\Obj Q_q$ y$\Obj S_\sigma$ estará dada por las configuraciones de$M$ durante una ejecución en la entrada$w$. Entonces, por ejemplo,$\Sat{M}{\Obj Q_q(\num{m}, \num{n})}$ iff$T$, cuando se ejecuta en la entrada$w$ para$n$ pasos, está en estado$q$ y escaneo cuadrado$m$. Ahora desde$T(M, w) \Entails E(M, w)$ por hipótesis, y desde$\Sat{M}{T(M, w)}$ por construcción,$\Sat{M}{E(M, w)}$. Pero$\Sat{M}{E(M, w)}$ si hay algunos$n \in \Domain{M} = \Nat$ para que$M$, ejecutar en la entrada$w$, esté en una configuración de detención después de$n$ los pasos.

Definición$\PageIndex{1}$

Dejar$C(M, w, n)$ ser la oració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\] donde$q$ está el estado de$M$ en el tiempo$n$,$M$ está escaneando cuadrado$m$ en tiempo$n$, cuadrado$i$ contiene el símbolo$\sigma_i$ en el momento$n$$0 \le i \le k$ y$k$ es el cuadrado no blanco más a la derecha de la cinta en el momento$0$, o el cuadrado más a la derecha que el cabezal de la cinta haya visitado después de$n$ los pasos, lo que sea mayor.

Lema$\PageIndex{1}$

Si$M$ ejecutar en la entrada$w$ está en una configuración de detención después de$n$ los pasos, entonces$C(M, w, n) \Entails E(M, w)$.

Comprobante. Supongamos que$M$ se detiene para la entrada$w$ después de$n$ los pasos. Hay algún estado$q$$m$, cuadrado y símbolo$\sigma$ tal que:

Después de$n$ los pasos,$M$ se encuentra en el estado$q$ de escaneo cuadrado$m$ en el que$\sigma$ aparece.
La función de transición no$\delta(q, \sigma)$ está definida.

$C(M, w, n)$es la descripción de esta configuración e incluirá las cláusulas$\Obj Q_{q}(\num{m}, \num{n})$ y$\Obj S_{\sigma}(\num{m}, \num{n})$. Estas cláusulas en conjunto implican$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\] ya que$\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}))$, como$\tuple{q',\sigma'} \in X$. ◻

Entonces si$M$ se detiene por entrada$w$, entonces hay algunos$n$ tales que$C(M, w, n) \Entails E(M,w)$. Ahora vamos a mostrar eso para cualquier momento$n$,$T(M, w) \Entails C(M, w, n)$.

Lema$\PageIndex{2}$

Para cada uno$n$, si no se$M$ ha detenido después de$n$ los pasos,$T(M, w) \Entails C(M, w, n)$.

Comprobante. Base de inducción: Si$n = 0$, entonces las conjunciones de$C(M, w, 0)$ son también conjunciones de$T(M, w)$, así lo conllevan.

Hipótesis inductiva: Si no se$M$ ha detenido antes del paso$n$ th, entonces$T(M,w) \Entails C(M, w, n)$. Tenemos que demostrar que (a menos que$C(M, w, n)$ describa una configuración de detención),$T(M, w) \Entails C(M, w, n+1)$.

Supongamos$n > 0$ y después de$n$ los pasos,$M$ iniciado en$w$ está en el estado$q$ de escaneo cuadrado$m$. Dado que$M$ no se detiene después de$n$ los pasos, debe haber una instrucción de una de las siguientes tres formas en el programa de$M$:

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

Consideraremos cada uno de estos tres casos a su vez.

Supongamos que hay una instrucción de la forma (1). Por Definición 13.5.1 (3a), esto significa que

\ [\ comenzar {alineado}
&\ lforall {x} {\ lforall {y} {((\ Obj Q_ {q} (x, y)\ tierra\ Obj S_\ sigma (x, y))\ lif {}}}\\
&\ qquad (\ Obj Q_ {q'} (x', y')\ tierra\ Obj S_ {\ sigma_ '} (x, y')\ tierra A (x, y))
\ final {alineado}\]

es una conjunción de$T(M,w)$. Esto conlleva la siguiente frase (instanciación universal,$\num{m}$ para$x$ y$\num{n}$ para$y$):

\ [\ comenzar {alineado}
& (\ Obj Q_ {q} (\ num {m},\ num {n})\ tierra\ Obj S_ {\ sigma} (\ num {m},\ num {n}))\ lif {}\\
&\ qquad (\ Obj Q_ {q'} (\ num {m} ',\ num {n}')\ tierra\ Obj S_ {\ sigma'} (\ num {m},\ num {n} ')\ tierra A (\ num {m},\ num {n})).
\ end {alineado}\]

Por hipótesis de inducción$T(M, w) \Entails C(M, w, n)$, es decir,

\[\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\]

Ya que después de$n$ los pasos, la cinta cuadrada$m$ contiene$\sigma$, la conjunción correspondiente es$\Obj S_\sigma(\num{m}, \num{n})$, por lo que esto conlleva:

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

Ahora conseguimos

\ [\ begin {alineado}
&\ Obj Q_ {q'} (\ num {m} ',\ num {n}')\ tierra\ Obj S_ {\ sigma'} (\ num {m},\ num {n} ')\ tierra {}\\
&\ qquad\ Obj S_ {\ sigma_0} (\ num {0},\ num {n})\ tierra\ puntos\ tierra\ Obj S_ {\ sigma_k} (\ num {k},\ num {n}')\ tierra {}\\\
&\ qquad\ lforall {x} {(\ num {k} < x\ lif\ Obj S_\ tmEn blanco (x,\ num {n} '))}
\ final {alineado}\]

de la siguiente manera: La primera línea viene directamente del consecuente del condicional precedente, por modus ponens. Cada conjunción en la línea media —que excluye$S_{\sigma_m}(\num{m},\num{n}')$ — sigue de la conjunción correspondiente$C(M, w, n)$ junto con$A(\num{m}, \num{n})$.

Si$m < k$,$T(M,w) \Proves \num{m} < \num {k}$ (Proposición 13.5.1) y por transitividad de$<$, tenemos$\lforall{x}{(\num{k} < x \lif \num{m} < x)}$. Si$m = k$, entonces solo$\lforall{x}{(\num{k} < x \lif \num{m} < x)}$ por lógica. La última línea sigue entonces de la conjunción correspondiente en$C(M, w, n)$,$\lforall{x}{(\num{k} < x \lif \num{m} < x)}$, y$A(\num{m}, \num{n})$. Si$m<k$, esto ya lo es$C(M, w, n+1)$.

Ahora supongamos$m=k$. En ese caso, después de$n+1$ escalones, el cabezal de cinta también ha visitado plaza$k+1$, que ahora es la plaza más a la derecha visitada. Así$C(M, w, n+1)$ tiene una nueva conjunción,$\Obj S_\TMblank(\num{k}',\num{n}')$, y el último conjuto lo es$\lforall{x}{(\num{k}' < x \lif \Obj S_\TMblank(x, \num{n}'))}$. Tenemos que verificar que estas dos frases también están implícitas.

Ya lo tenemos$\lforall{x}{(\num{k} < x \lif \Obj S_\TMblank(x, \num{n}'))}$. En particular, esto nos da$\num{k} < \num{k}' \lif \Obj S_\TMblank(\num{k}', \num{n}')$. Del axioma$\lforall{x}{x < x'}$ obtenemos$\num{k} < \num{k}'$. Por modus ponens,$\Obj S_\TMblank(\num{k}',\num{n}')$ sigue.

También, ya que$T(M,w) \Proves \num{k} < \num{k}'$, el axioma para la transitividad de nos$<$ da$\lforall{x}{(\num{k}' < x \lif \Obj S_\TMblank(x, \num{n}'))}$. (Dejamos la verificación de esto como ejercicio.)
Supongamos que hay una instrucción de la forma (2). Entonces, por la Definición 13.5.1 (3b),

\ [\ begin {alineado}
&\ lforall {x} {\ lforall {y} {((\ Obj Q_ {q} (x', y)\ tierra\ Obj S_ {\ sigma} (x', y))\ lif {}}}\\
&\ qquad (\ Obj Q_ {q'} (x, y')\ tierra\ Obj S_ {\ sigma'} (x', y')\ tierra A (x, y))\ tierra {}\\\
&\ lforall {y} {((\ Obj Q_ {q_i} (\ Obj 0, y)\ tierra\ Obj S _ {\ sigma} (\ Obj 0, y))\ lif {}}\\
&\ qquad (\ Obj Q_ {q_j} (\ Obj 0, y')\ tierra\ Obj S_ {\ sigma'} (\ Obj 0, y')\ tierra A (\ Obj 0, y)))
\ fin {alineado}\]

es una conjunción de$T(M,w)$. Si$m>0$, entonces vamos$l = m - 1$ (es decir,$m = l+1$). La primera conjunción de la frase anterior conlleva lo siguiente:

\ [\ comenzar {alineado}
& (\ Obj Q_ {q} (\ num {l} ',\ num {n})\ tierra\ Obj S_ {\ sigma} (\ num {l}',\ num {n}))\ lif {}\\
&\ qquad (\ Obj Q_ {q'} (\ num {l},\ num {n} ')\ tierra\ Obj S_ {\ sigma'} (\ num {l}',\ num {n} ')\ tierra A (\ num {l},\ num {n}))
\ final {alineado}\]

En caso contrario, tomemos$l = m = 0$ y consideremos la siguiente frase que conlleva la segunda conjunción:

\ [\ comenzar {alineado}
& (\ Obj Q_ {q_i} (\ Obj 0,\ num {n})\ tierra\ Obj S_ {\ sigma} (\ Obj 0,\ num {n})\ lif {}\\
&\ qquad (\ Obj Q_ {q_j} (\ Obj 0,\ num {n} ')\ tierra\ Obj S_ {\ sigma'} (\ Obj 0,\ num {n}')\ tierra A (\ Obj 0,\ num {n}))
\ final {alineado}\]

Cualquiera de las dos frases implica

\ [\ begin {alineado}
&\ Obj Q_ {q'} (\ num {l},\ num {n} ')\ tierra\ Obj S_ {\ sigma'} (\ num {m},\ num {n}')\ tierra {}\\
&\ qquad\ Obj S_ {\ sigma_0} (\ num {0},\ num {n} ')\ tierra\ puntos\ tierra\ Obj S_ {\ sigma_k} (\ num {k},\ num {n}')\ tierra {}\\\
&\ qquad\ lforall {x} {(\ num {k} < x\ lif\ Obj S_\ tmEn blanco (x,\ num {n} '))}
\ final {alineado}\]

como antes. (Obsérvese que en el primer caso,$\num{l}' \ident \num{l+1} \ident \num{m}$ y en el segundo$\num{l} \ident \Obj 0$.) Pero esto solo lo es$C(M, w, n+1)$.
El caso (3) se deja como ejercicio.

Eso lo hemos demostrado para cualquier$n$,$T(M, w) \Entails C(M, w, n)$. ◻

Problema$\PageIndex{1}$

Caso completo (3) del comprobante de Lemma$\PageIndex{2}$.

Problema$\PageIndex{2}$

Dar una derivación$\Obj S_{\sigma_i}(\num{i}, \num{n}')$ de$\Obj S_{\sigma_i}(\num{i}, \num{n})$ y$A(m, n)$ (asumiendo$i \neq m$, es decir, cualquiera$i < m$ o$m < i$).

Problema$\PageIndex{3}$

Dar una derivación$\lforall{x}{(\num{k}' < x \lif \Obj S_\TMblank(x, \num{n}'))}$ de$\lforall{x}{(\num{k} < x \lif \Obj S_\TMblank(x, \num{n}'))}$,$\lforall{x}{x < x'}$, y$\lforall{x}{\lforall{y}{\lforall{z}{ ((x < y \land y < z) \lif x < z)}}}$.)

Lema$\PageIndex{3}$

Si$M$ se detiene en la entrada$w$, entonces$T(M, w) \lif E(M, w)$ es válido.

Comprobante. Por Lemma$\PageIndex{2}$, sabemos que, para cualquier momento$n$, la descripción$C(M, w, n)$ de la configuración de$M$ en el momento$n$ está implicada por$T(M, w)$. Supongamos que$M$ se detiene después de$k$ pasos. Será escaneo cuadrado$m$, digamos. Luego$C(M, w, k)$ describe una configuración de detención de$M$, es decir, contiene como conjunciones tanto como$\Obj Q_q(\num{m}, \num{k})$$\Obj S_\sigma(\num{m}, \num{k})$ con$\delta(q,\sigma)$ indefinido. Así, por Lemma$\PageIndex{1}$,$C(M, w, k) \Entails E(M, w)$. Pero ya que$T(M, w) \Entails C(M, w, k)$, tenemos$T(M, w) \Entails E(M, w)$ y por lo tanto$T(M, w) \lif E(M, w)$ es válido. ◻

Para completar la verificación de nuestro reclamo, también tenemos que establecer la dirección inversa: si$T(M, w) \lif E(M, w)$ es válida, entonces de hecho$M$ se detiene cuando se inicia en la entrada$m$.

Lema$\PageIndex{4}$

Si$\Entails T(M, w) \lif E(M, w)$, entonces se$M$ detiene en la entrada$w$.

Comprobante. Considerar la$\Lang L_M$ -estructura$\Struct M$ con dominio$\Nat$ que interpreta$\Obj 0$ como$0$,$'$ como la función sucesora, y$<$ como la relación menor que, y los predicados $\Obj Q_q$y de la$\Obj S_\sigma$ siguiente manera:\[\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}\] En otras palabras, construimos la estructura$\Struct{M}$ para que describa lo que$w$ realmente hace el$M$ inicio de la entrada, paso a paso. Claramente,$\Sat{M}{T(M, w)}$. Si$\Entails T(M, w) \lif E(M, w)$, entonces también$\Sat{M}{E(M, w)}$, es decir$\Domain{M} = \Nat$,\[\Sat{M}{\lexists{x}{\lexists{y}{(\bigvee_{\tuple{q, \sigma} \in X}(\Obj Q_q(x, y) \land \Obj S_\sigma(x, y)))}}}.\nonumber\] As, debe haber$m$,$\Sat{M}{\Obj Q_q(\num{m}, \num{n}) \land \Obj S_\sigma(\num{m}, \num{n})}$ para$n \in \Nat$ que para algunos$q$ y$\sigma$ tal que $\delta(q, \sigma)$está indefinido. Por la definición de$\Struct M$, esto significa que$M$ comenzó en la entrada$w$ después de$n$ los pasos está en estado$q$ y símbolo de lectura$\sigma$, y la función de transición es indefinida, es decir, $M$se ha detenido. ◻