Is a loop a quantifier?

Question

Somewhere I read that the universal quantifier, i.e. $\forall p$, could be interpreted as a sequence of conjunctions of propositions, elements or variables: $p_1\land p_2 \land... \land p_n... $

The same could be said of the existential quantifier, it could be interpreted a sequence of disjunctions.

But, a loop, used in computer language, (i.e. for, while) is a sequence of conditions.

So, can I interpret a loop, used in computer language, as a kind of quantifier? For example, could ''while (i!=10)...'' be translated as ''$\forall i(i\in \Bbb N,(i \neq 10) \to P(i))$''? If not, why?

Answer 1

In the following sense it can be formalized using second order quantification.

In the Situation Calculus (a theory of action), while is defined as a complex action as follows:

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

where $\delta^*$ means doing $\delta$ zero or more times and is defined as follows:

\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*} Which involves second order quantification.

For all definitions and more details you can see chapter 6 of the book Knowledge in Action (2001). Here I give some of the definitions.

A situation is a finite sequence of actions. $do(a,s)$ is the situation obtained from executing action $a$ in situation $s$. $Do(\delta,s,s')$ means "it is possible to reach situation $s'$ from situation $s$ by executing a sequence of actions specified by $\delta$".

• Primitive actions: $Do(a,s,s')\stackrel{def}{=}Poss(a[s],s)\land s'=do(a[s],s)$.
• Test actions: $Do(\phi?,s,s')\stackrel{def}{=}\phi[s]\land s'=s$.
• Sequence: $Do(\delta_1;\delta_2,s,s')\stackrel{def}{=}(\exists s'').Do(\delta_1,s,s'')\land Do(\delta_2,s'',s')$.

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

More on Situation Calculus:

The language of the Situation Calculus is a many-sorted first order language (with some second-order elements). There are three sorts: action for actions, situation for situations, and object for everything else. A distinguished constant $S_0$ represents the initial situation, and a distinguished function symbol $do:action\times situation\rightarrow situation$ represents the execution of an action. A situation is a finite sequence of actions starting from the initial situation. A binary predicate symbol $\sqsubset$ defines an ordering relation on situations. A fluent is a fact whose truth value may vary from situation to situation; it is a predicate that takes a situation as the final argument (e.x. $holding(x,s)$, meaning "the agent is holding object $x$ in situation $s$"). A distinguished predicate $Poss:action\times situation$ denotes it is possible to execute an action in a situation.

The expression $Do(\delta,s,s')$ (defined above) is a shorthand for a formula of SitCalc. It is used to define complex actions.

Answer 2

Some versions of $\forall$ can be translated into loops and some cannot. Specifically, when the domain of the quantifier is constructively isomorphic to natural numbers, and when argument to the quantifier is translatable into a decision procedure, then a general translation is possible. Examples:

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

The domain of the loop is natural numbers, and divisibility can be written as a decision procedure, so this is just:

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

On the other hand:

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

Can't be expressed as a loop since real numbers are not isomorphic to natural numbers. You can't loop through real numbers. Also

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

Arguably might not be completely translatable into a loop since you can't actually write a decision procedure that asserts divergence. Also, some logics just have different rules for quantification that don't make any assumptions about the domain at all, such as

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

is a provable in natural deduction because of its $\forall$ rules, despite not have any obvious translation as a decision procedure.