Toby Wilkinson
email: stw08r@ecs.soton.ac.uk

Internal Models for Coalgebraic Modal Logics

Keywords: Coalgebra, Modal Logic, Dual Adjunction, Expressivity

We present ongoing work into the systematic study of the use of dual adjunctions in coalgebraic modal logic. We introduce a category of internal models for a modal logic. These are constructed from syntax, and yield a generalised notion of canonical model. Further, expressivity of a modal logic is shown to be characterised by factorisation of its models via internal models and the existence of cospans of internal models.

Introduction

The now standard approach to coalgebraic modal logic is through a so called logical connection -a dual adjunction between two base categories X and A. The category X represents state spaces, or sets of processes, and the category A base logics, typically presented as algebras. The standard example is that of the categories Set and BA, where the latter is taken to represent classical propositional logics.

To these are added transition structures and modal operators. The modal operators, added to the base logics, aim to capture the dynamics of the transition structures. In choosing the modalities there is often a conflict between fully capturing the dynamics, and choosing modalities with an intuitive meaning, as logics with modalities that are hard to understand are unlikely to be adopted.

The transition structures are defined as coalgebras for an endofunctor T on X, and the modal logics as algebras for an endofunctor L on A. The semantics are then given by means of a natural transformation. Clearly this is a very general framework. Our work aims to explore the rich structure of this framework through the use of categorical techniques.

The first step is to make precise when a T -coalgebra is a model for an Lalgebra, and this requires the notion of a valuation of an L-algebra in a Tcoalgebra. A model then becomes a coalgebra, valuation pair. The models for an L-algebra form a category, and the structure of this category determines many of the properties of the modal logic that the L-algebra represents.

The main contribution of this paper is the observation that for each Lalgebra, there is a full subcategory of its category of models that in many cases determines the logical properties of that L-algebra. These models we call the internal models, and as will be seen, they generalise the concept of canonical models found in Kripke semantics [START_REF] Blackburn | Modal Logic[END_REF]. Like canonical models, they can be thought of as being constructed from the syntax of the modal logic.

The most important property that an L-algebra can have, is that every model factors via an internal model. If an L-algebra has this property, then the information content of the category of models is contained entirely within the subcategory of internal models, and the other models need not be considered. This turns out to be very useful, since if X is wellpowered and certain morphisms are monomorphisms, then because the category of internal models is thin, its objects can be partitioned into a collection of equivalence classes that is a set (actually a poset). Moreover, under similar conditions, and if X has an appropriate factorisation system, the forgetful functor from the category of internal models to X detects colimits. So if X is cocomplete, wellpowered, and has an appropriate factorisation system, then the category of internal models is cocomplete, and a final internal model exists as the coproduct of a representative from each of the equivalence classes of internal models. This forms the basis of an adjoint functor theorem between the categories Alg(L) and CoAlg(T ).

The factorisation of models via internal models is shown to follow from the existence of a factorisation system (E, M ) in X, and a condition that essentially amounts to T preserving M , and a particular natural transformation being componentwise in M . This is a restatement of [START_REF] Klin | Coalgebraic modal logic beyond sets[END_REF]Theorem 4.2] and [START_REF] Jacobs | Exemplaric Expressivity of Modal Logics[END_REF]Theorem 4].

In [START_REF] Klin | Coalgebraic modal logic beyond sets[END_REF][START_REF] Jacobs | Exemplaric Expressivity of Modal Logics[END_REF] this result is used to prove expressivity results for coalgebraic modal logics. We go beyond this, and show that under certain mild assumptions on the category X and if T preserves M , then an L-algebra is expressive for its category of models, if and only if, every model factors via an internal model, and for every pair of internal models there exists a cospan. This result is a purely categorical characterisation of expressivity, and provides strong support to the school of thought that the correct way to formulate expressivity is via cospans, and not by bisimulation relations represented as spans. This is particularly important for labelled Markov processes, for which in [START_REF] Danos | Bisimulation and cocongruence for probabilistic systems[END_REF], the authors point out that the failure of T to preserve weak pullbacks, which is the case for the Giry monad on measurable spaces, poses a severe difficulty to the construction of such a bisimulation. In [START_REF] Jacobs | Exemplaric Expressivity of Modal Logics[END_REF] the expressivity result of [START_REF] Danos | Bisimulation and cocongruence for probabilistic systems[END_REF] is recast in our dual adjunction framework, and we examine it in Example 24 (3) and Example 36 [START_REF] Danos | Bisimulation and cocongruence for probabilistic systems[END_REF].

A general outline of this paper is as follows. In section 2 we recall the category theoretic notion of a factorisation system. Then in section 3 we explain the dual adjunction framework in which we work. In section [START_REF] Doberkat | Stochastic Coalgebraic Logic[END_REF] we define what we mean by a model for a modal logic, and introduce the concept of an internal model. Then in section 5 we show when colimits of models and internal models exist. The proofs of these results are relatively straightforward, but long and tedious, so we restrict our presentation to an outline of the proofs. In section 6 an adjoint functor theorem is proved as a simple example of the utility of internal models. Then in section 7 internal models are used to characterise expressivity.

Preliminaries

In what follows we will need to be able to factorise morphisms. The standard approach to this is via a factorisation system [START_REF] Adámek | Abstract and Concrete Categories[END_REF].

Definition 1. In a category C, a pair (E, M ) of classes of morphisms is called a factorisation system for C, if the following hold:

1. If e ∈ E, and h an isomorphism in C, 1. In the category Set the obvious factorisation system (E, M ), is to take E to be all the epimorphisms (surjective functions), and M all the monomorphisms (injective functions). 2. In the category Top of topological spaces, (Epi, Mono) is not a factorisation system, however (RegEpi, Mono) and (Epi, RegMono) are. Here, RegEpi is the class of regular epimorphisms (quotients), and RegMono is the class of regular monomorphisms (embeddings).

then if h • e exists, h • e ∈ E. 2. If m ∈ M , and h an isomorphism in C, then if m • h exists, m • h ∈ M .
We shall also make use of the following proposition which is a statement of parts of [START_REF] Adámek | Abstract and Concrete Categories[END_REF]Propositions 14.6,14.9]. Proposition 4. Let C be a category with a factorisation system (E, M ).

1. Each of E and M is closed under composition. 2. If f • g ∈ M and f ∈ M , then g ∈ M . 3. If f • g ∈ E and g ∈ E, then f ∈ E.
A class of monomorphisms defines a notion of subobject in a category, and it is often important that for every object in a category its collection of subobjects is a set. The following definitions are standard [START_REF] Adámek | Abstract and Concrete Categories[END_REF].

Definition 5. Given a class M of monomorphisms in a category C we define the following:

1. An M -subobject of an object A in C is a pair (S, m), where m : S → A is in M . 2. Two M -subobjects (S, m) and (S , m ) of A are isomorphic if there exists an isomorphism h :

S → S such that m = m • h. 3. C is M -wellpowered if no object in C has a proper class of pairwise non- isomorphic M -subobjects.
Here by pairwise non-isomorphic we mean that any pair of distinct subobjects are non-isomorphic.

Dually, for a class E of epimorphisms we can define an E-quotient object of an object A as a pair (e, Q), where e :

A → Q is in E. The obvious dual notion to C being M -wellpowered is that C is E-cowellpowered.
Definition 6. A category C is thin if each homset has at most one element.

Proposition 7. Given a class M of monomorphisms in a category C, the Msubobjects of an object A form a thin category Sub M (A), the objects of which can be partitioned by isomorphisms into a collection of equivalence classes that carries a partial order, and if C is M -wellpowered this collection is a set.

Dual-Adjunction Framework

Increasingly, the standard approach to coalgebraic modal logic is to formulate it in a dual-adjunction framework [START_REF] Kupke | Stone coalgebras[END_REF][START_REF] Klin | Coalgebraic modal logic beyond sets[END_REF][START_REF] Jacobs | Exemplaric Expressivity of Modal Logics[END_REF].

A S & & L % % X P f f T y y
Briefly this consists of two categories A and X, and two contravariant functors P and S that form a dual adjunction i.e. there exists a natural isomorphism

Φ : A(-1 , P (-2 )) ⇒ X(-2 , S(-1 ))
Such a dual-adjunction is often referred to as a logical connection [START_REF] Pavlovic | Testing Semantics: Connecting Processes and Process Logic[END_REF], and we denote the unit and counit by

ρ : id A ⇒ P S σ : id X ⇒ SP
The category X represents a collection of state spaces, and a collection of generalised transition systems is defined on these state spaces as coalgebras for an endofunctor T . Similarly, the category A represents a collection of base logics to which modal operators are to be added. These are introduced via an endofunctor L, and the corresponding modal logics are the L-algebras. The semantics of these modal logics is given in two stages. First the dual adjunction gives a semantics for the base logics in terms of the state spaces, and then secondly, a natural transformation δ : LP ⇒ P T

gives

Models and Internal Models

The Kripke semantics for modal logic [START_REF] Blackburn | Modal Logic[END_REF] introduces the concepts of frame, valuation, and model, where a model is a pair consisting of a frame and a valuation. There are obvious generalisations of these notions to coalgebraic modal logic.

Definition 9. Given an L-algebra (A, α) and a T -coalgebra (X, γ), if there exists a morphism f (not necessarily unique) such that the diagram below commutes, then (X, γ) is called a frame for (A, α), and f is called a valuation of (A, α) in (X, γ), and the pair is called a model for (A, α).

L(A)

L(f ) / / α LP (X) δ X P T (X) P (γ) A f / / P (X)
Clearly, if (A, α) is the initial L-algebra then every T -coalgebra is a frame, but in general this is not the case.

Remark 10. If we were following the conventions of Kripke semantics for modal logic [START_REF] Blackburn | Modal Logic[END_REF] we would call every T -coalgebra a frame irrespective of the choice of Lalgebra. We do not do this as we already have a name for such entities -they are T -coalgebras. Therefore we reserve the name frame for only those T -coalgebras for which valuations exists, and this necessarily makes the concept of a frame one that is relative to a choice of L-algebra. Now, as observed in [START_REF] Pavlovic | Testing Semantics: Connecting Processes and Process Logic[END_REF], the logical connection allows every model diagram in A to be redrawn in X as

X f / / γ S(A) S(α) SL(A) T (X) T (f ) / / T S(A) δ * A O O
where f is the adjunct of f , and δ * : T S ⇒ SL is defined following [START_REF] Klin | Coalgebraic modal logic beyond sets[END_REF] as

δ * = SLρ • δ S
where ρ is the unit of the logical connection. Such an f we will call a theory map.

Definition 11 (Models). For an L-algebra (A, α) we define Mod(A, α), the category of models for (A, α), with objects given by pairs

