Compositional language for hypotheses about computations

[Vanessa Kosoy]

TLDR: I sketch a language for describing (either Bayesian or infra-Bayesian) hypotheses about computations (i.e. computable^[1] logical/​analytic facts). This is achieved via a novel (AFAIK) branch of automata theory, which generalizes both ordinary and tree automata by recasting them in category-theoretic language. The resulting theory can be equipped with a intriguing self-referential feature: automata that “build” and run new automata in “runtime”.

Epistemic status: this is an “extended shortform” i.e. the explanations are terse, the math is a sketch (in particular the proofs are not spelled out) and there might be errors (but probably not fatal errors). I made it a top-level post because it seemed worth reporting and was too long for a shortform.

Motivation

Finite-state automata are a convenient tool for constructing hypotheses classes that admit efficient learning. A classical example is MDPs in reinforcement learning. Ordinary automata accept strings in input. This is convenient when the input is a time sequence. However, in Turing Reinforcement Learning and infra-Bayesian physicalism we want to equip our agent with beliefs about computations, which don’t form a time sequence in the ordinary sense.

Computations are often represented as trees: e.g. syntax trees of lambda calculus, or any other functional programming language, or expressions defining recursive functions. Hence, the obvious guess is using tree automata. Specifically, we will focus on bottom-up tree automata which are more powerful and more convenient for other reasons as well.

One limitation of this is that hypotheses described using (infra-)probabilistic tree automata are missing correlations between computations. Even if two programs contain a literally identical subroutine, or a single program uses multiple copies of an identical subroutine, the uncertainty is about the different copies is uncorrelated.

Another limitation is that sophisticated automata might require exponentially many states, meaning that a straightforward (tabular) description of the transition rules is exponentially large. Instead, we would like a convenient compositional language for constructing such automata (analogously^[2] to the compositional language I proposed for MDPs).

Therefore, a generalization is called for.

Deterministic Operadic Automata

Bottom-up deterministic tree automata are algebras over the operad of trees^[3] (modulo accepting states, which are not encoded in the algebra structure). More precisely, they are algebras over the free operad generated by the input alphabet of the tree automaton, where the arity of each symbol in the alphabet becomes the operadic arity of the corresponding generator. The transition rules of the tree automaton are the operations in the algebra.

So, we can now define a deterministic automaton over a (colored) operad $O$ to be an $O$-algebra. The automaton is “finite” when the colors are a finite set, and the algebra elements of each color are a finite set. An example application is: take the operad of lambda terms, quotient by $\eta$-reduction and $\alpha$-conversion, and add the renaming of free variables as additional operations into the operad. This leads to hypotheses-about-lambda-expressions which have a better inherent understanding of the semantics. On the other hand, the finiteness condition seems too restrictive now. But, maybe we can get away with, finite number of orbits under the action of the variable-renaming group. More generally, it is not clear which operads lead to a computationally-convenient notion of automaton (similarly how many problems are computationally/​statistically tractable for ordinary automata): this seems like a good problem to investigate.

Deterministic Operadic Transducers

The automata-theoretic notion of “transducer” also has a natural operadic analogue. However, in full generality, this analogue turns out to be much more powerful than classical transducers, even if the underlying operad is just the operad of the free monoid over some alphabet (i.e. in the case where operadic automata are just ordinary automata)^[4]: ordinary transducers can only add symbols to the end of the output as they process new input symbols, whereas operadic transducers can e.g. add symbols to the beginning, or write into two “working tapes” s.t. the output is their concatenation.

Given an operad $O$, we define the associated “state operad”^[5] $O^S$ as follows. Define “$O$-signature” to be a pair of (i) a list of $O$-colors (the input types) and (ii) an $O$-color (the output type).

• A color $A$ of $O^S$ is a set $S\left(A\right)$ (the “state space”), and for each $x\in S\left(A\right)$, a finite tuple $V\left(x\right)$ of $O$-signatures (the “variables” defined at the given state).

• An operation of $O^S$ is a mapping $f:{\prod }_{i}S\left(A_i\right)\to S\left(B\right)$ (where $A_i$ are the the input colors and $B$ is the output color) and, for each $x\in {\prod }_{i}S\left(A_i\right)$ and $\sigma \in V\left(f\right(x\left)\right)$, an operation of signature $\sigma$ in the operad freely generated by $O$ and generators corresponding to the components of $V\left(x_i\right)$ for all $i$.

