# syntax and semantics for transfinite algorithms

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.

• 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? Jun 25, 2021 at 4:45
• 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. Jun 25, 2021 at 8:14