((X, γ), f : X → S(A))
where (X, γ) is a T -coalgebra, and f is a theory map (as above), and morphisms

g : ((X 1 , γ 1 ), f 1 ) → ((X 2 , γ 2 ), f 2 )
given by a T -coalgebra morphism g :

(X 1 , γ 1 ) → (X 2 , γ 2 ) such that f 1 = f 2 • g.
In the above definition, the requirement on model morphisms that f 1 = f 2 •g arises from the fact that theory maps need not be unique. In simple terms, we have to ensure that any propositional variables are given interpretations in the two models that are compatible with the T -coalgebra morphism.

In [START_REF] Doberkat | Stochastic Coalgebraic Logic[END_REF] a similar definition of a category of models for an L-algebra is made, however this is done in terms of diagrams in A i.e. pairs of T -coalgebras and valuations. In what follows next we prefer to work in X, but as already noted above, and first observed in [START_REF] Pavlovic | Testing Semantics: Connecting Processes and Process Logic[END_REF], the logical connection allows us to move freely backwards and forwards between the two definitions. We can make this precise with the following proposition.

Proposition 12. The natural transformation δ : LP ⇒ P T defines a functor P : CoAlg(T ) → Alg(L) given by

P (X, γ) = (P (X), P (γ) • δ X ) P (f ) = P (f ) : P (Z, ξ) → P (X, γ)
where f : (X, γ) → (Z, ξ), and for each L-algebra (A, α), Mod(A, α) is dually isomorphic to the comma category ((A, α) ↓ P ).

We are now ready to introduce our key idea. Recall from Kripke semantics the notion of a canonical model [START_REF] Blackburn | Modal Logic[END_REF]. This is a model of a modal logic constructed from the syntax itself. The idea is that when trying to prove completeness, by the way the canonical model is constructed from the syntax, for every formula that is not derivable, one can find a state that witnesses that the formula is not valid.

In such a canonical model the possible worlds are the theories of the logic. In our setup, S(A) is the collection of all possible theories of (A, α), so an obvious question is when can we construct a model from S(A) i.e. when can we put a T -coalgebra structure on S(A) such that it becomes a model for (A, α)?

In general this cannot be done, but in [START_REF] Schröder | Strong completeness of coalgebraic modal logics[END_REF] conditions are given in the case of the standard logical connection between BA and Set (Example 8 (1)) for the existence of a, not necessarily unique, model for the initial L-algebra with carrier set S(A). From this they derive a strong completeness result.

To illustrate our approach consider a toy example, where the logical connection consists of functors P and S given by the contravariant powerset functor on Set, the functors L and T both map every object to the two element set 2, and δ X (i) = {i} for i ∈ 2. Then the initial L-algebra is (2, id 2 ), and a final T -coalgebra is given by ({{0}, {1}}, γ), where γ({i}) = i. Here it should be observed that the carrier set of the final coalgebra is clearly a proper subset of S(2), so our approach is to consider not just models constructed from the whole of S(A), but to consider models built from subobjects of S(A). In other words, models where the theory map is a monomorphism.

Definition 13 (Internal Models). Given a class M of monomorphisms in X, we define the category IntMod M (A, α) to be the full subcategory of Mod(A, α) where the theory maps are in M , and write

G : IntMod M (A, α) → Mod(A, α)
for the corresponding inclusion functor.

We parameterise by the class M , as sometimes we require the morphisms of M to have additional properties, for example, that the members of M are preserved by T . In Example 24 (3) the Giry functor does not preserve all monomorphisms, but does preserve a particular subclass of them.

Proposition 14. The category IntMod

M (A, α) is thin, and if for all m ∈ M δ * A • T (m) is a monomorphism, then the forgetful functor from IntMod M (A, α) to Sub M (S(A)) is full.
Proof. Since the theory maps of internal models are monomorphisms the category IntMod M (A, α) is thin. For the second part, consider a pair of internal models I 1 and I 2 , and a morphism g in Sub M (S(A)) between the theory maps of I 1 and I 2 . We have to show that g is an internal model morphism, but this can be seen to easily follow if δ * A • T (m 2 ) is a monomorphism, where m 2 is the theory map of I 2 .

At this point we should provide some intuition for the condition on δ * A •T (m). Indeed, in the rest of the paper we shall frequently see the slightly strengthened

condition m ∈ M ⇒ δ * A • T (m) ∈ M .
The reason for this particular formulation of the condition is a technical one relating to use of the unique diagonalisation property of a factorisation system, but we can motivate this choice as follows.

If we consider the logical connection of Example 8 (1) between BA and Set, and consider the finite powerset functor on Set, then as we shall see in Example 24 (1), we can choose L to add a finite meet preserving operator to each Boolean algebra. Then given an L-algebra (A, α), say the Lindenbaum-Tarski algebra of the logic S4 (for some set of propositional variables), every state of an internal model for (A, α) has a distinct theory consisting of the set of formulae that are satisfied in that state. Informally,1 the function S(α) can then be thought of as taking each such theory s, and generating the set of formulae a, such that a ∈ s. Since this set is an element in SL(A) it is also an ultrafilter. The function δ * A • T (m) therefore sends the set U of successors of a state x, to the set of formulae satisfied by all x ∈ U , and these are precisely those in the theory of x that are prefixed with the operator. In this example, the condition that m ∈ M ⇒ δ * A • T (m) ∈ M means that in models where each state has a distinct theory, that for each finite set of possible successors, the set of formulae that are satisfied by all members of that set is also distinct.

The utility of internal models arises from the observation that in many cases it is possible to take a model and "quotient by behavioural equivalence" i.e. produce a smaller model by identifying states that are behaviourally equivalent. Such a quotiented model will be an internal model, and we say the model factors via the internal model.

The above is not very precise as we have not said what we mean by quotient and behavioural equivalence. This will become clear in Section 7, but first we make the following definition. If the category X has a proper factorisation system (E, M ), factoring a model via an internal model, can be viewed as putting a T -coalgebra structure map on an E-quotient object of the state space of the model. As we will see in Section 7, this corresponds to quotienting with respect to behavioural equivalence.

We can also note that the construction of models is functorial. To see this, observe that since δ * is a natural transformation, and (g • f ) = S(f ) • g , that we have the following proposition.

Proposition 17. For every L-algebra morphism f : (A, α) → (A , α ) there exists a functor

Mod(f ) : Mod(A , α ) → Mod(A, α) ((X, γ), g ) → ((X, γ), (g • f ) ) h → h where h : ((X, γ), g ) → ((X , γ ), g ).
Can we construct a similar functor between the categories IntMod M (A , α ) and IntMod M (A, α) for such an L-algebra morphism? The answer is yes whenever all models in Mod(A, α) factor via an internal model in IntMod M (A, α).

Theorem 18. If the category X has a factorisation system (E, M ) and

m ∈ M ⇒ δ * A • T (m) ∈ M
then for all L-algebra morphisms f : (A, α) → (A , α ) there exists a functor Then by the diagonalisation property of the factorisation system, there is a unique µ such that the above diagram commutes, and it is not hard to see that

IntMod M (f ) : IntMod M (A , α ) → IntMod M (A, α) ((X, γ), g ) → ((I, ζ), m) h → µ where h : ((X, γ), g ) → ((X , γ ), g ), (g • f ) = m • e, (g • f ) = m • e ,
δ * A • T (m ) ∈ M means that µ is a morphism in IntMod M (A, α).
5 Colimits in Mod(A, α) and IntMod M (A, α)

As we shall see in future sections, one of the most important aspects of the structure of the categories Mod(A, α) and IntMod M (A, α) is the presence, or otherwise, of colimits. In this section we shall see that in the case of the category Mod(A, α), the forgetful functor from Mod(A, α) to X creates small colimits, but that for the category IntMod M (A, α), the corresponding forgetful functor does not. However, under certain additional conditions it does detect small colimits, but does not necessarily preserve them.

We define the following forgetful functors

U : CoAlg(T ) → X V : Mod(A, α) → X V * : Mod(A, α) → CoAlg(T ) W : IntMod M (A, α) → X where V = U V * and W = V G.
To start we state without proof the well known result (see for example [START_REF] Rutten | Universal coalgebra: a theory of systems[END_REF] for the case in Set) that the forgetful functor U : CoAlg(T ) → X creates small colimits.

Theorem 19. The forgetful functor U : CoAlg(T ) → X creates small colimits.

The case for the forgetful functor V : Mod(A, α) → X follows in a similar fashion, with the additional detail that a theory map must be constructed for the colimit.

Theorem 20. The forgetful functor V : Mod(A, α) → X creates small colimits.

Proof. Consider a small category J and a functor D : J → Mod(A, α), and suppose that X has colimits of shape J. Then we have that V D has a colimit (C, φ j : V D(j) → C) j∈J . We now proceed as follows (sketch):

1. Use the functor V * and Theorem 19 to construct a colimiting T -coalgebra (C, χ). 2. Use the theory maps and the universal property of C to construct a morphism g from C to S(A). 3. Use the universal property of C to show that there is a unique morphism from C to SL(A) and that this makes g into a theory map, ((C, χ), g) a model, and the φ j model morphisms. 4. For another cocone of D use the functor V * and the universal property of (C, χ) to construct a unique mediating morphism to the underlying Tcoalgebra. 5. Use the uniqueness of g to show that the mediating morphism is a model morphism, and thus ((C, χ), g) is the colimit of D.

It is clear that (((C, χ), g), φ j : D(j) → ((C, χ), g)) j∈J is the unique cocone for D that is mapped by V to the colimit (C, φ) of V D. Thus we can conclude that V creates colimits of shape J.

For the category IntMod M (A, α) the details are more complicated. The approach we take is that the colimit is constructed in Mod(A, α), and then the resulting colimiting model is factored via an internal model using Proposition 16.

Theorem 21. Given an L-algebra (A, α), if the following hold:

1. the category X has a factorisation system (E, M ), 2. m ∈ M ⇒ δ * A • T (m) ∈ M , then the forgetful functor W : IntMod M (A, α) → X detects small colimits.

Proof. Consider a small category J and a functor D : J → IntMod M (A, α), and suppose that X has colimits of shape J. Then by Theorem 20, the functor GD has the colimit (((C, χ), g), τ j : GD(j) → ((C, χ), g)) j∈J in Mod(A, α). We now proceed as follows (sketch):

1. Use Proposition 16 to factor ((C, χ), g) via an internal model ((I, ζ), m) by e : ((C, χ), g) → ((I, ζ), m). 2. For another cocone (((Z, ξ), h), ψ j : D(j) → ((Z, ξ), h)) j∈J of D there is a unique mediating morphism µ : ((C, χ), g) → ((Z, ξ), h) in Mod(A, α).

The uniqueness of g means

g = h • V (µ),

An Adjoint Functor Theorem

