Exponential objects in a category of abstract automata.

167 Views Asked by At

I'm working with a more or less standard definition of the category Aut(C) of automata over a category C (where C has finite products) which has tuples $$ A=\langle I_{A},O_{A},S_{A},\sigma_{A}, \omega_{A},q_{A}^{0}\rangle$$ as objects, where $I_{A}$,$O_{A}$ and $S_{A}$ are objects in C, and $\sigma_{A}:I_{A}\times S_{A}\longrightarrow S_{A}$ (the next state function), $\omega_{A}:I_{A}\times S_{A}\longrightarrow O_{A}$ (the output function) and $q_{A}^{0}:1\longrightarrow S_{A}$ (initial state) are morphisms in C. An automata homomorphism or simulation $f:A\longrightarrow B$ is a tuple $f=\langle f_{I},f_{S},f_{O}\rangle$ such that $f_{I}: I_{A}\longrightarrow I_{B}$, $f_{S}:S_{A}\longrightarrow S_{B}$ and $f_{O}:O_{A}\longrightarrow O_{A}$ are arrows in C and the following equalities are true: $$f_{S}\circ\sigma_{A}=\sigma_{B}\circ f_{I}\times f_{S}\tag{1}$$ $$f_{O}\circ\omega_{A}=\omega_{B}\circ f_{I}\times f_{S}\tag{2}$$ $$f_{S}\circ q_{A}^{0}=q_{B}^{0}\tag{3}$$ It's easy to proof that Aut(C) has finte products and it is a known fact that:

Theorem: If C is cartesian closed then Aut(C) is cartesian closed.

However, so far I haven't found any proof of this so I'm trying to do it myself but I'm stuck on the definition of exponential objects. It seems natural to define for any pair of automata $A,B\in$ Aut(C) the object $B^{A}$ with $$I_{B^{A}}=I_{B}^{I_{A}}$$ $$S_{B^{A}}=S_{B}^{S_{A}}$$ $$O_{B^{A}}=O_{B}^{O_{A}}$$ where objects on the right are exponentials in C, but $\sigma_{B^{A}}$ and $\omega_{B^{A}}$ are a little bit trickier because the evaluating map $\varepsilon: A\times B^{A}\longrightarrow B$ and curry $\lambda g: Z\longrightarrow B^{A}$, $g:A\times Z\longrightarrow B$, have to fulfill $(1)$,$(2)$ and $(3)$ in order to be morphisms in Aut(C).

Any ideas or references?

PD The theorem is supposed to be proven in the following papper but I can't find it anywhere:

Cazanescu, V. 1967. "On the Category of Abstract Sequential Automata" (paper in Romanian followed by summary in French and Russian), Ann. Univ. Bucharest, Math. and Mechanics Series, 16, No. 1, 31-37.

Thanks.

1

There are 1 best solutions below

1
On BEST ANSWER

Here is a way to come up with the exponential objects.

Assuming that $C$ is nice enough, the forgetful functors $I,O,S : \mathrm{Aut}(C) \to C$ should have left adjoints $I^*,O^*,S^*$. For example, for every object $X \in C$, then $I^*(X)$ will be the free automaton generated by an input object $X$. Explicitly, this is given by input object $X$, state object $1$, output object $X$, the canonical output morphism $X \times 1 \cong X$, the unique transition morphism $X \times 1 \to 1$ and the unique initial state $1 \to 1$.

Now if $A,B$ are automata with internal hom $\underline{\hom}(A,B)$ (assuming for the moment that it exists), then for every $X \in C$ we have $$\hom(X,I(\underline{\hom}(A,B)))=\hom(I^*(X),\underline{\hom}(A,B)) \cong \hom(I^*(X) \times A,B).$$ Now describe the set of morphisms of automata $I^*(X) \times A \to B$ explicitly. Using that $C$ is cartesian closed, find a specific object $P$ such that the morphisms correspond to morphisms $X \to P$. Then $P$ will be your $I(\underline{\hom}(A,B))$. Similarly one finds output and state objects of the internal hom. The transition and output morphisms can be found via naturality.

In the end, you have to verify if the constructed automaton $\underline{\hom}(A,B)$ really is an internal hom.