¿Es un bucle un cuantificador?

Question

En algún lugar leí que el cuantificador universal, es decir $\forall p$ , podría interpretarse como una secuencia de conjunciones de proposiciones, elementos o variables: $p_1\land p_2 \land... \land p_n... $

Lo mismo podría decirse del cuantificador existencial, podría interpretarse como una secuencia de disyunciones.

Pero, un bucle, utilizado en lenguaje informático, (es decir, for, while) es una secuencia de condiciones.

Entonces, ¿puedo interpretar un bucle, utilizado en el lenguaje informático, como una especie de cuantificador? Por ejemplo, ¿podría traducirse ''while (i!=10)...'' como '' $\forall i(i\in \Bbb N,(i \neq 10) \to P(i))$ ''? Si no, ¿por qué?

Answer 1

En el siguiente sentido se puede formalizar utilizando la cuantificación de segundo orden.

En el Cálculo de Situación (una teoría de la acción), mientras que se define como una acción compleja de la siguiente manera:

$ while\ \phi\ do\ \delta\ endWhile \stackrel{def}{=} [\phi?; \delta]^*;\neg \phi?$

donde $\delta^*$ significa hacer $\delta$ cero o más veces y se define como sigue:

\begin{align*} Do(\delta&^*,s,s')\stackrel{def}{=}\\ &(\forall P).\{(\forall s_1)P(s_1,s_1)\land(\forall s_1,s_2,s_3)[Do(\delta,s_1,s_2)\land P(s_2,s_3)\supset P(s_1,s_3)]\}\supset P(s,s'). \end{align*} Lo que implica una cuantificación de segundo orden.

Para todas las definiciones y más detalles, puede consultar el capítulo 6 del libro El conocimiento en acción (2001) . Aquí doy algunas de las definiciones.

Una situación es una secuencia finita de acciones. $do(a,s)$ es la situación que se obtiene al ejecutar la acción $a$ en situación $s$ . $Do(\delta,s,s')$ significa que "es posible llegar a la situación $s'$ de la situación $s$ ejecutando una secuencia de acciones especificadas por $\delta$ ".

• Acciones primitivas: $Do(a,s,s')\stackrel{def}{=}Poss(a[s],s)\land s'=do(a[s],s)$ .
• Acciones de prueba: $Do(\phi?,s,s')\stackrel{def}{=}\phi[s]\land s'=s$ .
• Secuencia: $Do(\delta_1;\delta_2,s,s')\stackrel{def}{=}(\exists s'').Do(\delta_1,s,s'')\land Do(\delta_2,s'',s')$ .

$-------------$

Más información sobre el cálculo de situaciones:

El lenguaje del Cálculo de Situación es un lenguaje de primer orden ordenado (con algunos elementos de segundo orden). Hay tres tipos: acción para las acciones, situación para las situaciones, y objeto para todo lo demás. Una constante distinguida $S_0$ representa la situación inicial, y un símbolo de función distinguida $do:action\times situation\rightarrow situation$ representa la ejecución de una acción. A situación es una secuencia finita de acciones a partir de la situación inicial. Un símbolo de predicado binario $\sqsubset$ define una relación de ordenación sobre las situaciones. A fluido es un hecho cuyo valor de verdad puede variar de una situación a otra; es un predicado que toma una situación como argumento final (e.x. $holding(x,s)$ , lo que significa que "el agente tiene un objeto $x$ en situación $s$ "). Un predicado distinguido $Poss:action\times situation$ denota que es posible ejecutar una acción en una situación.

La expresión $Do(\delta,s,s')$ (definido anteriormente) es una abreviatura de una fórmula de SitCalc. Se utiliza para definir acciones complejas.

Answer 2

Algunas versiones de $\forall$ pueden traducirse en bucles y otras no. En concreto, cuando el dominio del cuantificador es constructivamente isomorfo a los números naturales, y cuando el argumento del cuantificador es traducible a un procedimiento de decisión, entonces es posible una traducción general. Ejemplos:

$$\forall x \in \mathbb N ~:~ 2|x \lor 2|(x + 1)$$

El dominio del bucle son los números naturales, y la divisibilidad se puede escribir como un procedimiento de decisión, por lo que es justo:

for i = 0; true; i++
  if (i % 2) == 0 return true
  if ((i + 1) % 2 == 0 return true

Por otro lado:

$$\forall x \in \mathbb R ~:~ f(x) \ne x$$

No se puede expresar como un bucle ya que los números reales no son isomorfos a los números naturales. No se puede hacer un bucle a través de los números reales. También

$$\forall x \in \mathbb N ~:~ P \text{ is a program that converges on input } x$$

Podría no ser completamente traducible en un bucle ya que no se puede escribir un procedimiento de decisión que afirme la divergencia. Además, algunas lógicas tienen reglas diferentes para la cuantificación que no hacen ninguna suposición sobre el dominio, como por ejemplo

$$\forall x ~:~ (Px \to \exists y ~:~ Py)$$

es un demostrable en la deducción natural debido a su $\forall$ normas, a pesar de no tener ninguna traducción obvia como procedimiento de decisión.