As a simple example to show the utility of the categories IntMod M (A, α) we prove an adjoint functor theorem.

To find a functor S : Alg(L) → CoAlg(T ) that together with P forms a dual adjunction between Alg(L) and CoAlg(T ) we must show that for every L-algebra there is a universal morphism to P . But this is the same as requiring that each comma category ((A, α) ↓ P ) has an initial object.

Theorem 22. If for all L-algebras (A, α) the following hold:

1. every model in Mod(A, α) factors via some model in IntMod M (A, α), 2. IntMod M (A, α) has a final object, then there exists a dual adjunction between Alg(L) and CoAlg(T ).

Proof. We are required to show that for any L-algebra (A, α) that ((A, α) ↓ P ) has an initial object. But by Proposition 12 this is the same as requiring that each Mod(A, α) has a final object.

Consider such a Mod(A, α). By the two premises above, every model in Mod(A, α) factors via the final object in IntMod M (A, α), and since the theory map of the final internal model is a monomorphism, the morphism from a model in Mod(A, α) to the final internal model is unique. Thus the final object in IntMod M (A, α) is the final object in Mod(A, α).

In the above proof, no explicit use was made of the class M , only that IntMod M (A, α) is a special subcategory of Mod(A, α) -it has a final object, and for all objects in Mod(A, α) there exists a unique morphism to an object in IntMod M (A, α). Therefore for each L-algebra a different class M of monomorphisms could in principle be chosen, but typically the same class would be used for all L-algebras. Indeed, the choice of M is likely to be driven by the properties of the base category X and the functor T , as in the following corollary.

Corollary 23. If the following hold:

1. X has a factorisation system (E, M ), is M -wellpowered, and has small coproducts, 2. for all L-algebras (A, α) we have m ∈ M ⇒ δ * A • T (m) ∈ M , then there is a dual adjunction between Alg(L) and CoAlg(T ).

Proof. By Proposition 16, for every L-algebra, every model in Mod(A, α) factors via an internal model in IntMod M (A, α). Now since X is M -wellpowered, by Proposition 7, the objects of Sub M (A) can be partitioned into a set of equivalence classes. Also by Proposition 14, the forgetful functor from IntMod M (A, α) to Sub M (A) is full and IntMod M (A, α) is thin. Therefore the objects of IntMod M (A, α) can also be partitioned into a set of equivalence classes, and since X has small coproducts, by Theorem 21, the coproduct of a representative from each equivalence class exists. Further, since IntMod M (A, α) is thin, and between each pair of representatives of an equivalence class there exists an isomorphism, the injections into the coproduct yield a unique morphism from each object of IntMod M (A, α) to the coproduct. Thus the coproduct is the final object in IntMod M (A, α).

Finally by Theorem 22 we have the result.

In most cases, for a particular choice of X, the existence of a factorisation system, wellpoweredness, and the existence of small coproducts, is well known. Further, it is often straightforward to show that T preserves M , thus by Proposition 4, what is left to show is that δ * is componentwise in M , and this is typically where the bulk of the work lies.

Example 24.

Example 8 (1):

Set clearly satisfies the premises of Corollary 23 with the usual factorisation system given by surjective and injective functions. Then if we take T to be the finite powerset functor P f , and L to be the functor that adds a finite meet preserving operator to a Boolean algebra, it is shown in [START_REF] Jacobs | Exemplaric Expressivity of Modal Logics[END_REF]Theorem 9] that for a natural choice of δ, that δ * is componentwise injective. From this, and that P f preserves injections, Corollary 23 yields a dual adjunction between Alg(L) and CoAlg(P f ).

Expressivity

The notion of expressivity for a coalgebraic modal logic states that two states are logically equivalent if and only if they are behaviourally equivalent. Here logically equivalent means "have the same theory", and behaviourally equivalent means "can be identified in a model", where the identification is by means of coalgebra homomorphisms.

To investigate expressivity we need to access individual states of objects in X, so we make the additional assumption: Assumption 1. The category X is a concrete category [START_REF] Adámek | Abstract and Concrete Categories[END_REF] i.e. the objects are sets with some additional structure, and the morphisms have underlying functions. Technically this means we assume there is a faithful forgetful functor from X to the category Set. Definition 25. Given two models X 1 , X 2 in Mod(A, α), and states x 1 ∈ X 1 , x 2 ∈ X 2 , we say x 1 and x 2 are logically equivalent if

f 1 (x 1 ) = f 2 (x 2 )
where f 1 and f 2 are the theory maps of X 1 and X 2 respectively. Definition 26. Given two models X 1 , X 2 in Mod(A, α), and states x 1 ∈ X 1 , x 2 ∈ X 2 , we say x 1 and x 2 are behaviourally equivalent if there exists in Mod(A, α) a cospan

X 1 g1 / / X 3 X 2 g2 o o such that g 1 (x 1 ) = g 2 (x 2 ).
Our definition extends the standard definition of behavioural equivalence. The forgetful functor from Mod(A, α) to CoAlg(T ) yields the usual definition of behavioural equivalence as a cospan in CoAlg(T ) [START_REF] Kupke | Algebraic semantics for coalgebraic logics[END_REF], but in addition, the forgetful functor to X yields a condition that the theory maps are compatible. This is because we are working with arbitrary L-algebras, and not just the initial L-algebra, and is similar to the definition of bisimulation in [START_REF] Blackburn | Modal Logic[END_REF].

We have the following obvious result and definition.

Proposition 27. Given two models X 1 , X 2 in Mod(A, α), and states x 1 ∈ X 1 , x 2 ∈ X 2 , if x 1 and x 2 are behaviourally equivalent then x 1 and x 2 are logically equivalent.

Definition 28. An L-algebra (A, α) is expressive for Mod(A, α) if for all models in Mod(A, α), states are logically equivalent if and only if they are behaviourally equivalent.

To use internal models to investigate the phenomena of expressivity we must choose the class M to be a subclass of the class of monomorphisms that have injective underlying functions. See Example 36 (3) for a case where M is chosen to be a strict subclass.

Theorem 29. Given an L-algebra (A, α), and if M is a subclass of the class of monomorphisms in X that have injective underlying functions, then if the following hold:

1. every model in Mod(A, α) factors via some model in IntMod M (A, α), 2. for every pair I 1 , I 2 in IntMod M (A, α) there is a cospan

I 1 → I 3 ← I 2 in IntMod M (A, α), then (A, α) is expressive for Mod(A, α).
Proof. Take any pair of models X 1 and X 2 in Mod(A, α). Then these factor via the internal models I 1 and I 2 respectively, and by assumption there exists an internal model I 3 such that there exists a cospan

I 1 → I 3 ← I 2 in IntMod M (A, α).
Thus both X 1 and X 2 factor via I 3 . Spelling this out, the models ((X 1 , γ 1 ), f 1 ) and ((X 2 , γ 2 ), f 2 ) factor via the internal model ((

I 3 , ζ 3 ), m 3 ) via T -coalgebra morphisms g 1 : (X 1 , γ 1 ) → (I 3 , ζ 3 ) and g 2 : (X 2 , γ 2 ) → (I 3 , ζ 3 ) such that f 1 = m 3 • g 1 and f 2 = m 3 • g 2 .
Now suppose two states x 1 ∈ X 1 and x 2 ∈ X 2 are logically equivalent for (A, α). Then

f 1 (x 1 ) = f 2 (x 2 ), which means m 3 • g 1 (x 1 ) = m 3 • g 2 (x 2
), and since m 3 is injective, g 1 (x 1 ) = g 2 (x 2 ), and x 1 and x 2 are behaviourally equivalent.

The converse direction is given by Proposition 27.

In addition to Assumption 1, for several of the results that follow we will also need to make assumptions about the category Mod(A, α). Whenever we require these additional assumptions this will be indicated in the premises of the relevant proposition, lemma, or theorem. Assumption 2. Given an L-algebra (A, α) the category Mod(A, α) has small pushouts, a factorisation system (E Mod(A,α) , M Mod(A,α) ), and is E Mod(A,α)cowellpowered, where M Mod(A,α) is a subclass of those morphisms in Mod(A, α) with injective underlying functions, and E Mod(A,α) is a subclass of those morphisms in Mod(A, α) with surjective underlying functions.

Note that there is a forgetful functor from Mod(A, α) to Set since X is a concrete category, and further, since faithful functors reflect monomorphisms and epimorphisms [1, Propositions 7.37 and 7.44], we have

M Mod(A,α) ⊆ Inject Mod(A,α) ⊆ monos in Mod(A, α) E Mod(A,α) ⊆ Surject Mod(A,α) ⊆ epis in Mod(A, α)
where Inject Mod(A,α) is the class of morphisms in Mod(A, α) with injective underlying functions, and Surject Mod(A,α) those with surjective underlying functions.

Using Assumption 2 we can prove a converse to Theorem 29. The most difficult part is the proof that expressivity of (A, α) for Mod(A, α) implies that all models factor via internal models. The reason for this is that, whilst it is intuitively obvious that since we think of a theory map as having an underlying function it ought to factor via its image, the construction of a T -coalgebra structure map on this image need not be straightforward. We therefore need to ensure that any operations we might perform on a model always result in another model.

Theorem 30. Given an L-algebra (A, α), and with the following assumptions:

1. the conditions of Assumption 2 hold, 2. the class M of monomorphisms used to define IntMod M (A, α) is precisely the class of morphisms with injective underlying functions, if (A, α) is expressive for Mod(A, α) then every model in Mod(A, α) factors via an internal model in IntMod M (A, α).

Proof. We proceed as follows:

1. All model morphisms have an (E Mod(A,α) , M Mod(A,α) )-factorisation:

Any model morphism g : ((X, γ), f ) → ((X , γ ), f ) factors via a model ((I, ζ), f • m)
, where g = m • e, and e : ((X, γ), f

) → ((I, ζ), f • m) is in E Mod(A,α) and m : ((I, ζ), f • m) → ((X , γ ), f ) is in M Mod(A,α) . 2.
Take the pushout of the E Mod(A,α) -quotient objects of ((X, γ), f ):

Given a model ((X, γ), f ), since Mod(A, α) is E Mod(A,α) -cowellpowered, the collection of equivalence classes of E Mod(A,α) -quotient objects is indexed by a set J, and we can therefore take the pushout of a representative from each equivalence class <ej > ((I j , ζ j ), f j ), which by Theorem 20 we can write as (( <ej > I j , ζ), f † ) for some ζ and f † . This gives the following diagram

X f g $ $ ej / / / / I j mj / / fj ; ; pj X f / / S(A) <ej > I j f † E E
where any g : ((X, γ), f ) → ((X , γ ), f ) factors via a representative of one of the equivalence classes.

Construct a model epimorphism

