12
$\begingroup$

Given an endofunctor $F : Set \rightarrow Set$, we can define observation functions as functions that are polymorphic for any $F$-coalgebra, that is $obs$ is defined for any $F$-coalgebra $\langle A, c : A \rightarrow FA\rangle$. $$ obs : \forall \langle A, c \rangle . A \to B $$ Another way of looking at observation functions is as functions of the final $F$-coalgebra if it exists. We get the polymorphism automatically by composing the observation function with the unique homomorphism to the final $F$-coalgebra. But this only works if the final $F$-coalgebra exists.

One of the defining characteristics of an observation function is that it cancels any coalgebra homomorphism composed to the right, due to its polymorphism. If $hom$ is an $F$-coalgebra homomorphism, then: $$ obs = obs \circ hom $$ During my research, in an attempt to define a notion of observational consistency between one coalgebra and another, I had the idea of a weak coalgebra homomorphism. The idea is that we can "fake" a coalgebra homomorphism if we know the observation function ahead of time. Thus, we might satisfy, $$ obs = obs \circ hom $$ but only for one particular $obs$.

For example, let $FX = \{0,1\} \times X$, and let $obs$ be defined as $$ obs : \forall \langle A, c\rangle. A \to \{0,1\}^2 $$ $$ obs = \langle (\pi_1 \circ c), (\pi_1 \circ c \circ \pi_2 \circ c) \rangle $$ That is, $obs$ takes the first two elements of a stream.

Then, an F-coalgebra homomorphism would need to ensure that it preserves all the elements of the stream, whereas a weak homomorphism for $obs$ only needs to preserve the first two elements of the stream.

In my research, this notion would be useful in order to show that one coalgebra is observationally consistent with another by showing that every finite linear observation function has a weak homomorphism from the first coalgebra to the second coalgebra. In other words, every finite linear observation on the first coalgebra can be reproduced on the second coalgebra.