Given operads $O_{1,2}$ and $A,B$ respective colors, a determinsitic operadic transducer from $A$ to $B$ can now be defined as an operad morphism $F$ from $O_1$ to $O_2^S$ s.t. for any $x\in S\left(F\right(A\left)\right)$, the tuple $V\left(x\right)$ starts with a $0$-ary signature whose output color is $B$. Given such $F$, we can transform any $0$-ary operation with output color $A$ to a $0$-ary operation with output color $B$ (exercise for the reader).

It is also possible to make transducers process morphisms of general signature. We leave out the details, since the notation in the operad setting is unwieldy. We do explain it for cartesian transducers below.

Deterministic Cartesian Automata/​Transducers

It is often convenient to represent programs as directed acyclic graphs (DAGs) rather than trees. Indeed, we want to be able to define a term once and use it multiple types later. Hence, it is natural to look for a flavor of automaton that can process DAGs. This is achieved by replacing operads with cartesian monoidal categories and algebras by strong monoidal functors from the category to $Set$. DAGs are thought of as morphisms in a free cartesian category, just like trees are operations in a free operad.

Given a cartesian category $C$, we can define the “state cartesian category” $C^S$ as follows. Here, a “$C$”-signature” is just a pair of objects (source and target).

• An object $A$ of $C^S$ is a set $S\left(A\right)$ (the “state space”), and for each $x\in S\left(A\right)$, a finite tuple $V\left(x\right)$ of $C$-signatures (the “variables” defined at the given state).

• A morphism from $A$ to $B$ in $C^S$ is a mapping $f:S\left(A\right)\to S\left(B\right)$ and, for each $x\in S\left(A\right)$ and $\sigma \in V\left(f\right(x\left)\right)$, a morphism of signature $\sigma$ in the cartesian category freely generated by $C$ and generators corresponding to the components of $V\left(x\right)$.

Given $A,B$ objects of $C^S$, we have $S(A\times B)=S\left(A\right)\times S\left(B\right)$ and $V(x,y)$ is the concatenation of $V\left(x\right)$ and $V\left(y\right)$.

A determinsitic cartesian transducer is now defined as consisting of:

• Input cartesian category $C$ and output cartesian category $D$

• Primary input $C$-signature ${\sigma }_0=A\to B$

• Auxiliary input $D$-signatures ${\sigma }_1\dots {\sigma }_n$

• Input state set $X$

• Output $D$-signatures ${\tau }_1\dots {\tau }_m$

• Output state set $Y$

• A cartesian functor $F$ from $C$ to $D^S$ s.t. (i) $S\left(F\right(A\left)\right)=X$ and for any $x\in X$, $V\left(x\right)$ is a prefix of ${\sigma }_1\dots {\sigma }_n$ (ii) $S\left(F\right(B\left)\right)=Y$ and for any $y\in Y$, ${\tau }_1\dots {\tau }_m$ is a prefix of $V\left(y\right)$

A transducer can accept an element of $X$ and morphisms of signatures ${\sigma }_0\dots {\sigma }_n$ and output an element of $Y$ and morphisms of signatures ${\tau }_1\dots {\tau }_m$.

Compositional language

We can now start defining our compositional language for constructing automata. This language describes^[6] automata/​transducers as string diagrams. There are two types of edges: edges labeled with sets, and edges labeled with a cartesian category $C$ and some $C$-signature. Vertices are labeled by transducers. Each vertex has incoming edges with labels corresponding to the transducer’s input state space and input signatures, and outgoing edges with labels corresponding to the transducer’s out state space and output signatures. The edges should be thought of as “wires” that conduct set elements or morphisms of prescribed signature respectively.

There is an interesting phenomenon here: string diagrams are in themselves morphisms of some cartesian category (with signature corresponding to labels of the diagram’s external edges)! This allows us to get self-referential, and add a special type of vertex in our diagram, which has one input which is a diagram of the same type (with prescribed external edge labels) and some number of other inputs, and whose semantics is applying the diagram to the inputs (where the outputs and other inputs have labels matching the diagram type).