h : ((X, γ), f ) → (( <ej > I j , ζ), f † ):
By the definition of a pushout there is a morphism h = p j • e j for all j ∈ J in Mod(A, α). To show that this is an epimorphism we use the fact that the forgetful functor V : Mod(A, α) → X reflects epimorphisms. Given any parallel pair of morphisms u and v in Mod(A, α) where

V (u), V (v) : <ej > I j → Y , if u • h = v • h, then u • p j • e j = v • p j • e j ,
but since e j is an epimorphism, we must have u • p j = v • p j = q j as in the following diagram

X h # # ej / / / / I j qj # # pj <ej > I j u / / v / / Y
Clearly the q j form a cocone for the pushout, so by the universal property of the pushout u = v, and thus h is an epimorphism. 4. Show h, p j ∈ E Mod(A,α) for all j ∈ J:

If we take the (E Mod(A,α) , M Mod(A,α) )-factorisation of h in Mod(A, α) given by e and m, then by the diagonalisation property of the factorisation system, there exists a unique Mod(A, α) morphism µ j for each j ∈ J such that the following diagram commutes

X ej / / / / e I j pj µj { { I m / / <ej > I j
Once again the µ j form a cocone for the pushout, so there exists a unique Mod(A, α) morphism η : <ej > I j → I such that µ j = η • p j . Now trivially id I • e = e, and also η

• m • e = η • m • µ j • e j = η • p j • e j = µ j • e j = e
so since e is an epimorphism we must have η • m = id I . Similarly, we have id <e j > Ij • h = h, and m • η • h = m • η • p j • e j = m • µ j • e j = p j • e j = h and since h is also an epimorphism, we must have m • η = id <e j > Ij . From this we deduce that m is an isomorphism, and therefore h ∈ E Mod(A,α) , and so by Proposition 4, p j ∈ E Mod(A,α) for all j ∈ J. 5. Show that f † has an underlying injective function:

Since <ej > I j has an underlying set we can pick a pair of states w 1 , w 2 ∈ <ej > I j . Now since h ∈ E Mod(A,α) is a surjective function, there exists states x 1 , x 2 ∈ X such that w 1 = h(x 1 ) and w 2 = h(x 2 ). Thus if f † (w 1 ) = f † (w 2 ) then f (x 1 ) = f (x 2 ), and by expressivity there must exist a g : ((X, γ), f ) → ((X , γ ), f ) such that g(x 1 ) = g(x 2 ), and therefore a j ∈ J such that m j •e j (x 1 ) = m j •e j (x 2 ). However, since m j ∈ M Mod(A,α) , we have that m j is injective, therefore e j (x 1 ) = e j (x 2 ). Thus p j • e j (x 1 ) = p j • e j (x 2 ), which implies h(x 1 ) = h(x 2 ), and therefore w 1 = w 2 . Therefore f † has an injective underlying function. 6. Observe that this makes (( <ej > I j , ζ), f † ) an internal model:

Since IntMod M (A, α) is defined in terms of precisely those morphisms with underlying injective functions, the model ((

<ej > I j , ζ), f † ) is an object in IntMod M (A, α).
Remark 31. It should be noted that the statement of Theorem 30 requires that the category of internal models that we consider include all models with an injective theory map. If we had instead tried to consider only models with theory maps that are, say, embeddings, Theorem 30 would fail to hold, as expressivity is not in general a strong enough condition to ensure f † is an embedding (consider topological spaces where injective continuous functions need not be embeddings).

Corollary 32. Given an L-algebra (A, α), and with the following assumptions:

1. the conditions of Assumption 2 hold, 2. Mod(A, α) has binary coproducts, 3. the class M of monomorphisms used to define IntMod M (A, α) is precisely the class of morphisms with injective underlying functions, if (A, α) is expressive for Mod(A, α) then for every pair

I 1 , I 2 in IntMod M (A, α) there is a cospan I 1 → I 3 ← I 2 in IntMod M (A, α).
Proof. Given two internal models I 1 and I 2 , since they are also models their coproduct exists, and by Theorem 30 the coproduct factors via an internal model, say I 3 , and this induces an obvious cospan between I 1 and I 2 .

From Theorems 29, 30, and Corollary 32 we obtain our main expressivity result -an abstract, category theoretic, characterisation of expressivity.

Theorem 33. Given an L-algebra (A, α), and with the following assumptions: The conditions of Assumption 2 follow from appropriate conditions on the category X and the functor T . Indeed, such conditions on X essentially summarise the category theoretic properties of Set that underpin the intuitive understanding that models with injective theory maps fully capture the notion of expressivity. This is made precise in the following corollary.

Corollary 34. Given an L-algebra (A, α), and with the following assumptions:

1. X is a concrete category (over Set) that is cocomplete, has a factorisation system (E X , M X ), and is E X -cowellpowered, where M X is chosen to be a subclass of those morphisms in X with injective underlying functions, and E X is chosen to be a subclass of those morphisms in X with surjective underlying functions, Proof. We have to show that the premises of Theorem 33 hold. Firstly we observe that by Theorem 20 Mod(A, α) is cocomplete.

T preserves M

X i.e. m ∈ M X ⇒ T (m) ∈ M X , 3
To show that the factorisation system of X lifts to Mod(A, α) we note that in [START_REF] Jacobs | Exemplaric Expressivity of Modal Logics[END_REF] it is observed that if T preserves M X , and the members of M X are monomorphisms, then the factorisation system of X lifts to CoAlg(T ), and it is easy to see that this extends to Mod(A, α).

Finally, Mod(A, α) is E X -cowellpowered since the morphisms in E X are epimorphisms, and this ensures that given a span in Mod(A, α) where the underlying morphisms are in E X , there is an isomorphism between the two so defined E X -quotient objects in Mod(A, α), if and only if, there is an isomorphism between the underlying E X -quotient objects in X.

The above characterisation of expressivity, whilst providing a neat, element free definition of expressivity, is not very useful for proving a given L-algebra is expressive for its category of models. For this we have a direct corollary of Theorem 29 that generalises [8, Theorem 4.2] and [6, Theorem 4] (they only consider the initial L-algebra and pairs of states in the same T -coalgebra).

Corollary 35. If given an L-algebra (A, α) the following hold:

1. X is a concrete category (over Set) with binary coproducts, and a factorisation system (E, M ), where M is a subclass of the class of monomorphisms in X that have injective underlying functions,

2. m ∈ M ⇒ δ * A • T (m) ∈ M , then (A, α) is expressive for Mod(A, α).
Proof. By Proposition 16 every model in Mod(A, α) factors via an internal model in IntMod M (A, α). Also since X has binary coproducts, by Theorem 21 the coproduct of every pair of objects in IntMod M (A, α) exists. So by Theorem 29 we have the result.

An examination of corollaries 23 and 35 reveals that with the exception of the exact choice of the class M , the primary difference is between requiring the base category X have all small coproducts or just binary coproducts. In most categories of interest finite cocompleteness usually also means cocompleteness, and so the existence of a dual adjunction between Alg(L) and CoAlg(T ) essentially amounts to every L-algebra being expressive for its class of models.

Example 36.

1. Example 24 (1): Every L-algebra (A, α) is expressive for Mod(A, α).

The category Alg(L) ∼ = MA (the category of modal algebras). Thus given a set of propositional variables, the free modal algebra over that set, quotiented by a set of axioms, represents a basic modal logic that is expressive for the image finite transition systems that are models for that logic. The category Alg(K) is isomorphic to the category of meet semilattices each with a countable set of order preserving unary operations. Thus a modal logic with finite conjunctions and probabilistic modalities, over an arbitrary set of propositional variables and axioms, is expressive for the Markov processes that are models for that logic.

These examples are generalisations of the results in [START_REF] Jacobs | Exemplaric Expressivity of Modal Logics[END_REF] to arbitrary L-algebras, not just the initial L-algebra, and thus in particular to modal logics with propositional variables and additional axioms. The results of [START_REF] Jacobs | Exemplaric Expressivity of Modal Logics[END_REF] can be retrieved by taking the intitial L-algebra, and then every T -coalgebra can be made into a model via a unique choice of theory map (forced by initiality).

Conclusions and Future Work

We have introduced internal models for a modal logic, and shown their utility for exploring properties of a logic. Indeed, it should be noted that with the exception of the proofs of the existence of colimits in Mod(A, α) and IntMod M (A, α), and the proof that expressivity implies that models factor via internal models, the proofs using internal models are relatively short. Most of the structure of Mod(A, α) is related to whether models always factor via internal models.

The category IntMod M (A, α) is not yet fully understood, and indeed, an obvious question is that, given that internal models can be thought of as generalisations of the canonical models of Kripke semantics, do internal models have anything to say about completeness? To answer this will require a systematic treatment of the different possible notions of semantic consequence that can be defined for the coalgebraic semantics of modal logics -local/global, and frame/model.

Several authors have used enriched categories in their work on coalgebras [START_REF] Hasuo | Generic forward and backward simulations[END_REF][START_REF] Kapulkin | Expressivity of Coalgebraic Logic over Posets[END_REF], and an interesting question is how much of the work of this paper will translate to the enriched setting, and what new phenomena can be addressed in such an enriched framework? Some preliminary work towards answering this question has been started.

  Research supported by an EPSRC Doctoral Training Account.

3 .Definition 2 .

 32 C has (E, M )-factorisations; i.e. every morphism f in C factors as f = m • e, with m ∈ M and e ∈ E. 4. C has the unique (E, M )-diagonalisation property; i.e. every commuting square in C with e ∈ E and m ∈ M , has a unique diagonal d such that the following commutes A e In a category C a factorisation system (E, M ) is called proper, if E is a subclass of the epimorphisms of C, and if M is a subclass of the monomorphisms of C. Example 3.

Definition 15 .

 15 We say a model X in Mod(A, α) factors via the internal model I in IntMod M (A, α) if there exists a morphism g : X → G(I) in Mod(A, α). It is possible to give very general conditions under which models factor via internal models. The following proposition is essentially a restatement of [8, Theorem 4.2] and [6, Theorem 4]. Proposition 16. If the category X has a factorisation system (E, M ) and m ∈ M ⇒ δ * A • T (m) ∈ M then every model in Mod(A, α) factors via an internal model in IntMod M (A, α). Proof. Consider a model ((X, γ), f ) in Mod(A, α). Then by the factorisation system there exists e ∈ E and m ∈ M such that f = m • e, and by the definition of a model, the perimeter of the following diagram commutes X e / / / / T (e)•γ I S(α)•m ζ z z T (I) δ * A •T (m) / / SL(A) and by assumption δ * A • T (m) ∈ M , and so by the diagonalisation property of the factorisation system, there exists a unique ζ : I → T (I) making the diagram commute. Thus ((I, ζ), m) is an internal model in IntMod M (A, α), and e is the morphism by which ((X, γ), f ) factors via ((I, ζ), m).

/

  and µ is the unique morphism in IntMod M (A, α) such that / S(A) Proof. By Proposition 16 ((X, γ), (g • f ) ) factors via ((I, ζ), m) with (g • f ) = m • e, and ((X , γ ), (g • f ) ) factors via ((I , ζ ), m ) with (g • f ) = m • e .

  then use the diagonalisation property of the factorisation system to construct a unique η : I → Z. 4. Use δ * A • T (h) ∈ M and thus a monomorphism to show that η is an internal model morphism, and (((I, ζ), m), e•τ j : D(j) → ((I, ζ), m)) j∈J is the colimit of D.

2 .

 2 Example 8 (3): Again take Set with the usual factorisation system. This time take T to be the valuation functor V O of[START_REF] Jacobs | Exemplaric Expressivity of Modal Logics[END_REF] Section 3.1]. This is a generalisation of the finite powerset, finitely supported discrete subdistribution, and finitely supported multiset functors. O is a downward-closed subset of a partially ordered commutative cancellative monoid M , and M also has the property x ≤ x + y for all x, y ∈ M . Then the valuation functor sends a set to the set of its valuations in OV O (X) = {φ : X → O | supp(φ) is finite and x∈X φ(x) ∈ O}The analogous generalisation of L in the previous example

1 .

 1 the conditions of Assumption 2 hold, 2. Mod(A, α) has binary coproducts, 3. the class M of monomorphisms used to define IntMod M (A, α) is precisely the class of morphisms with injective underlying functions, (A, α) is expressive for Mod(A, α) if and only if 1. every model in Mod(A, α) factors via an internal model in IntMod M (A, α), 2. for every pair I 1 , I 2 in IntMod M (A, α) there is a cospan I 1 → I 3 ← I 2 in IntMod M (A, α).

2 .

 2 Example 24 (2): Every K O -algebra (A, α) is expressive for Mod(A, α). The category Alg(K O ) is isomorphic to the category of meet semilattices each with a set of order preserving unary operations of cardinality | O|. Thus if (a) O = O = M = N, the monoid with (0, +), then Alg(K O ) is isomorphic to the algebras for the signature { , ∧, ♦ k } k∈N , where { , ∧} define a meet semilattice with top, and the ♦ k are order preserving. Thus the conjunction fragment of graded modal logic, over an arbitrary set of proposition variables and axioms, is expressive for the multi-transition systems that are models for that logic. (b) Similarly, if M = (R ≥0 , +, 0), O = [0, 1], and O = Q ∩ [0, 1], then finite conjunction modal logic, over an arbitrary set of proposition variables and axioms, with the standard probabilistic modalities, is expressive for the Markov chains that are models for that logic. 3. Example 24 (3): Every K-algebra (A, α) is expressive for Mod(A, α).

  Meas is wellpowered and cocomplete. Also in[START_REF] Jacobs | Exemplaric Expressivity of Modal Logics[END_REF] Section 3.1] it is observed that morphisms with surjective underlying functions, and morphisms with injective underlying functions and surjective inverse image functions, form a factorisation system (E, M ). Moreover, the Giry functor (or monad) G is observed to preserve M . For L take K, an instance ofK O above, for O = Q ∩ [0, 1].Then for a natural choice of δ, it is shown in[START_REF] Jacobs | Exemplaric Expressivity of Modal Logics[END_REF] Theorem 17] that δ * is componentwise in M . From this, Corollary 23 yields a dual adjunction between Alg(K) and CoAlg(G).

