<p>Let's say I wanted to <em>informally</em> describe a very simple algorithm for searching through an (undirected) finite connected graph <span class="math-container">$G = (V,E)$</span>. I could define, for each natural number <span class="math-container">$n$</span>, a set <span class="math-container">$S_n$</span> and a list <span class="math-container">$L_n$</span> as follows:</p>
<p>Initially, <span class="math-container">$S_0$</span> is initialized to some vertex <span class="math-container">$v_0$</span> and <span class="math-container">$L_0 = ()$</span>, the empty list.
Thereafter, if <span class="math-container">$S_n \setminus L_n$</span> is nonempty, pick <span class="math-container">$v_n \in S_n \setminus L_n$</span>. Let <span class="math-container">$L_{n+1} = (L_n , v_n)$</span> and <span class="math-container">$S_{n+1} = S_n \cup \Gamma v_n$</span>, where <span class="math-container">$\Gamma v$</span> means the neighborhood of <span class="math-container">$v$</span>.
(If <span class="math-container">$S_n \setminus L_n$</span> is empty, simply let <span class="math-container">$S_{n+1} = S_n$</span> and <span class="math-container">$L_{n+1} = L_n$</span>.)</p>
<p>Once the recursion stabilizes, <span class="math-container">$S$</span> is equal to <span class="math-container">$V$</span> and <span class="math-container">$L$</span> is some traversal of the vertices of <span class="math-container">$G$</span>.
Luckily, we don't need such cumbersome notation, because we could express this algorithm in a natural program syntax:</p>
<p><span class="math-container">$S = \{v_0\},\ L = () \\ \mathtt{while\ } S \setminus L \neq \emptyset, \\ \ \ \mathtt{pick}\ v \in S \setminus L \\ \ \ L = (L,v) \\ \ \ S = S \cup \Gamma v$</span></p>
<p><strong>Now</strong> suppose that I wanted to extend this algorithm to <strong>infinite</strong> graphs. This is a straightforward: I define <span class="math-container">$S_\alpha$</span> and <span class="math-container">$L_\alpha$</span> for <em>ordinals</em> <span class="math-container">$\alpha$</span>; the successor stages are exactly like above, and I take limits of <span class="math-container">$L$</span> and unions of <span class="math-container">$S$</span> at limit stages: i.e., for <span class="math-container">$\alpha$</span> limit,</p>
<p><span class="math-container">$L_\alpha = \lim_{\beta &lt; \alpha} L_\beta$</span>, <span class="math-container">$S_\alpha = \bigcup_{\beta &lt; \alpha} S_\beta$</span>.</p>
<p>Once this recursion stabilizes, <span class="math-container">$S$</span> again equals <span class="math-container">$V$</span>, and <span class="math-container">$L$</span> is a (well-ordered) traversal of the vertices of <span class="math-container">$G$</span>.</p>
<p>However, I lack a clear <strong>syntax</strong> for expressing this algorithm. Really, the while loop above should work, given the right semantics. However, that semantics should account for while loops that can be iterated any ordinal number of times, whereas in any standard (e.g., operational) semantics, a while loop that does not terminate after a finite number of steps diverges. Therefore my question is</p>
<p><strong>Is there a formal semantics for the while loop above according to which it correctly computes infinite graph search?</strong></p>
<p>More generally,</p>
<p><strong>is there a community of researchers that studies the syntax and semantics of transfinite algorithms from a programming languages perspective?</strong></p>
<p>By &quot;transfinite algorithm&quot; I mean roughly any algorithm whose running time can be an infinite ordinal.</p>

CC BY-SA 4.0
2021-06-25T04:45:38.683Z
Hopefully I'll have a chance to write up a full answer, but are you at all familiar with lazy evaluation? What about co-induction or guarded recursion?
Joey Eremondi
CC BY-SA 4.0
2021-06-25T08:14:10.420Z
Lazy evaluation and co-induction yes, guarded recursion no. I see how these might give meaningful semantics when the closure ordinal ("running time") of a while loop is exactly $\omega$, but I do not see how to push it further. Whereas, in the traversal algorithm above, any ordinal may occur as the running time.
Siddharth
<pl.programming-languages><semantics>
syntax and semantics for transfinite algorithms
Siddharth
# syntax and semantics for transfinite algorithms

(Asked by: username_0 on 2021-06-22)

Let's say I wanted to *informally* describe a very simple algorithm for searching through an (undirected) finite connected graph $G = (V,E)$. I could define, for each natural number $n$, a set $S\_n$ and a list $L\_n$ as follows:

Initially, $S\_0$ is initialized to some vertex $v\_0$ and $L\_0 = ()$, the empty list.
Thereafter, if $S\_n \setminus L\_n$ is nonempty, pick $v\_n \in S\_n \setminus L\_n$. Let $L\_{n+1} = (L\_n , v\_n)$ and $S\_{n+1} = S\_n \cup \Gamma v\_n$, where $\Gamma v$ means the neighborhood of $v$.
(If $S\_n \setminus L\_n$ is empty, simply let $S\_{n+1} = S\_n$ and $L\_{n+1} = L\_n$.)

Once the recursion stabilizes, $S$ is equal to $V$ and $L$ is some traversal of the vertices of $G$.
Luckily, we don't need such cumbersome notation, because we could express this algorithm in a natural program syntax:

$S = \{v\_0\},\ L = () \\ \mathtt{while\ } S \setminus L \neq \emptyset, \\ \ \ \mathtt{pick}\ v \in S \setminus L \\ \ \ L = (L,v) \\ \ \ S = S \cup \Gamma v$

**Now** suppose that I wanted to extend this algorithm to **infinite** graphs. This is a straightforward: I define $S\_\alpha$ and $L\_\alpha$ for *ordinals* $\alpha$; the successor stages are exactly like above, and I take limits of $L$ and unions of $S$ at limit stages: i.e., for $\alpha$ limit,

$L\_\alpha = \lim\_{\beta < \alpha} L\_\beta$, $S\_\alpha = \bigcup\_{\beta < \alpha} S\_\beta$.

Once this recursion stabilizes, $S$ again equals $V$, and $L$ is a (well-ordered) traversal of the vertices of $G$.

However, I lack a clear **syntax** for expressing this algorithm. Really, the while loop above should work, given the right semantics. However, that semantics should account for while loops that can be iterated any ordinal number of times, whereas in any standard (e.g., operational) semantics, a while loop that does not terminate after a finite number of steps diverges. Therefore my question is

**Is there a formal semantics for the while loop above according to which it correctly computes infinite graph search?**

More generally,

**is there a community of researchers that studies the syntax and semantics of transfinite algorithms from a programming languages perspective?**

By "transfinite algorithm" I mean roughly any algorithm whose running time can be an infinite ordinal.

**Tags:** pl.programming-languages, semantics
> **Comments:**
> **username_1**: Hopefully I'll have a chance to write up a full answer, but are you at all familiar with lazy evaluation? What about co-induction or guarded recursion?  
> **username_0**: Lazy evaluation and co-induction yes, guarded recursion no. I see how these might give meaningful semantics when the closure ordinal ("running time") of a while loop is exactly $\omega$, but I do not see how to push it further. Whereas, in the traversal algorithm above, any ordinal may occur as the running time.  

---

## 0 answers