I think that without further constraints, the resulting language might be Turing complete: at the very least, it is possible to create an infinite loop by coming up with an input $\alpha$ and a diagram $D$ s.t.$D$ contains a transducer $T$ which transforms $\alpha$ into $D$, and $D$ runs its input through $T$ and runs another copy of the input through the diagram $T$ outputs. [EDIT: Actually, this requires $T$ to produce a diagram $D$ which contains $T$. Unless we allow this explicitly, it shouldn’t be possible with “plain” cartesian automata. However, I think it is possible with closed cartesian automata (see below and comment).]

To avoid infinite loops, we can add a counter for the “level of meta” (i.e. the meta-vertex in diagrams of level $k$ can only accept diagrams of level lower than $k$). It is also possible to make this counter an ordinal, by representing ordinals in some notation that itself naturally takes the form of trees/​DAGs. Although to get a tractable language, we need to impose some strong constraints: even without the meta-vertex, we can get super-exponential blowup because each transducer can increase the size of the content of a variable by a constant factor for every input symbol. Possibly we should require our category to be equipped with some way to measure the “size” of morphisms (i.e. a functor to $N$, or maybe a lax functor to $N$ regarded as a 2-category using its order), and most transducers to e.g. only increase size by $O\left(1\right)$.

Monadic Cartesian Automata (MCA)

So far, everything was determinsitic. But, we want our hypotheses to have probabilistic and maybe also “infra-probabilistic” uncertainty. The obvious way to define probabilistic automata is to replace cartesian categories with Markov categories and replace $Set$ with e.g. $Stoch$ (the category of measurable spaces with Markov kernels as morphisms). However, this is poorly suited for our purpose, because (i) we a joint distribution over the outputs of all programs, and (ii) if an identical subroutine is defined multiple times, we want our uncertainty about those copies to be strongly correlated. Intuitively, want we want is allow all automata read from an additional “tape” filled with random bits. This can be naturally expressed using monads.

Fix a monad $M_0:Set\to Set$^[7] that is equipped with “lax cartesian structure”^[5:1]. By this we mean that it has lax monoidal structure ${\mu }^0$ w.r.t. the monoidal structure of $Set$ given by products, and this structure satisfies that for any sets $X,Y,Z$ and mappings $f:X\to Y$ and $g:X\to Z$, we have

$$M_0\left(\right(f\times g)\circ {\Delta }_X)={\mu }_{Y,Z}^0\circ \left(M_0\right(f)\times M_0(g\left)\right)\circ {\Delta }_{M_0\left(X\right)}$$

Here, $\Delta$ stands for the diagonal mapping.

Also, we require that ${\mu }_{X,Y}^0\circ ({\eta }_X\times {id}_{M_0\left(Y\right)})$ is a strength of $M_0$, where $\eta$ is the monad unit. However, we require neither that ${\mu }^0$ arises from this strength nor that it makes $M_0$ commutative (typically neither holds!) We call such a monad “memo monad”.

The prototypical example is when $M_0\left(X\right)$ is the set of binary trees whose leaves are labeled by elements of $X$^[8]. We think of such a tree as a way to select an element of $X$ by reading a stream of bits. Monad multiplication works by attaching the label-trees to the “parent” tree at the corresponding leaves. The monoidal structure works by taking the union of two trees, where each tree is regarded as the subset of $\{0,1{\}}^{\ast }$ corresponding to the bitstrings that describe the paths from the root to each vertex (imagine placing one tree such that it overlaps the other), and propagating the labels to the leaves in the obvious way.

Another example is binary trees whose non-leaf nodes are labeled by symbols from some fixed alphabet $\Sigma$. We think of each element of $\Sigma$ as corresponding to its own stream can be be queried indepedently. We won’t spell out the monoidal structure, but imagine running two subroutines one after the other while memoizing all the queries the first subroutine made from the benefit of the second. As opposed to the first example, this monoidal structure is not symmetric.

We also need $M_0$ to be equipped with a strong monad morphism to the monad $PFM$ defined as follows. For any set $X$,

$$PFM\left(X\right):=\underset{n=1}{\overset{\infty }{⨆}}(X^n\times D(\left[n\right]\left)\right)$$