is K O , where O is a dense subset of O, and this functor adds to a meet semilattice an order preserving modality o for each o ∈ O. It is shown in [6, Theorem 13] that for a natural choice of δ, that the resulting δ * is componentwise injective. From this, and that V O preserves injections, Corollary 23 yields a dual adjunction between Alg(K O ) and CoAlg(V O ). 3. Example 8 (4): Since σ-algebras are closed under intersection, Meas is topological over Set, and since Meas is fibre-small, by [1, Theorem 21.16],

  . the class M of monomorphisms used to define IntMod M (A, α) is precisely the class of morphisms with injective underlying functions i.e. M X ⊆ M , (A, α) is expressive for Mod(A, α) if and only if 1. every model in Mod(A, α) factors via an internal model in IntMod M (A, α), 2. for every pair I 1 , I 2 in IntMod M (A, α) there is a cospan I 1 → I 3 ← I 2 in IntMod M (A, α).

The elements of L(A) are actually equivalence classes of elements of A arising from a free Boolean algebra construction over the underlying meet semilattice of A [10, Proposition 3.12].

Acknowledgements. The author would like to thank Corina Cîrstea for the many interesting discussions, her invaluable guidance, and her careful proof reading. Many thanks also go to John Power for his detailed feedback on an early draft of this paper, and to the anonymous referees for their encouraging feedback and useful suggestions.


Marcello M Bonsangue

Jan Rutten

Joost Winter

Defining Context-Free Power Series Coalgebraically

des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

In [START_REF] Winter | Contextfree languages, coalgebraically[END_REF], we gave a coalgebraic presentation of context-free languages, characterizing them by means of so-called systems of behavioural differential equations. These equations define languages by specifying their initial (or output) value, which signals the presence of the empty word in the language, together with their (Brzozowski) input derivatives: one derivative for each letter in the alphabet of the languages under consideration. The main result of [START_REF] Winter | Contextfree languages, coalgebraically[END_REF] was a precise definition of a format for such behavioural differential equations, together with the observation that a language is context-free if and only if it can be specified by means of a system of equations in this format.

In the present paper, we will generalize the approach above from languages to formal power series, for which we define a general notion of context-freeness, again in terms of a well-defined class of behavioural differential equations. Formal power series include as examples languages but also other types of systems such as streams and infinite binary trees. Next we will connect our coalgebraic notion of context-free power series to various existing notions of algebraic power series, and establish, for a large number of cases, equivalence of these notions.

More precisely, we will provide a general, coalgebraic notion of contextfreeness and we will show the following existing notions to be instances thereof:

-Automatic sequences over a finite field IF q .

-Algebraic power series (as zeros of polynomial equations) in a single variable, over a perfect field F . All these notions are equivalent to each other, and to the notion of 'contextfree' power series defined in this article. We shall prove the latter through an easy correspondence between behavioural differential equations and algebraic systems in Greibach normal form. The other correspondences, some of which are not widely known, can all be found elsewhere in the literature (see Figure 1 for an overview of the various equivalences and for references to the literature).

The paper is organized as follows. In Section 2, we recall some of the basic definitions regarding algebraic structures; formal power series; and the coinductive calculus for streams and power series, fixing some notation as we go along. Section 3 will define our coalgebraic notion of a context-free power series, by means of behavioural differential equations. In Section 4, we will relate our coalgebraic notion of context-freeness to the various notions of algebraicity.

In addition to providing a unified view on many different but related notions of algebraicity, we shall illustrate, in Section 5, that the coalgebraic definition of context-freeness enables us to give new, transparent proofs of existing theorems. Two examples will be: a new proof for a result by Chomsky and Schützenberger (Section 5.2); and a new proof of various closure properties, such as the fact that the zip-operation applied to two algebraic streams again yields an algebraic stream (Section 5.1).

Acknowledgements: We would like to express our gratitude to Jeffrey Shallit, for pointing us towards the article by Michel Fliess [START_REF] Fliess | Sur divers produits de sries formelles[END_REF], in which the two notions of algebraicity are related, as well as to Jean Berstel, Christophe Reutenauer, Jean-Paul Allouche and Arto Salomaa. We thank the referees for providing constructive comments and help in improving this paper.

Preliminaries

Algebraic Structures

Recall that a semiring (S, +, •) consists of a set S, together with two binary operations + and •, and constants 0, 1 ∈ S, satisfying the following conditions for all s 1 , s 2 , s 3 ∈ S:

s 1 + (s 2 + s 3 ) = (s 1 + s 2 ) + s 3 s 1 • (s 2 • s 3 ) = (s 1 • s 2 ) • s 3 s 1 + 0 = s 1 = 0 + s 1 s 1 • 1 = s 1 = 1 • s 1 s 1 + s 2 = s 2 + s 1 s 1 • (s 2 + s 3 ) = s 1 • s 2 + s 1 • s 3 s 1 • 0 = 0 = 0 • s 1 (s 1 + s 2 ) • s 3 = s 1 • s 3 + s 2 • s 3
A ring (R, +, •) is a semiring in which, for every element r 1 ∈ R, there is an additive inverse r 2 ∈ R, such that r 1 + r 2 = 0 = r 2 + r 1 . A ring is called commutative if for all r 1 , r 2 ∈ R, we have r 1 • r 2 = r 2 • r 1 .

A field (F, +, •) is a commutative ring in which for every element

f 1 ∈ F with f 1 = 0, there is a multiplicative inverse f 2 such that f 1 • f 2 = 1 = f 2 • f 1 .
For every field (F, +, •), there is a unique semiring homomorphism f from the semiring (IN, +, •) to F . If there are elements n ∈ IN with n = 0 such that f (n) = 0 F , we say F has characteristic p if p is the smallest number with this condition; if there are no such elements, we say that F has characteristic 0. Whenever F has characteristic 0 then F is infinite, otherwise if p = 0 then p is a prime number and F is a finite field.

We say a field F is perfect when F has either characteristic 0, or when F has characteristic p and, for every f ∈ F , there is a g ∈ F such that f = g p (here we inductively define g 0 = 1 and g n+1 = g • g n ). Examples of perfect fields are the reals and of the rationals. The field of rational functions in one variable and with coefficients over a finite field is an example of a field that is not perfect.

Formal Power Series

In this subsection, we will introduce, using mostly classical notation, formal power series with coefficients in semirings S, and (noncommuting) variables in a finite alphabet A. Such series were originally introduced as a generalization of classical power series, abstracting away from the traditional interpretation as Taylor series of a function. Another way to look at formal power series is to regard them as generalizations of formal languages, or as a presentation of weighted languages over some semiring S and an alphabet A.

For the remainder of this section, we fix a finite set A, called the alphabet, as well as a semiring (S, +, •) to denote the coefficients of the power series. Furthermore, recall that the set A * of words over A corresponds to the free monoid over A.

Given a semiring (S, +, •), and an alphabet A, a formal power series with coefficients in S and noncommuting variables in A is a function σ : A * → S assigning to each word in A * an element of S. We let S A denote the set of all power series with coefficients in S and variables in A. In the literature, the notation (σ, w) is widely used to denote the value of the series σ at the word w. In this paper, we will in addition often use the notation σ(w) instead of (σ, w).

