3
$\begingroup$

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 finite 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 theorem 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}=\langle I_{B^{A}},O_{B^{A}},S_{B^{A}},\sigma_{B^{A}}, \omega_{B^{A}},q_{B^{A}}^{0}\rangle$ taking $$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}$ (for $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.

$\endgroup$
3
  • 1
    $\begingroup$ I've just discovered that this was cross-posted: math.stackexchange.com/questions/861766/… User 130569: please don't cross-post without saying so (preferably with a link). For example, Martin Brandenburg answered the question there with a suggestion similar to what I put down in my second paragraph. The moral of the story is that you thus create a situation where people duplicate efforts. $\endgroup$
    – Todd Trimble
    Jul 12, 2014 at 11:30
  • $\begingroup$ Sorry, I'm new here. Should I delete the other post? $\endgroup$
    – user130569
    Jul 14, 2014 at 6:56
  • 1
    $\begingroup$ No, please don't; just provide a link there to the thread here; thanks. $\endgroup$
    – Todd Trimble
    Jul 14, 2014 at 9:57

1 Answer 1

2
$\begingroup$

Something doesn't look quite right to me about the claim. Working in $\mathbf{Aut} = \mathbf{Aut}(\mathrm{Set})$, the initial object $\bot$ is the automaton with underlying sets $(I, S, O) = (\emptyset, \{q^0\}, \emptyset)$ with uniquely determined initial state, and empty functions for the transition or next-state function and output function. If $\mathbf{Aut}$ were cartesian closed, then we would have to have $Y \times \bot \cong \bot$ for any automaton $Y$ (since then $Y \times -$, being a left adjoint, would have to preserve the initial object). However, this seems patently false because products in $\mathbf{Aut}$ are computed componentwise (this is a consequence of the fact that the evident forgetful functor $\mathbf{Aut} \to \mathrm{Set}^3$ taking $Y$ to $(I_Y, S_Y, O_Y)$ is monadic: automata as described here are described by a multisorted algebraic [purely equational] theory). But $\{q^0\} \times S_Y \cong \{q^0\}$ is false if $S_Y$ has more than one element.

There may be variant notions of automata which do yield cartesian closed categories (as discussed for example here, where the category is a quasitopos). In case some wire was crossed and some such variant was meant, the following remarks might be useful for calculating exponentials, at least in cases where automata are described by multisorted algebraic theories as above. If we pretend for a moment that the category described above were cartesian closed, then one can systematically extract the structure of an exponential automaton $Z^Y$ in terms of the structures of automata $Y, Z$ by invoking, e.g.,

$$I_{Z^Y} \cong \mathrm{Set}^3((1, 0, 0), U(Z^Y)) \cong \mathbf{Aut}(F(1, 0, 0), Z^Y) \cong \mathbf{Aut}(F(1, 0, 0) \times Y, Z)$$

where $F \dashv U: \mathbf{Aut} \to \mathrm{Set}$ is the free-forgetful adjunction. Thus the set of inputs of $Z^Y$ would be naturally identified with the set of automaton maps $F(1, 0, 0) \times Y \to Z$; similarly the set of states of $Z^Y$ would be naturally identified with the set of automaton maps $F(0, 1, 0) \times Y \to Z$, and the set of outputs with the set of maps $F(0, 0, 1) \times Y \to Z$. This naturally invites one to work out the structure of various free automata $F(m, n, p)$, and write out very explicit descriptions of automaton maps of type $F(m, n, p) \times Y \to Z$. In brief, the entire structure of $Z^Y$ could be worked out very explicitly; roughly, one uses a canonical co-automaton structure on free objects in $\mathbf{Aut}$ where general transition maps and output maps are coded up by homming out of suitable automaton maps $F(0, 1, 0) \to F(1, 1, 0)$ and $F(0, 0, 1) \to F(1, 1, 0)$, respectively. I'll just leave these as hints, as this might make for a good exercise in categorical reasoning; the point is that one shouldn't have to guess at the structure of exponentials: assuming they exist, one can deduce their structure very explicitly by using these or similar techniques, and calculate to one's heart's content.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.