Here, $\left[n\right]$ is the set $\{0,1\dots n-1\}$ and $D$ is the distribution monad.

We think of these as distributions over a list of outcomes of size $n$, with each outcome labeled by an element of $X$. Monad multiplication works by combining concatenation of strings with multiplication of probabilities in the natural way. Importantly, there are canonical monad morphisms from $PFM$ to both the free monoid monad $FM$ and the distribution monad $D$.

The morphism from $M_0$ to $PFM$ means that $M_0$ automatically acquires monad morphisms to $FM$ (we will denote it $m_{FM}$) and $D$ (we will denote it $m_D$). In the case of binary trees, this morphism is defined by listing the leaves of the tree in horizontal order and assigning probabilities by postulating a fair coin at each non-leaf vertex.

To define automata, we require that our cartesian categories are equipped with a memo monad. Given a cartesian category $C$ with memo monad $M$, a $(C,M)$-automaton is a strong monoidal functor $F:C\to Set$ together with a natural isomorhism between $M_0\circ F$ and $F\circ M$ which is (i) strong monoidal (ii) makes $F$ a morphism in the 2-category of monads on arbitrary categories (we call this a “memo functor”). Given $A,B$ objects in $C$ and $\alpha :A\to M\left(B\right)$ a morphism, $m_D\left(F\right(\alpha \left)\right)$ is a Markov kernel from $F\left(A\right)$ (the initial state of the automaton) to $F\left(B\right)$ (the final state of the automaton).

Notice that, given ${\alpha }_1:A_1\to B_1$ and ${\alpha }_2:A_2\to B_2$, $m_D\left(F\right({\alpha }_1\times {\alpha }_2\left)\right)$ has the marginals $m_D\left(F\right({\alpha }_1\times {\alpha }_i\left)\right)$, but the corresponding random variables are not independent. (Because of how $m_D$ interacts with the monoidal structure of $M_0$.) This means we get a non-trivial joint distribution over all morphisms, which is why we introduced monads in the first place.

This formalism has an infra-Bayesian analogue as well: it requires replacing $D$ by a the $\square$ monad (and we know it is a monad) and replacing $PFM$ by the corresponding infra-Bayesian monad. We won’t spell out the details.

Monadic cartesian transducers can be defined, but we won’t spell out the definition. The definition is spelled out for the case of closed cartesian transducers (see below), where the notation is a little simpler.

Processing DAGs with MCAs

As we discussed, programs are DAGs therefore DAGs are the starting point of any chain of transducers we might want to build. DAGs can be naturall regarded as morphisms in a free cartesian category. But how to embed them into a free cartesian category with memo monad? We do it as follows:

• Assume any “generator” vertex has one outgoing edge (and any number of incoming edge). Such a vertex corresponds to a generator morphism with signature ${\prod }_i{A}_i\to M\left(B\right)$, where the $A_i$ and $B$ are generator objects and $M$ is the memo monad.