Given a formal power series σ, we say its support is the set of words w ∈ A * such that σ(w) = 0. We call a formal power series σ polynomial whenever its support is a finite set, or in other words, there are only finitely many words w such that σ(w) = 0. The set of all polynomial power series with coefficients in S and variables in A is denoted by S A .

We will be using the fact that the set S A of all power series is a final coalgebra of the functor S × (-) A [START_REF] Jan | Behavioural differential equations: a coinductive calculus of streams, automata, and power series[END_REF]. The final coalgebra structure can be defined using a generalisation of the notion of Brzozowski derivatives, originally introduced for regular expressions and languages, as follows.

Given a coalgebra (X, (o, δ) : X → S × X A ), and an element x ∈ X, we write x a for δ(x)(a), and call it the a-derivative of x; furthermore, we call o(x) the output value of x. The set S A can now be given a S × (-) A -coalgebra structure by defining, for σ ∈ S A , a ∈ A and w ∈ A * , σ a (w) := σ(a • w) and by setting, furthermore, o(σ) := σ(λ), where λ is the empty word. One can easily prove that this turns S A into a final coalgebra for the functor S ×(-) A . Given any coalgebra for this functor, and an element t of its carrier set, we let t denote the value of t under the unique homomorphism of this coalgebra to S A . Given a coalgebra (X, (o, δ)) can furthermore generalize the notion of Brzozowski derivatives from derivatives to alphabet symbols to word derivatives, by setting x λ for all x ∈ X and inductively defining x a•w = (x a ) w .

We also recall the following notion. For two S×(-)

A -coalgebras (X, (o X , δ X )) and (Y, (o Y , δ Y )), a relation R ⊆ X × Y is a bisimulation if (x, y) ∈ R implies o X (x) = o Y (y)
and, for all a ∈ A, (x a , y a ) ∈ R.

A coinductive calculus for streams and power series

We briefly recall a few basic facts from [START_REF] Jan | Behavioural differential equations: a coinductive calculus of streams, automata, and power series[END_REF], where a coinductive calculus of streams, languages and formal power series was introduced.

An algebraic structure can be conveniently given to the set S A of formal power series by defining operators by means of so-called behavioural differential equations. For instance,the (element-wise) sum of two series σ and τ is defined as the unique series satisfying the following equations:

o(σ + τ ) = o(σ) + o(τ ) (σ + τ ) a = σ a + τ a
for all a ∈ A. Similarly, the following equations If the alphabet A is a singleton set: A = {X}, then S A coincides with the set S ω of streams over S. In that case, we write σ for σ X (and often also σ(0) for o(σ)). If S is a field then for every series σ with o(σ) = 0 there exists an inverse, defined by the following equations:

o(σ • τ ) = o(σ) • o(τ ) (σ • τ ) a = σ a • τ + [o(σ)] • τ a
o(σ -1 ) = o(σ) -1 (σ -1 ) = -o(σ -1 ) • σ • σ -1
We will use the following shorthand notation:

σ τ := σ • τ -1
For more details see [START_REF] Jan | Behavioural differential equations: a coinductive calculus of streams, automata, and power series[END_REF] and [START_REF] Jan | A coinductive calculus of streams[END_REF].

Context-free power series

In this section, we will present a format for behavioural differential equations that generalizes the format used to characterize context-free languages, presented in [START_REF] Winter | Contextfree languages, coalgebraically[END_REF]. Here we will introduce a format for formal power series, which we will use to define the notion of context-free power series. As we will see later, the present notion coincides with an existing notion of context-free power series in the literature. We start by presenting a syntax describing our format of behavioural differential equations. As before, let A be a finite set of alphabet symbols and let S be a semiring. Furthermore, let X be a (possibly infinite) set of variables. The variables x ∈ X will represent power series in S A .

We call a behavioural differential equation (for formal power series) wellformed if it consists of (i) an equation o(x) = s, with s ∈ S, which specifies the output value of x; and (ii) an equation x a = t, for each a ∈ A, with t ∈ T X, where T X is the following inductively defined set of terms:

T X t ::= s ∈ S | x ∈ X | a ∈ A | t + t | t • t
We say that a system of equations is context-free for X if it consists of one wellformed equation for each x ∈ X. Equivalently, a context-free system of equations over X can be viewed as a mapping f : X → S × T X A , by defining f = (o, δ) with δ(x) = x a , as before.

We notice that for every set X, S × T X A carries a suitable algebra structure so that we can interpret the above terms transforming a context-free system of equations f :

X → S × T X A into a S × (-) A -coalgebra f : T X → S × T X A ,
where f is defined inductively as follows:

t o(t) t a x o(x) x a (as specified by f ) s s 0 b 0 if b = a then 1 else 0 u + v o(u) + o(v) u a + v a u • v o(u) • o(v) u a • v + o(u) • v a
Next we can combine a system of equations f : X → S × T X A , its extension f , and the final homomorphism into the final coalgebra S A , in the following diagram:

X ⊂ i -T X - -S A S × T X A f ? - f S × (S A ) A ?
A solution for our context-free system of equations is an assignment of variables x ∈ X to power series s x such that s x = i(x) ∈ S A for all x ∈ X.

The above diagram shows that by every context-free system of equations has a unique solution, fixed by the definition extending f to f , and the unique homomorphism from the coalgebra (T X, f ) into the final coalgebra.

The same solution can also be obtained by providing an appropriate semiring structure to S × T X A , which is equivalent to defining the extension from f to f in the sense that there is a unique semiring morphism from the free semiring (with variables in S, X, and A) T X to S × T X A with the provided semiring structure, such that a) when applying the forgetful functor to this morphism, we obtain f , and b) making the left part of the diagram commute. In this sense, the work here can be seen as an instance of the coalgebraic generalization of the powerset construction (see e.g. [START_REF] Silva | Generalizing the powerset construction, coalgebraically[END_REF]).

By using the definition of f , one can furthermore easily show that t 1 + t 2 is the sum of t 1 and t 2 , whereas t 1 • t 2 is the convolution product of t 1 with t 2 . Definition 1. We call a formal power series over a semiring S and an alphabet A context-free if it is the solution of a context-free system of behavioural differential equations, for some finite set X of variables.

As a first example of a context-free power series (over the semiring of the natural numbers and over a singleton alphabet), taken from [START_REF] Jan | Coinductive counting: bisimulation in enumerative combinatorics[END_REF], consider the stream defined by the following equation:

o(x) = 1 x = x • x (1)
Its solution is the stream of Catalan numbers 1, 1, 2, 5, 14, 42, 132, 429, 1430, . . .

The nth element of this stream counts the number of well-bracketed words consisting of n pairs of opening and closing brackets. In Section 5.2, we will show how to derive the above equation from a context-free grammar representing pairs of brackets.

Another example of a context-free stream, using the finite field IF 2 (characterized by 1 + 1 = 0) as underlying semiring, is defined by the following system of equations (where now X = {x, y, z, w}):

o(x) = 0 x = y o(y) = 1 y = z o(z) = 1 z = z + y + x • x • w o(w) = 1 w = y • w
One can show that this system of equations generates the stream 0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1, 0, 1, 1, 0, . . . which is the so-called Thue-Morse sequence. (This stream can also be characterized as the morphic sequence generated by the morphism with p(0) = 01 and p(1) = 10.) In Appendix A, a derivation of this system of equations will be given, and in Section 4.3, we will see yet another characterization of this sequence.

In some situations, it is convenient to deal with terms in a disjunctive normal form. We will later see that weighted grammars in weak Greibach normal form can be directly regarded as systems of equations in which every derivative is in disjunctive normal form. Definition 2. A system of equations f : X → S ×T X A is in disjunctive normal form if for every x ∈ X and a ∈ A, x a = t where t is a term of the following form:

t ::= c | c + t c ::= a • c | x • c | s (a ∈ A, x ∈ X, s ∈ S)
We let the subset of T X consisting of all terms that are in disjunctive normal form be denoted by DX. It is not very difficult to prove that every well-formed system of equations is equivalent to a system in disjunctive normal form.

Algebraicity and context-freeness

In this section, we will connect the notion of context-free power series defined above with several existing notions of algebraic power series, as well as with series definable by weighted grammars and q-automatic sequences.

We recall the following definition of algebraicity, given in [START_REF] Petre | Handbook of Weighted Automata, chapter Algebraic systems and pushdown automata[END_REF], and originating from [START_REF] Fliess | Sur divers produits de sries formelles[END_REF].

Definition 3. An S-algebraic system is a set of equations of the form

x i = p i i ≤ n
for some fixed n ∈ N, where p i ∈ S A ∪ X . Such a system is called proper if, for all i, (p i , λ) = 0, and for all i, j ≤ n, (p i , x j ) = 0. Furthermore, such a system is said to be in Greibach normal form if its support is contained in the set A ∪ AX ∪ AXX.

A solution to an S-algebraic system consists of an assignment of power series in S A to the variables x i , such that, when replacing the variables x i with the associated power series, all of the equations hold [START_REF] Petre | Handbook of Weighted Automata, chapter Algebraic systems and pushdown automata[END_REF]. In general, a solution to an S-algebraic system does not need to exists, and if a solution exists, it does not need to be unique. However, whenever a system is proper, a unique solution exists, and can be constructed as limit of an approximation sequence of power series starting from 0. Such solutions are called strong solutions [START_REF] Petre | Handbook of Weighted Automata, chapter Algebraic systems and pushdown automata[END_REF].

Definition 4. A strong solution to an S-algebraic system is solution where for each power series σ associated to a variable x, (σ, λ) = 0 holds. We call a formal power series σ (constructively) S-algebraic if it can be written as s + σ, where s ∈ S and σ is a strong solution to an S-algebraic system.

In [START_REF] Petre | Handbook of Weighted Automata, chapter Algebraic systems and pushdown automata[END_REF], the following results w. Given an S-algebraic system in Greibach normal form, it is easy to see that it is equivalent to a system of behavioral differential equations representing a context-free power series. Furthermore, if σ is context-free then also σ + s is context-free, for any s ∈ S. It follows that any constructively S-algebraic power series also is context-free.

For the other direction, take any system of behavioural differential equations, and a variable y in this system representing a context-free power series. From this system, we construct a new system as follows: we replace each variable x ∈ X by a variable x such that (x, λ) = 0 and for all w ∈ A + , (x, w) = (x, w). We do this, by setting o(x) = 0 for each x ∈ X, and in each expression representing x a , substituting (ȳ + (y, λ)) for each y ∈ X in the corresponding expression for xa . It is easy to see that this new system of equations can be regarded as a proper S-algebraic system, so it follows that ȳ, and hence also y, is constructively S-algebraic.

All in all, we have obtained the following:

Theorem 5. A formal power series over a semiring S is S-context-free iff it is constructively S-algebraic.

Weighted grammars and languages