(What I mean by linear observation function feels mostly irrelevant, but for the sake of sharing... A linear observation function is more or less one that uses each state of the carrier set only once. I'm trying to model an oracle, and the user is not allowed to go back and pretend it never asked a question.)

My questions are thus:

  1. Has this been researched? Do "weak coalgebra homomorphisms" exist already, under some other name perhaps?

  2. Is there a more "category theory" way to present this?

Edit: Removed two questions which aren't that important.

$\endgroup$
11
  • 4
    $\begingroup$ Is there some reason to think that a computer science Q&A site is the right place for this question? $\endgroup$ – Sasho Nikolov Dec 10 '11 at 20:02
  • 5
    $\begingroup$ Yes. $F$-coalgebras have applications in computer science, and this question came up while doing research in computer science. Also, there are other questions about $F$-coalgebras on cstheory.stackexchange. $\endgroup$ – Francisco Mota Dec 10 '11 at 20:10
  • 1
    $\begingroup$ As an example of applications to computer science, notions of indistinguishibility (which are used in cryptography sometimes) might be definable in terms of weak homomorphisms. $\endgroup$ – Francisco Mota Dec 10 '11 at 20:31
  • 1
    $\begingroup$ I'd be curious to see a reference where this has been done and used to prove something. $\endgroup$ – Sasho Nikolov Dec 10 '11 at 20:46
  • 1
    $\begingroup$ This article: citeseer.ist.psu.edu/viewdoc/summary?doi=10.1.1.11.7571 Seems to have a very similar idea of "weak homomorphism" to mine above. But the definition is slightly different and I don't know if it actually coincides. It defines an observer $O$, which I don't understand yet, and it defines a weak homomorphism for $O$ between $\langle A, \alpha \rangle$ and $\langle B, \beta \rangle$ as a function $f: A \to B$ such that $$ \beta^O \circ f = O(f) \circ \alpha^O $$ But I don't yet know what the $O$ means. $\endgroup$ – Francisco Mota Dec 10 '11 at 23:54
6
$\begingroup$

The `weak morphisms' you describe do have a name in a slightly restricted setting. They can also be defined quite generally, as I'll explain.

In the case where $T : \mathsf{Set} \to \mathsf{Set}$ preserves weak pullbacks (many natural functors on $\mathsf{Set}$ do) it is known that behavioural equivalence coincides with coalgebraic bisimilarity. Then your morphisms are known as functional $\alpha$-step bisimulations where $\alpha$ is an ordinal. Admittedly I've only ever seen them defined for ordinals $\alpha \leq \omega$. Prior to coalgebra, modal logicians had studied n-step bisimulations for Kripke frames, which amount to n-step bisimulations for coalgebras for the powerset functor. Your requirement that they be functions as opposed to relations makes them functional n-step bisimulations.

On the other hand, you can define the concept you are talking about in a far more general setting without referring to coalgebraic bisimulations. For any category $\mathbb{C}$ which has limits of ordinal-indexed cochains and any functor $T : \mathbb{C} \to \mathbb{C}$ one can define $T$ 's terminal sequence. The condition regarding limits is actually rather weak e.g. many categories (including $\mathsf{Set}$) are actually complete i.e. have all small limits. The terminal sequence is a diagram in $\mathbb{C}$ and looks like:

$1 \quad \xleftarrow{!_{T1}} \quad T1 \quad \xleftarrow{T !_{T1}} \quad T^2 1 \quad \xleftarrow{T^2 !_{T1}} \quad \dots \quad T^\omega 1 \quad \xleftarrow{f_\omega^{\omega + 1}} \quad T(T^\omega 1) \quad \xleftarrow{Tf_\omega^{\omega + 1}} \quad \dots$

Here $1$ is the terminal object in $\mathbb{C}$ (limit of empty cochain). For example in $\mathsf{Set}$ this can be taken to be the one element set $1 = \{*\}$. The map $!_{T1} : T1 \to 1$ is the unique morphism into the terminal object e.g. in $\mathsf{Set}$ is simply maps every element of $T1$ to $*$. Each $T^n 1$ is computed by iterating $T$ and $T^\omega 1$ is the limit of the cochain preceding it. One can then continue beyond $\omega$, if necessary. Intuitively $T^\alpha 1$ is the collection of $\alpha$-step behaviours.

Now any $T$-coalgebra $(Z,\gamma)$ induces a cone over this sequence i.e. a collection of $\mathbb{C}$-morphisms $\mathsf{beh}_\gamma^\alpha : Z \to T^\alpha 1$ for each ordinal $\alpha$. I'll just define them for $\alpha < \omega$:

$\mathsf{beh}_\gamma^0 : Z \to 1$ is the unique map into the terminal object.

$\mathsf{beh}_\gamma^{n+1} = T\mathsf{beh}_\gamma^n \circ \gamma : Z \to T^{n+1} 1$

Intuitively these maps send a state in $Z$ to its $\alpha$-step behaviour. Now we can describe what you are talking about. Suppose we have two $T$-coalgebras $(A,\gamma)$ and $(B,\delta)$. Then a $\mathbb{C}$-morphism $f : A \to B$ preserves $\alpha$-step behaviour iff:

$\mathsf{beh}_\delta^\alpha \circ f = \mathsf{beh}_\gamma^\alpha$

That is, the $\alpha$-step behaviour of $f(z)$ in $\delta$ is precisely the $\alpha$-step behaviour of $z$ in $\gamma$.

Anyway, I hope this is helpful. You can find various references by googling 'terminal sequence coalgebra' or 'final sequence coalgebra'.

$\endgroup$
4
  • $\begingroup$ Thank you for this informative and accessible answer! I have one remark and one question. Remark: The idea of an "observation function" and "weak morphism" as in my post is a bit more general -- the weak morphism need not preserve all behavior up to the $\alpha$ level (and this is crucial for my application). This can easily be 'fixed' by having $\mathsf{obs}:T^\alpha 1 \to B$ and $\mathsf{obs} \circ \mathsf{beh}_\delta^\alpha \circ f = \mathsf{obs} \circ \mathsf{beh}_\gamma^\alpha$. Question: What is the difference between $\mathsf{beh}_\gamma^\omega$ and $\mathsf{beh}_\gamma^{\omega+1}$? $\endgroup$ – Francisco Mota Dec 16 '11 at 1:18
  • $\begingroup$ I'm not sure that I understand your remark. Do you mean that the depth of behaviour preserved varies e.g. $z$ and $f(z)$ are 2-step equivalent but $z'$ and $f(z')$ are 4-step equivalent? Note that $\alpha$-step equivalence implies $\beta$-step equivalence for all $\beta \leq \alpha$. $\endgroup$ – Rob Dec 16 '11 at 1:56
  • $\begingroup$ It is not so easy for me to explain the difference between $\mathsf{beh}_\gamma^\omega$ and $\mathsf{beh}_\gamma^{\omega+1}$ in so little space. Briefly, the behaviour of many functors is determined by its $\omega$-step behaviour e.g. for $2 \times Id : \mathsf{Set} \to \mathsf{Set}$ each infinite binary stream is determined by its depth n approximants. However there exist functors whose behaviours are not determined in this way e.g. countable powerset or full powerset functor. In these cases $\mathsf{beh}_\gamma^{\omega + 1}$ provides additional information. $\endgroup$ – Rob Dec 16 '11 at 2:07
  • $\begingroup$ No, you can keep $\alpha$ constant. The idea is that we don't want to show full bisimilarity, just part of it. For example, if my functor gave rise to a tree structure, such as $X \mapsto (2 \times X)^2$, I could choose only to look at one branch up to depth $\alpha$, rather than look at all nodes up to depth $\alpha$. Thank you for the answer. $\endgroup$ – Francisco Mota Dec 16 '11 at 9:43
5
$\begingroup$

As a rule, one should avoid heavily overloaded terminology like weak, regular, normal, etc. unless the notion has some universality. In particular, it appears your notion doesn't correspond with the usual notion of weak homomorphism after arrow flipping.

There are always more descriptive terms whenever your doing something less universal, like "observationally weakened homomorphism" shortened to "ow-homomorphism" perhaps.

Your notion of observation function already provides a category theoretic presentation. I'd worry more about clarifying what exactly it means, and why it's interesting, rather than seeking the most generality possible. In particular, you should usually give an informative example and non-example when introducing unusual notions in print.

$\endgroup$
1
  • $\begingroup$ Thank you for the answer. I agree with your recommendation to use a more specific name. I still intend to go read the papers on Weak Bisimulations by Jan Rothe (citeseer.ist.psu.edu/viewdoc/summary?doi=10.1.1.11.7571) to determine how they are related to my definition above, but I am (prematurely) convinced that they are different. Once again, thank you. $\endgroup$ – Francisco Mota Dec 12 '11 at 18:38

Your Answer

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

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