• A generator morphism $\alpha :{\prod }_i{A}_i\to M\left(B\right)$ can be transformed to a morphism ${\alpha }^K:{\prod }_{i}M\left(A_i\right)\to M\left(B\right)$ as follows. To get ${\alpha }^K$, we compose (i) the monoidal structure for $M$ (to get from ${\prod }_{i}M\left(A_i\right)$ to $M\left({\prod }_i{A}_i\right)$ (ii) $M\left(\alpha \right)$ (to get from $M\left({\prod }_i{A}_i\right)$ to $M^2\left(B\right)$) (iii) the monad multiplication of $M$ (to get from $M^2\left(B\right)$ to $M\left(B\right)$).

• The morphisms of form ${\alpha }^K$ can be vertically and horizontally composed with each other in the usual way to evaluate the DAG. In particular, every edge corresponds to $M\left(A\right)$ for some generator object $A$.

• Any external incoming edge labeled by a generator objected $A$ is interpreted as the monad unit on $A$ in order to get from $A$ to $M\left(A\right)$.

It would be nice to formulate this process as evaluating a string diagram in the corresponding Kleisli category, but for a memo monad the Kleisli category is not even monoidal. Maybe there is some way to make it work, but atm I don’t know how.

(Monadic) Closed Cartesian Automata/​Transducers

It is convenient to require that our cartesian categories are closed, since it allows simplifying the definition of the “state category” 2-functor and improve its properties. We will also require the category to have arbitrary (not just finite) products. Indeed, let $C$ be such a category. Then we define the $C^S$ as follows:

• An object $A$ of $C^S$ is a set $S\left(A\right)$ (the “state space”), and for each $x\in S\left(A\right)$, an object $V_A\left(x\right)$ of $C$ (the “variables” defined at the given state).

• A morphism $\alpha :A\to B$ in $C^S$ is a mapping $S\left(\alpha \right):S\left(A\right)\to S\left(B\right)$ and, for each $x\in S\left(A\right)$, a morphism $V_{\alpha }\left(x\right):V_A\left(x\right)\to V_B\left(S\right(\alpha ,x\left)\right)$.

Given $A,B$ objects of $C^S$, we have $$S(A\times B)=S\left(A\right)\times S\left(B\right)$$ $$V_{A\times B}(x,y)=V_A\left(x\right)\times V_B\left(y\right)$$

Moreover, $$S\left(B^A\right)=S(B{)}^{S\left(A\right)}$$ $$V_{B^A}\left(f\right)=\prod _{x\in S\left(A\right)}{V}_B\left(f\right(x){)}^{V_A\left(x\right)}$$

So far, we could avoid the infinite products by requiring that $S\left(A\right)$ is finite. But, when $C$ is equipped with a memo monad $M$, we also want $C^S$ to have a memo monad $M^S$. This will require infinite sets. We define $M^S$ as follows:

$$S\left(M^S\right(A\left)\right):=M_0\left(S\right(A\left)\right)$$ $$V_{M^S\left(A\right)}\left(x\right):=\prod _{i\in \left[\left|m_{FM}\right(S\left(A\right)\left)\right|\right]}{V}_A\left(m_{FM}\right(S\left(A\right){)}_i)$$

$M^S$ is indeed a monad, but to define the memo (monoidal) structure on it, we need additional structure on $m_{PFM}$. Let $X$ and $Y$ be two sets and consider the following two mappings $f_{1,2}:M_0\left(X\right)\times M_0\left(Y\right)\to PFM\left(X\right)$:

$$f_1:=m_{PFM}\left(X\right)\circ {pr}_{M_0\left(X\right)}$$ $$f_2:=m_{PFM}\left(X\right)\circ M_0\left({pr}_X\right)\circ {\mu }_{X,Y}^0$$

In general, this diagram doesn’t commute, i.e. $f_1\ne f_2$. But, we require that it “lax commutes” in the following sense.

For any set $Z$, $PFM\left(Z\right)$ can be regarded as a category, in which a morphism from $(u,p)\in Z^n\times D\left[n\right]$ to $(v,q)\in Z^m\times D\left[m\right]$ is a mapping $\alpha :\left[n\right]\to \left[m\right]$ s.t. the following conditions hold:

• For any $i\in \left[n\right]$, $u_i=v_{\alpha \left(i\right)}$.

• ${\alpha }_{\ast }\left(p\right)=q$

This allows us to regard $f_1$ and $f_2$ as functors, and we postulate a natural transformation ${\varphi }_{X,Y}:f_1\to f_2$. We also postulate another natural transformation ${\varphi }_{X,Y}^{\prime }$ related in the same way to ${pr}_Y$ (it is separate since ${\mu }^0$ is not symmetric). Since $f_1$ and $f_2$ are actually natural transformations in terms of their dependence on $X,Y$, we require that $\varphi$ and ${\varphi }^{\prime }$ are 2-natural transformations. Possibly there are more conditions we need to satisfy but we won’t try to specify them precisely. In the case of trees/​queries, $\varphi ,{\varphi }^{\prime }$ are defined using the observation that, knowing the result of making more queries is sufficient to predict the result of making less queries.

We can now define the monoidal structure ${\mu }^S$ on $M^S$ given the monoidal structure $\mu$ on $M$. Consider some $A,B$ objects in $C^S$. We define

$$S\left({\mu }_{A,B}^S\right):={\mu }_{S\left(A\right),S\left(B\right)}^0$$ $$V_{{\mu }_{A,B}^S}(x,y{)}_i:={id}_{V_A(x{)}_{{\varphi }_{S\left(A\right),S\left(B\right)}\left(i\right)}}\times {id}_{V_B(x{)}_{{\varphi }_{S\left(A\right),S\left(B\right)}^{\prime }\left(i\right)}}$$

As before, a (monadic) closed cartesian automaton is a (memo) cartesian closed functor from $C$ to $Set$. A (monadic) closed cartesian transducer from $C$ to $D$ is a (memo) cartesian closed functor from $C$ to $D^S$. Given an object $A$ of $C$, a transducer $F$ can be regarded as taking morphisms $\alpha :1\to A$ as inputs producing $y$ and $\beta$ as outputs, where:

• $y:=S\left(F\right(\alpha \left)\right)$

• $\beta :=V_{F\left(\alpha \right)}$

Notice that these automata are in general not “finite” in any sense. To have a notion of “finite” automaton/​transducer, we need to have a fully faithfull cartesian closed subcategory $C_{fin}$ of $C$ representing “finite” objects, which (in some sense?) generates all of $C$ if arbitrary products are allowed. We can then define $C_{fin}^S$ to consist of $A$ s.t.$S\left(A\right)$ is a finite set and for every $x\in S\left(A\right)$, $V_A\left(x\right)$ is in $C_{fin}$. A finite automaton is a functor $F$ s.t.$F\left(A\right)$ is a finite set whenever $A$ is a finite object, and a finite transducer is a functor $F$ s.t.$F\left(A\right)$ is a finite object whenever $A$ is. We should probably also require that, if an infinite product ${\prod }_{\beta }{A}_{\beta }$ is a finite object, then all of $A_{\beta }$ are finite objects and all but a finite number of them are isomorphic to the terminal object $1$. Notice that the later condition is consistent with the way we defined $C_{fin}^S$.

Curiously, the state category 2-functor seems to be a “commutative”^[9] 2-monad. Indeed, the 2-monad multiplication corresponds to the functor $P:(C^S{)}^S\to C^S$ defined as follows. Given $A$ an object of $(C^S{)}^S$:

• $S\left(P\right(A\left)\right):={\bigsqcup }_{x\in S\left(A\right)}S\left(V_A\right(x\left)\right)$

• $V_{P\left(A\right)}(x,y):=V_{V_A\left(x\right)}\left(y\right)$

The 2-monoidal structure corresponds to the functor $\nu :C^S\times D^S\to (C\times D{)}^S$ defined as follows. Given $A$ and object of $C^S$ and $B$ an object of $D$:

• $S\left(\nu \right(A,B\left)\right):=S\left(A\right)\times S\left(B\right)$

• $V_{\nu (A,B)}(x,y):=V_A\left(x\right)\times V_B\left(y\right)$

This means that transducers are 1-morphisms in the corresponding Kleisli 2-category. In particular, composition of two transducers is a transducer. Moreover, an automaton is just a transducer from $C$ to the terminal closed cartesian category. And, transducer string diagrams are essentially just string diagrams in the Kleisli 2-category.

---

1. ↩︎

   We can use the same methods to talk about arbitrary describable facts, but I’m content with computable.

2. ↩︎

   The analogy is very rough, it is possible that there is some stronger compositional language that contains both as segments.

3. ↩︎

   This is obvious, but I haven’t seen it in the literature.

4. ↩︎

   I don’t know whether even this special case is already known under some other name in automata theory.

5. ↩︎↩︎

   I don’t know whether there is a standard name for this in category theory.

6. ↩︎

   In full generality, I’m not sure the composition of transducers yields transducers (however, it certainly does for closed cartesian automata, see below), so this language might define a broader class of “automata” rather than just describing them.

7. ↩︎

   Instead of $Set$, we can use a different cartesian category for the state spaces of our automata, e.g. compact Polish spaces. But, we will continue the explanation using $Set$, for the sake of simplicity.

8. ↩︎

   Equivalently, $M_0\left(X\right)$ is the free magma on $X$. In fact, algebras over $M_0$ are precisely magmas.

9. ↩︎

   Not sure what is the right term for 2-monads.