Another way of viewing context-free power series is by regarding them as (weighted) languages generated by weighted context-free grammars [START_REF] Petre | Handbook of Weighted Automata, chapter Algebraic systems and pushdown automata[END_REF]. A context-free grammar weighted over a semiring S consists of a set X of nonterminals, a set A of terminals, and an assignment

f : X → P ω (S × (A ∪ X) * )
representing the traditional production rules of a context free grammar each associated with a weight in S. We write x s → u whenever (s, u) ∈ f (x), to say that x produces u with weight s.

We say that such a grammar is in weak Greibach normal form if, for every production x s → u, u is either the empty word λ, or of the form a • w, with a ∈ A, and w ∈ (A ∪ X) * .

We can now extend weighted rules to weighted derivations as follows: when v is a sequence of terminals in A * , x is a nonterminal in X, and w is a sequence of both terminals and nonterminals in (A ∪ X) * , we write vxw s ⇒ vuw iff x s → u, and call this a single leftmost derivation (with weight s). A leftmost derivation of word w ∈ A * from a nonterminal x ∈ X is finite sequence of single leftmost derivation x s1 ⇒ . . . sn ⇒ w. There may be many different ways a word can be derived from a nonterminal x, therefore we can (try to) assign a weight s to every word w derived from x, denoted by x s ⇒ * w as follows:

s = x s 1 ⇒... sn ⇒w n s i .
The idea here is to take the sum over all derivations, and within each derivation, to take the product of the weight of each of the steps involved in the derivation. Note, however, that this sum may be an infinite sum which is not necessarily always defined. It is, however, always defined, whenever the grammar is in weak Greibach normal form. Grammars over the Boolean semiring or over the semiring of natural numbers extended with infitity always have an equivalent Greibach normal form [ ÉL05].

Given a weighted grammar in Greibach normal form, we can construct a system of behavioural differential equations, with X, the set of nonterminals from the grammar, as set of variables for the system. We now can set o(x) = s if there is a production rule x s → λ, and o(x) = 0 if no such rule exists; and furthermore, set

x a = x s →a•w s • w
The equivalence between weighted grammars in weak Greibach normal form and well-formed systems of behavioural differential equations essentially follows from the following proposition, the easy proof of which is omitted. Proposition 6. For any word w ∈ A * have o(x w ) = s iff x s ⇒ * w.

F -algebraic streams

Next we consider yet another notion of algebraicity, which applies only to formal power series in one variable (here typically denoted by X), that is, streams, with coefficients in a field F . Definition 7. An F -stream σ is called F -algebraic iff there exist polynomial F -streams p 1 , . . . , p n , with at least one p i not equal to zero, such that i≤n p i σ i = 0.

The next proposition shows that under very mild conditions, we can constructively show that F -algebraic streams are context-free.

Proposition 8. Given any field F , let σ be an F -algebraic stream that is a solution to the equation i,j≤m,n f ij X j σ i = 0 (recall that a polynomial p is of the form i≤n f i X i ). Whenever i≤m f i0 ( k<i o(σ) k σ i-k-1 ) = 0, then σ is context-free (and hence also constructively F -algebraic).

Proof. Note that i,j≤m,n

f ij σ i X j = i≤m f i0 σ i + i≤m,1≤j≤n f ij σ i X j = 0
where all f ij ∈ F . Taking derivatives, we now obtain

σ i≤m f i0 ( k<i o(σ) k σ i-k-1 ) + i≤m,1≤j≤n f ij σ i X j-1 = 0 and hence σ i≤m f i0 ( k<i o(σ) k σ i-k-1 ) = - i≤m,1≤j≤n f ij σ i X j-1
When i≤m f i0 ( k<i o(σ) k σ i-k-1 ) = 0, we can rewrite this as

σ = - i≤m,1≤j≤n f ij σ i X j-1 i≤m f i0 ( k<i o(σ) k σ i-k-1
) from which we can easily eliminate the fraction by introducing a new variable τ representing ( i≤m f i0 ( k<i o(σ) k σ i-k-1 )) -1 .

Leaving out some further intermediate steps, we obtain the following system of behavioural differential equations in two variables, with o(σ) given:

σ = -( i≤m,1≤j≤n f ij σ i X j-1 ) • τ o(τ ) = ( i≤m f i0 • (i -1) • o(σ) i ) -1 τ = -o(τ ) • σ • ( i≤m f i0 ( k≤i-1 o(σ) k ( j≤i-k-2 o(σ) j σ i-j-k-2 ))) • τ
There is the following, more general result by Fliess [START_REF] Fliess | Sur divers produits de sries formelles[END_REF], stating that the notions of algebraic and constructively algebraic (and hence context-free) coincide for any perfect field.

Proposition 9. Let F be a perfect field. Then a stream σ over F is F -algebraic iff it is constructively F -algebraic. This result is not very well-known. Its proof [Fli74, Proposition 7] is not very easy and too long to repeat here. We see it as one of the challenges for future research to better understand this proof, possibly by rephrasing it into the language of the present setting, along the lines of Proposition 8.

Automatic sequences

The theory of k-automatic sequences, developed in e.g. [START_REF] Allouche | Automatic Sequences -Theory, Applications, Generalizations[END_REF], is primarily concerned with streams over the set {0, . . . , k-1} that are characterized by so-called k-automata. Basically, a k-automaton is a deterministic Moore automaton with the set {0, . . . , k -1} as both input and output alphabets. However, differently from a Moore automaton, a k-automaton accepts streams. In fact, an infinite sequence σ is said to be k-automatic whenever a k-automaton exists, such that, for any n ∈ IN, taking the base k representation of n as input, the nth element σ(n) is yielded as output. More formally: Definition 10. For any number k ∈ IN, a k-automaton is a deterministic automaton A = (Q, T, q 0 , o), with Q as set of states, T : Q × {0, . . . , k -1} → Q as transition function, an initial state q 0 , and an output function o : Q → {0, . . . , k -1}.

A sequence σ(0)σ(1)σ(2) . . . is called k-automatic whenever σ(i) is the output obtained by taking the base k representation of the number i as input, for some k-automaton A.

As an example of an automatic sequence, consider the 2-automaton

q 0 /0 q 1 /

Applications of Context-Free Systems of Equations

In this section, we will see some examples of how the systems of context-free behavioural differential equations can be put to use, giving some clear and transparent proofs of existing theorems. The first example will provide a proof that the zip-operator, in all cases, preserves algebraicity, and the next example will consist of a new proof of a theorem by Chomsky and Schützenberger.

Zip preserves context-freeness

As an application of the above equivalences, we will now provide a newer and simpler version of [NR10, Proposition 18], stating that the zip operation preserves F -algebraicity over any field F . Recall that the zip operation can be defined coinductively as follows:

o(zip(σ, τ )) = o(σ) zip(σ, τ ) = zip(τ, σ )
We will now start by showing that, if σ is S-algebraic over a semiring S, then so are zip(σ, 0) and zip(0, σ): Proposition 12. If σ is a S-algebraic stream over a semiring S, then zip(σ, 0) and zip(0, σ) are also S-algebraic.

Proof. Let σ be characterized by a system of equations in disjunctive normal form with X as set of variables. Now consider the following translation of terms in disjunctive normal form:

T(s) = s (s ∈ S) T(X • c) = X • (X • T(c)) T(x • c) = x • T(c) (x ∈ X) T(c + t) = T(c) + T(t)
and consider a new system of equations, with X = {x | x ∈ X} as new set of variables, and set, for x ∈ X: o(x) = o(x), and x = X • T(x ). Now consider the relation

R = {(zip(u, 0), T(u)) | u ∈ DX} ∪ {(zip(0, u), X • T(u)) | u ∈ DX}
which is easily seen to be a bisimulation (up-to bisimilarity and addition) between the old system augmented with the zip-operator, and the new system. Hence, it follows that zip(σ, 0) and zip(0, σ) are also S-algebraic.

We can now directly continue with the theorem:

Theorem 13. Given a semiring S and streams σ and τ , zip(σ, τ ) is S-algebraic iff both σ and τ are S-algebraic.

Proof. For the right to left direction, use zip(σ, τ ) = zip(σ, 0) + zip(0, τ ), the previous result, plus the fact that addition preserves algebraicity. The left to right direction is also easy.

By using Fliess's Theorem 9, this result directly generalizes to F -algebraic streams over any perfect field F , and to automatic sequences.

A further easy generalization is using the n-zip of n > 2 different streams σ 1 , . . . , σ n , defined as follows:

o(n-zip(σ 1 , . . . , σ n )) = o(σ 1 ) n-zip(σ 1 , . . . , σ n ) = n-zip(σ 2 , . . . , σ n , σ 1 )
The following theorem can now be proved in a similar way as Theorem 13: Theorem 14. Given any semiring S and streams σ 1 , . . . , σ n , n-zip(σ 1 , . . . , σ n ) is S-algebraic iff all σs are S-algebraic.

Deriving systems of equations for streams

A theorem by Chomsky and Schützenberger states the following: if L is a contextfree language admitting an unambiguous CFG, and a k is the number of words of length k in L, then k∈IN a k x k is IN-algebraic. We will provide a proof of this theorem using systems of behavioural differential equations, that also gives us a way to construct k∈IN a k x k as a context-free power series.

The next theorem directly relates the degree of ambiguity of any CFG in weak Greibach normal form to a context-free formal power series using the semiring of natural numbers as underlying semiring. Recall that the degree of ambiguity of a word w w.r.t. a starting symbol x is equal to the number of distinct leftmost derivations x ⇒ * w [Nij80,PS09].

A lot of the argumentation and proofs in this section, even though not directly coinductive in the sense of using bisimulation techniques, still make use of the coalgebraic perspective. In fact the proofs of Propositions 15 and 16 are, at the heart, based on transformation of systems of behavioural differential equations to new equations. Proposition 15. Let (X, p) be a CFG in weak Greibach normal form over an alphabet A. We take the following system of equations, with IN as underlying semiring, and X as set of variables. For each x ∈ X, let o(x) = 1 if x → λ and 0 otherwise, and let Proof. We proceed by induction on w.

Base step: if w = λ, then the number of distinct leftmost derivations t ⇒ * w is 1 iff every symbol in t is a variable x with a rule t → λ, and 0 otherwise. But this corresponds precisely to o(t w ) = o(t).

Induction step: say w = a • w , and the theorem holds for all v with |v| < |w|. We distinguish three cases now.

#(v • t ⇒ * w ) + (If x → λ then #(t ⇒ * a • w ) else 0)
where #(t ⇒ * w) is the number of distinct leftmost derivations of w from t (if t is a variable x taken as a starting symbol, then this is the degree of ambiguity of w [Nij80,PS09]). Also,

