# Is the category of Turing categories an ∞-topos?

I'm an independent researcher working on programming languages. I would love to hear that this is all already known by simpler means, or that I'm wrong. I first opened this can of worms in the Before Times and have finally come around to finish it.

A Turing category is a category-theoretic way to talk about Turing-complete computation. A typical programming language has a collection of programs $$A$$ represented as (say) syntax trees, along with an composition function $$k : A \times A \to A$$ which runs programs in sequence. Its Turing category is the free category whose Turing object is $$A$$ and Kleene composition is $$k$$. (This might make more sense through a native-type-theoretic view.)

We can imagine a category of Turing categories, but we need structure-preserving maps. We might say that a functor $$F : \mathcal{C} \to \mathcal{D}$$ is a compiler when it sends Turing objects $$A_\mathcal{C} \mapsto A_\mathcal{D}$$, so that for any object $$X \in \mathcal{C}$$, let $$Y = F(X) \in \mathcal{D}$$, and the diagram:

$$\require{AMScd}$$ $$\begin{CD} A_\mathcal{C} @> F >> A_\mathcal{D} \\ @A s_{\mathcal{C},X} AA @V r_{\mathcal{D},Y} VV \\ X @> F >> Y \end{CD}$$

commutes up to equivalence. ($$s$$ freezes values as code and $$r$$ evaluates code to produce values.) This diagram captures the typical notion of compiler correctness: A program compiled from $$\mathcal{C}$$ to $$\mathcal{D}$$ should have equivalent behavior on all inputs. But notice that any functor which maps Turing objects to Turing objects must make this diagram commute up to equality! Proof: Take two copies of the diagram for the universal property (from nLab, linked above), one for $$\mathrm{id}_X \in \mathrm{Mor}(\mathcal{C})$$ and for $$\mathrm{id}_Y \in \mathrm{Mor}(\mathcal{D})$$; draw $$F$$ connecting them, and find the above square.

A few of us noticed that we can continue this pattern upwards to compiler compilers. A compiler compiler should have equivalent behavior on all compilers, but compilers are just ordinary Turing-complete programs, so we just repeat the above proof. Indeed, Turing categories seem to be objects in an ∞-category. Specifically, let Tomb be the ∞-category whose:

• Objects are Turing categories with a distinguished Turing object
• 1-arrows are Cartesian closed functors which send Turing objects to Turing objects
• 2-arrows are such functors restricted to 1-arrows

(We need to distinguish a Turing object per category because Turing categories are allowed to have more than one of them.) Tomb is so-called because composition of tombstone diagrams gives both the composition of 1-arrows and also both compositions of 2-arrows.

The practical rationale behind imagining Tomb is that we can think of its contents as long sequences of compilers for real-world programming languages, and we can imagine applying an n-arrow as changing the n'th language in the sequence without changing the behavior of the final program.

Turing objects are normally infinite. But curiously, the axioms allow for a Turing object which has just one element; the resulting Turing category has only one program. This gives us a terminal object in Tomb. We have products, but I'm not sure about sums, because of halting/partiality; we might have to pick products or sums. We can encode internal homs by noting that compilers can be found as programs in most Turing categories. So, I think that Tomb is Cartesian closed.

How much further can we go? Can we find Tomb to be an ∞-topos?

• Note that Turing categories are topoi. Would it help if compilers had to be geometric morphisms? I don't know. Jun 5, 2021 at 4:51
• The relationship between Turing categories (as in the nlab link) and programming languages/compilers/... is not clear to me. Can you say purely in category theoretic terms what a morphism between two Turing categories is? And what a 2-morphism between two parallel 1-morphisms is? (googling the words "turing category" and "compiler" mainly leads to an n-category cafe post by you, so this doesn't seem spelled out anywhere) Jun 5, 2021 at 8:21
• What is the displayed diagram supposed to mean? You have functors on the horizontal lines and morphisms on the vertical lines. Or to put it another way: in which category does the diagram take place? If you write down the diagram as an equation, what will it say? Jun 6, 2021 at 9:26
• The functor's computable, so we can find it inside any non-degenerate Turing category. I admit that this is central to the discussion but don't have good words for it. The diagram's meant to capture the equation that the compiler-as-functor is correct; anything computed in the origin category is computed similarly in the target category. Jun 7, 2021 at 3:56