Sometimes you go on a relaxed walk along the Atlantic Ocean during your vacation and end up thinking about Lu Wilson’s (or Luke Wilson; either is fine I heard) take on spatial programming. And sometimes these thoughts get weird... Apologies for the sloppy writeup, but I don’t want to diverttoo much vacation time into solitarily writing about computer science.

I will write Spatial Programming (SP) for the classic 2d grid of cells, and I will write Recursive Spatial Programming (RSP) for the recursive version that Lu introduces. I will call the set of possible values a single cell can take on the alphabet, because I am old-fashioned.

What makes spatial programming “infinitely scalable”? The fact that everything is locally bounded. Cells are only affected by other cells at a fixed maximum distance (call that greatest possible distance k, and write k-SP for SP with a maximum distance of k when it comes to rule range). You know what else is purely local? First-order logic, as per Gaifman’s theorem. What a funny coincidence.

Jumping (seemingly) elsewhere: k-SP can be reduced down to 1-SP by encoding in each cell its k-neighbourhood. This requires an exponentially (in k) larger alphabet, but it is doable. So without loss of generality we can think about 1-SP only.

We can treat the two-dimensional checkerboard layout of SP as a planar graph, specifically as a grid. In 1-SP, we effectively get a labelled graph: the edge relation gives neighbouring squares, and cell states can be encoded as unary relations. And suddenly we are in a setting where Gaifman applies. (okay, it also applies in k-SP, but it is especially obvious for 1-SP)

Even more usefully, this also puts us in a setting where Courcelle’s theorem applies. Interesting!

Our underlying graph is a grid, and as such has unbounded tree-width. That’s probably a good thing for the expressivity of SP. But this raises immediate questions of doing SP on more restrictive topologies: on a path, on a tree, on graphs of bounded tree-width. Does Courcelle yield (more) efficient evaluation strategies in these settings? Can we trade expessivity for efficiency? If so, can we characterise the formal languages we can recognise on restrictive kinds of topologies?

Another interesting aspect here is the parallel nature of SP: given that Gaifman gives us locality in first-order logic on graphs, there should be some algorithmic meta theorems for parallelisation of model checking on graphs (of bounded tree-width?). Is there a Courcelle-like theorem regarding parallel model checking for MSO? And does the probabilistic evaluation strategy of SP factor into this in any form?

Some other random thoughts regarding SP:

• Can we consider SP as a generalisation of tree automata? (And if so, do we gain anything from that?)
• I can imagine several sensible definitions for busy-beavers in SP. I wonder which makes the most sense, and what the first few programs look like.
• With the locality properties of SP come issues of available space being bounded by the running time of a computation. I wonder what that means for computing Ackermann-like functions. More generally, are there (meta-) theorems regarding the space consumption of SP?

So much for SP, I also pondered RSP a bit. Fundamentally, the ability to recursively partition space means that we can store arbitrarily much information in a constant amount of total surface area. That feels weird somehow.

As an example, it is pretty easy to construct a stack data structure that only requires a constant amount of area: it is clearly possible to implement a stack with a maximum capacity of one item in bounded space. Now take that stack and split the cell that stored the item into two: one half stores the item, the other half recursively contains another of these stacks. Voilà, unbounded stack with bounded surface area.

This construction is elegant on the one hand, but it also feels a bit inefficient: it requires a depth of n in order to store n items. A “nicer” implementation should probably get this down to a depth in O(log(n)), analogous to how we represent numbers in binary rather than as tally marks. Hmm, I wonder whether there is a general technique that could be used to convert linear “depth-first” RSP data structures into more balanced ones. Probably not though =/

So, what is a good way of measuring space consumption? Surface area is clearly too inexpressive. Counting the total number of cells is accurate but loses information about how much each dimension is used. A better direction might be to interpret depth of nesting as a third dimension compared to the 2d nature of SP. Then volumes of three-dimensional bounding boxes could be useful? Or the minimum of the extent in any of the three dimensions? And for all of these it might be appropriate to consider the depth to be on a logarithmic scale (to double the amount of information that can be represented in some part of a RSP environment, you can either double the height, double the width, or merely increment the depth). And then there is also the matter of varying the alphabet size (compare this to how with pushdown automata you can trade alphabet size for stack depth and vice versa).

As a closing thought, note that Gaifman and Courcelle clearly do not apply to RSP; RSP does not correspond to MSO on graphs at all. But I do wonder what an extension to MSO would look like that would generalise RSP. While it would probably need to shift from a logic to a computational formalism, it would still be a lot more restrictive than a formalism that allows for arbitrary graph construction. RSP still has some form of locality properties, and these might allow for interesting (and useful) theorems about a corresponding but more general graph-based computational model. And who knows, it might even admit Courcelle-like meta theorems.

I have to stop writing now, but I do hope that some day some model-checking folks (or logicians) will take a serious look at (recursive) spatial programming. This feels like an underexplored area to me that could be fun, fruitful, and useful.

~Aljoscha