Difference between revisions of "Coalgebra"

From cLab
Jump to: navigation, search
m (Typo)
Line 60: Line 60:
 
The notation for h is not fixed though.
 
The notation for h is not fixed though.
 
In the context of programming or Type Theory, the notation <math>\operatorname{corec} c</math> is used,
 
In the context of programming or Type Theory, the notation <math>\operatorname{corec} c</math> is used,
whereas category theorists prefer shorter notation like <math>\overline{c}</math>.
+
whereas category theorists prefer shorter notations like <math>\overline{c}</math>.
 
The latter is the one we use throughout this article.
 
The latter is the one we use throughout this article.
  

Revision as of 21:24, 25 February 2015

Idea

Many systems can be described by having some kind of state space and a map that assigns to each state the result of observations that can be made on that state and possible next states that are reachable from that state. From an abstract perspective, the structure of the states are described by a category C and the possible observations are specified by an endofunctor [math]F[/math] on this category. A coalgebra is then a morphism [math]X \to FX[/math] for some carrier X, the state space.

Let us take a look at some examples before we dive into formal definitions and results.

  1. Deterministic Automata. The typical, first year example one learns about in Computer Science are deterministic automata over a finite alphabet [math]A[/math]. These are given by a set of states [math]Q[/math], a set of final states [math]F \subseteq Q[/math] and a map [math]\delta : Q \times A \to Q[/math] that assigns to a state [math]q \in Q[/math] and an input symbol the next state. We can combine this data into a single map [math]c : Q \to 2 \times Q^A[/math] by putting [math]c = \langle c_1, c_2 \rangle[/math] with [math]c_1(q) = \top \Leftrightarrow q \in F[/math] and [math]c_2(q)(a) = c(q, a)[/math].
  2. Non-deterministic automata. These are an extension of deterministic automata where we allow a state to have a set of successors, they are maps of the type [math]Q \to 2 \times \mathcal{P}(Q)^A[/math].
  3. Differential Equations. A more mathematical example are (ordinary) differential equations, these assign to each point in space a time dependent vector field, i.e., they are given on vector spaces by maps of the form [math]V \to T(V)^{\R}[/math] where [math]T(V)[/math] is the tangent space and [math]\R[/math] are the real numbers.

Note that in all these cases we have completely ignored initial states or initial conditions. These are not part of coalgebras, every element of the state space can be initial.

Definition

<definition id="coalg"> Let C be a category and [math]F : \mathbf{C} \to \mathbf{C}[/math] an endofunctor on C. An F-coalgebra is a morphism [math]c : X \to F X[/math] in C, and a homomorphism from a coalgebra [math]c : X \to F X[/math] to [math]d : Y \to F Y[/math] is a morphism [math]f : X \to Y[/math] such that

[math] \begin{array}{ccc} X & \xrightarrow{\displaystyle f} & Y \\ \big\downarrow c & & \big\downarrow d \\ F X & \xrightarrow{\displaystyle F f} & F Y \end{array} [/math]

commutes. </definition> Sometimes it is clearer to denote a coalgebra [math]c : X \to F X[/math] not just by c but instead by [math](X, c)[/math] to clearly indicate the carrier of c.

Straight from the definition, we can prove the following. <theorem id="coalg-cat">

 [math]F[/math]-Coalgebras and their homomorphisms form a category [math]\mathrm{Coalg}(F)[/math].

</theorem>

Final Coalgebras

One can think of a coalgebra as the operational semantics of a system. To get the denotational semantics of such a coalgebra, we need a semantic domain where we can interpret it. This is provided by a final (F-)coalgebra, if it exists. <definition id="final-coalg">

 A final object in the category [math]\mathrm{Coalg}(F)[/math] is called a final (F)-coalgebra.

</definition> Concretely, this means that there is a coalgebra [math]\xi : \Omega \to F \Omega[/math] such that for every coalgebra [math]c : X \to F X[/math] there is a unique homomorphism [math]h : X \to \Omega[/math]. This map is sometimes called the corecursion of h or, similarly to linear extensions, the coinductive extension of h. The notation for h is not fixed though. In the context of programming or Type Theory, the notation [math]\operatorname{corec} c[/math] is used, whereas category theorists prefer shorter notations like [math]\overline{c}[/math]. The latter is the one we use throughout this article.

A classical result for final coalgebras, due to Lambek, is that they are fixed point of a functor. <theorem id="lambek-coalg">

 If [math]\xi : \Omega \to F \Omega[/math] is a final coalgebra, then [math]\xi[/math] is an isomorphism.

</theorem> This justifies the notation [math]\nu F[/math], which is sometimes used to denote a (chosen) final coalgebra for F.

TODO:

  • Examples: Streams, p-adic integers
  • Non-examples: powerset functor
  • Construction via final chain

Behavioural Equivalence

Final coalgebras allow us to compare the behaviour of states. For example, let F be a functor on [math]\mathbf{Set}[/math] and [math]c : X \to F X[/math] a function. We say that two states [math]x_1, x_2 \in X[/math] are behaviourally equivalent, if [math]\overline{c}(x_1) = \overline{c}(x_2)[/math]. This can be generalised in case F does not admit a final coalgebra. <definition id="behavioural-equivalence">

 Let [math]c : X \to F X[/math] and [math]d : Y \to F Y[/math] be coalgebras. If there is a cospan [math](X, c) \rightarrow (Z, e) \leftarrow (Y, d)[/math] in [math]\mathrm{Coalg}(F)[/math], then we say that c and d are behaviourally equivalent.

</definition>

TODO:

  • Compare to bisimilary and other notions. See [1]

References

  1. Sam Staton, Relating Coalgebraic Notions of Bisimulation.