5
$\begingroup$

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?

$\endgroup$
4
  • 1
    $\begingroup$ Note that Turing categories are topoi. Would it help if compilers had to be geometric morphisms? I don't know. $\endgroup$
    – Corbin
    Jun 5, 2021 at 4:51
  • 1
    $\begingroup$ 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) $\endgroup$ Jun 5, 2021 at 8:21
  • $\begingroup$ 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? $\endgroup$ Jun 6, 2021 at 9:26
  • $\begingroup$ 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. $\endgroup$
    – Corbin
    Jun 7, 2021 at 3:56

0

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.