o((x • t ) (a•w ) ) = o(((x • t ) a ) w = o((x a • t + o(x) • t a ) w ) = o(( v:x→av (v • t ) + o(x) • t a ) w ) = v:x→av o((v • t ) w ) + o(x) • o(t a•w )
Now apply the inductive hypothesis.

Proposition 16. Take a system of equations as constructed in Proposition 15. Now construct a new system of equations, representing a stream over IN, as follows: for each variable x in the old system, we let the new system have a corresponding variable x.

We now introduce a translation of terms with the following inductive definition:

T(n) = n for n ∈ IN, T(x) = x for x ∈ X, T(a) = X for a ∈ A, T(t + u) = T(t) + T(u), and T(t • u) = T(t) • T(u).
Using this translation, we now set o(x) = o(x), and x = a∈A T(x a ), and make the following claim: for all terms t in the old system, and for all n ∈ IN o(T(t) (n) ) = Base case: if n = 0, the only w s.t. |w| = n is λ, so the claim now amounts to o(T(t)) = o(t), which can easily be seen by induction on t.

Inductive step: assume that the claim holds for all m < n. For n, use induction on terms. If t = x, then (as T(x) = x) the claim amounts to

o(x (n) ) = w:|w|=n o(x w )
But on one hand we now have

o(x (n) ) = o((x ) (n-1) ) = o(( a∈A T(x a )) (n-1) ) = a∈A o(T(x a ) (n-1) )
and on the other hand we have and the desired equality now follows by applying the inductive hypothesis.

In the case where t = u • v, we make use of the equalities

(u • v) (n) = k=0...n o(u (k) ) • v (n-k) and (u • v) w = w=pq o(u p ) • v q Now observe o(T(u • v) (n) ) = o((T(u) • T(v)) (n) ) = o( k=0...n o(T(u) (k) ) • T(v) (n-k) ) = k=0...n o(T(u) (k) ) • o(T(v) (n-k) )
and

w:|w|=n o((u • v) w ) = w:|w|=n o( w=pq o(u p ) • v q ) = w:|w|=n w=pq o(u p ) • o(v q ) = k=0...n ( p:|p|=k o(u p ))( q:|q|=n-k o(v q ))
Applying the (inner) inductive hypothesis now yields

o(T(u • v) (n) ) = w:|w|=n o((u • v) w ),
as required.

The remaining base cases and inductive cases (w.r.t. the inner induction on terms) are easy. Furthermore, it is known from e.g. [Nij80, Section 5.2.1] that, if a context-free language admits an unambiguous, non-left-recursive grammar (i.e. a grammar with no a ∈ A and w ∈ (A ∪ X) * such that a ⇒ + aw), then it also admits an unambiguous grammar in Greibach normal form.

Together (and sometimes combined with a bit of ingenuity), these theorems form the ingredients for deriving systems of equations for a specification of certain sequences, such as the Catalan numbers or the Schroeder numbers, as context-free streams.

As a first example, consider the Catalan numbers. It is well-known that the nth Catalan number corresponds to the number of ways to combine n pairs of matching brackets. An unambiguous CFG in (weak) Greibach normal form representing matching pairs of brackets is x → axbx | 1 which corresponds to the system of equations

o(x) = 1 x a = xbx
We can transform this into a context-free specification of a stream, the even elements of which are the Catalan numbers, by replacing every alphabet symbol by the formal variable X:

o(σ) = 1 σ = σ • X • σ Now, because multiplication in streams is commutative, we can replace σ•X•σ by X • σ • σ.
Now, if we remove the remaining X from the system of equations we obtain a new stream the elements of which are exactly the even elements of the previous stream, that is, exactly the Catalan numbers. That this is the case is easily seen by providing a bisimulation, relating the system

o(σ) = 1 σ = X • σ • σ to zip(τ, υ)
, where τ is the stream of the Catalan numbers as defined earlier in (1), and υ is a stream of 0's:

o(τ ) = 1 τ = τ • τ o(υ) = 0 υ = υ
6 Conclusions and future work

We have presented a new, coalgebraic definition of context-free power series, by means of well-formed systems of behavioural differential equations. In addition, we have shown this new definition has various existing notions as instances, including context-free languages, algebraic power series, automatic sequences, and weighted context-free languages.

Behavioural differential equations offer a very general and elegant mechanism for the definition of streams, languages and more generally formal power series. For one thing, they allow the use of coinduction when proving equalities and general laws. Further, by restricting the shape or format of these differential equations, one can characterize different classes of solutions. We see our definition of context-free power series as an interesting new instance of this more general phenomenon. (Other existing examples include linear behavioural differential equations, used for instance to define rational streams.)

It has also been an interesting exercise to establish and find in the literature the various results on how the different notions, such as context-free and algebraic, are related. One of the surprises was the theorem by Fliess on the equivalence of F -algebraic and constructively algebraic streams (cf. the acknowledgements).

It remains interesting to see how much further we can carry this process of finding coalgebraic proofs of language-theoretic theorems. Still on our list is a more transparent proof of Fliess' original theorem. A possible further direction for research is to investigate what can be done by varying the coinductively defined operators: for example, by adding the Hadamard product as a primitive, it is known that we will reach a class of power series beyond the algebraic/contextfree class described in this paper.

A A concrete derivation of the context-freeness of Thue-Morse

In this appendix we find a specification of the Thue-Morse sequence as a contextfree stream. We start from the following polynomial:

X + (1 + X 2 )σ + (1 + X + X 2 + X 3 )σ 2
It is known that this polynomial has exactly two zeroes, namely the Thue-Morse sequence (0, 1, 1, 0, 1, 0, . . .) and its inverse (1, 0, 0, 1, 0, 1, . . .).[AS03, Example 12.1.2] We will now derive a system of behavioral equations for the Thue-Morse sequence itself, i.e. the system with σ(0) = 0, σ(1) = σ(2) = 1. The main idea of this process is to eliminate the presence of the formal variable X by taking derivatives.

We start from the equation X + (1 + X 2 )σ + (1 + X + X 2 + X 3 )σ 2 = 0 which can be rewritten as σ + σ 2 + X(1 + σ 2 ) + X 2 (σ + σ 2 ) + X 3 σ 2 = 0 and, taking derivatives on both sides, we now obtain (5)

σ + (σ 2 ) + 1 + σ 2 + X(σ + σ 2 ) + X 2 σ 2 = 0 Because (σ 2 ) = σ • σ + σ(0) • σ = σ • σ + 0 • σ = σ • σ,
Now, because (1 + σ)(0) = 1(0) + σ(0) = 1 + 0 = 1 (and, in the Boolean field, 1 has an inverse, namely 1), the inverse (1 + σ) -1 is well-defined, and, multiplying both sides from (5) by this inverse we obtain σ =

(1 + σ)(σ + σ ) + σ 2 1 + σ

= (1 + σ)(σ + σ ) 1 + σ + σ 2 1 + σ = σ + σ + σ 2 1 + σ
This equation can be turned into a system of behavioural differential equations, by letting the variables x, y, z, w represent the streams σ, σ , σ and (1 + σ) -1 respectively:

x(0) = 0 x = y y(0) = 1 y = z z(0) = 1 z = z + y + x 2 w w(0) = 1 w = yw Of these equations, the equations for w need some clarification: the inverse τ -1 of a stream τ is defined as (τ -1 )(0) = (τ (0)) -1 (τ -1 ) = -τ (0) -1 • (τ • τ -1 )

Fig. 1 .

 1 Fig. 1. An overview of the main equivalences

(

  with [o(σ)] = (o(σ), 0, 0, 0, . . .), i.e. the solution of the equation o([o(σ)]) = o(σ) and [o(σ)] a = [0]) uniquely determine the operation of convolution product.

-

  r.t. solutions to S-algebraic systems are presented: Every proper S-algebraic system has exactly one strong solution [PS09, Theorem 3.2]. -Every Boolean B-algebraic system (not necessarily proper) has a strong solution [PS09, Theorem 4]. -Any component of a strong solution to a proper S-algebraic system also occurs as a component of a strong solution to such a system in Greibach normal form [PS09, Theorem 3.2].

  Thue-Morse sequence. In[START_REF] Allouche | Automatic Sequences -Theory, Applications, Generalizations[END_REF], a large amount of information and results related to automatic sequences can be found.It turns out that these k-automatic sequences, for prime numbers k, are exactly the IF k -algebraic streams:Theorem 11. For any prime p, a sequence is p-automatic iff it is IF p -algebraic.Proof. See [BR11, Theorem 4.1].

u

  Now we claim the following: for each t ∈ (A + X) * and w ∈ A * , the weight o(t w ) of the w-derivative of t is equal to the number of distinct leftmost derivations t ⇒ * w.

  By induction on n.

  w ) = a∈A w:|w|=n-1 o((x a ) w )

  this equation can be rewritten asσ + σ • σ + 1 + σ 2 + X(σ + σ 2 ) + X 2 σ 2 = 0 (2)Taking derivatives from (2) another time, we obtainσ + (σ • σ) + (σ 2 ) + σ + σ 2 + Xσ 2 = 0from which, using the earlier simplification of (σ 2 ) , and the equality (σ• σ) = σ • σ + σ (0) • σ = σ • σ + σ(1) • σ = σ • σ + σ , we obtain σ + (σ • σ + σ ) + σ • σ + σ + σ 2 + Xσ 2 = 0 (3)Taking derivatives from (3) yet another time, we obtainσ + (σ • σ) + σ + (σ • σ) + σ + (σ 2 ) + σ 2 = 0which can be simplified, using the earlier equalities and (σ• σ) = σ • σ + σ(2) • σ = σ • σ + σ , to σ + (σ • σ + σ ) + σ + (σ • σ + σ ) + σ + σ • σ + σ 2 = 0. (4)From (4), we can cancel out two of the three occurrences of the term σ , givingσ + σ • σ + σ + σ • σ + σ + σ • σ + σ 2 = 0which, using the laws of distribution, can be simplified to(1 + σ)(σ ) + (1 + σ)(σ + σ ) + σ 2 = 0 which (because in the Boolean field a + b = 0 implies a = b) is equivalent to (1 + σ)(σ ) = (1 + σ)(σ + σ ) + σ 2 .

  1. t = a • t . Then the number of distinct leftmost derivations t ⇒ * w is equal to the number of distinct leftmost derivations t ⇒ * w . But also o(t w ) = o((a • t ) a•w ) = o(t w ). Now apply the inductive hypothesis. 2. t = b • t with b = a. Then the number of distinct derivations t ⇒ * w is zero, and the same holds for o(t w ). 3. t = x • t . Then the number of distinct leftmost derivations x • t ⇒ * a • w is equal to

v:x→av

Supported by the Dutch NWO project CoRE: Coinductive Calculi for Regular Expressions.

We now have

confirming that w(0) = 1 and w = yw are indeed the appropriate equations for w.