Search

We are interested in connections between the theory of fractal sets obtained as attractors of iterated function systems and process calculi. To this end, we reinterpret Milner's expressions for processes as contraction operators on a complete metric space. When the space is, for example, the plane, the denotations of fixed point terms correspond to familiar fractal sets. We give a sound and complete axiomatization of fractal equivalence, the congruence on terms consisting of pairs that construct identical self-similar sets in all interpretations. We further make connections to labelled Markov chains and to invariant measures. In all of this work, we use important results from process calculi. For example, we use Rabinovich's completeness theorem for trace equivalence in our own completeness theorem. In addition to our results, we also raise many questions related to both fractals and process calculi.

The Vietoris space of compact subsets of a given Hausdorff space yields an endofunctor $\mathscr V$ on the category of Hausdorff spaces. Vietoris polynomial endofunctors on that category are built from $\mathscr V$, the identity and constant functors by forming products, coproducts and compositions. These functors are known to have terminal coalgebras and we deduce that they also have initial algebras. We present an analogous class of endofunctors on the category of extended metric spaces, using in lieu of $\mathscr V$ the Hausdorff functor $\mathcal H$. We prove that the ensuing Hausdorff polynomial functors have terminal coalgebras and initial algebras. Whereas the canonical constructions of terminal coalgebras for Vietoris polynomial functors takes $\omega$ steps, one needs $\omega + \omega$ steps in general for Hausdorff ones. We also give a new proof that the closed set functor on metric spaces has no fixed points.

We consider dynamic versions of epistemic logic as formulated in Baltag and Moss "Logics for epistemic programs" (2004). That paper proposed a logical language (actually families of languages parameterized by action signatures) for dynamic epistemic logic. It had been shown that validity in the language is Pi-1-1-complete, so there are no recursively axiomatized complete logical systems for it. In contrast, this paper proves a weak completeness result for the fragment without action iteration, and a strong completeness result for the fragment without action iteration and common knowledge. Our work involves a detour into term rewriting theory. The argument uses modal filtration, and thus we obtain the finite model property and hence decidability. We also give a translation of our largest language into PDL, thereby obtaining a second proof of decidability. The paper closes with some results on expressive power. These are mostly concerned with comparing the action-iteration-free language with modal logic augmented by transitive closure operators. We answer a natural question about the languages we obtain by varying the action signature: we prove that a logical language with operators for private announcements is more expressive than one for public announcements., This paper was intended to be the "journal" version of our 1998 paper "The logic of common knowledge, public announcements,and private suspicions." It was mainly written in 2004, with a few bibliographic additions coming a few years later

This paper obtains a completeness result for inequational reasoning with applicative terms without variables in a setting where the intended semantic models are the full structures, the full type hierarchies over preorders for the base types. The syntax allows for the specification that a given symbol be interpreted as a monotone function, or an antitone function, or both. There is a natural set of five rules for inequational reasoning. One can add variables and also add a substitution rule, but we observe that this logic would be incomplete for full structures. This is why the completeness result in this paper pertains to terms without variables. Since the completeness is already known for the class of general (Henkin) structures, we are interested in full structures. We present a completeness theorem. Our result is not optimal because we restrict to base preorders which have a weak completeness property: every pair of elements has an upper bound and a lower bound. To compensate we add several rules to the logic. We also present extensions and variations of our completeness result., 23 pages

This paper studies presentations of the Sierpinski gasket as a final coalgebra for functors on several categories of metric spaces with additional designated points. The three categories which we study differ on their morphisms: one uses short (non-expanding) maps, a second uses Lipschitz maps, and a third uses continuous maps. The functor in all cases is very similar to what we find in the standard presentation of the gasket as an attractor. We prove that the Sierpinski gasket itself is the final coalgebra of a naturally-occurring functor in the continuous setting. In the short setting, the final coalgebra exists but it is better described as the completion of the initial algebra, and this is not isomorphic to the Sierpinski gasket. In the Lipschitz setting, the final coalgebra does not exist. We determine the initial algebras in all three settings as well., 21 pages

The Initial Algebra Theorem by Trnkov�� et al. states, under mild assumptions, that an endofunctor has an initial algebra provided it has a pre-fixed point. The proof crucially depends on transfinitely iterating the functor and in fact shows that, equivalently, the (transfinite) initial-algebra chain stops. We give a constructive proof of the Initial Algebra Theorem that avoids transfinite iteration of the functor. For a given pre-fixed point A of the functor, it uses Pataraia���s theorem to obtain the least fixed point of a monotone function on the partial order formed by all subobjects of A. Thanks to properties of recursive coalgebras, this least fixed point yields an initial algebra. We obtain new results on fixed points and initial algebras in categories enriched over directed-complete partial orders, again without iteration. Using transfinite iteration we equivalently obtain convergence of the initial-algebra chain as an equivalent condition, overall yielding a streamlined version of the original proof., LIPIcs, Vol. 211, 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021), pages 5:1-5:20

This paper studies Markov decision processes (MDPs) from the categorical perspective of coalgebra and algebra. Probabilistic systems, similar to MDPs but without rewards, have been extensively studied, also coalgebraically, from the perspective of program semantics. In this paper, we focus on the role of MDPs as models in optimal planning, where the reward structure is central. The main contributions of this paper are (i) to give a coinductive explanation of policy improvement using a new proof principle, based on Banach’s Fixpoint Theorem, that we call contraction coinduction, and (ii) to show that the long-term value function of a policy with respect to discounted sums can be obtained via a generalized notion of corecursive algebra, which is designed to take boundedness into account. We also explore boundedness features of the Kantorovich lifting of the distribution monad to metric spaces.

Front Matter, Table of Contents, Preface, List of Authors

LIPIcs, Volume 35, CALCO'15, Complete Volume, LIPIcs, Vol. 35, 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015), pages 0-0

We study finite state transduction of automatic and morphic sequences. Dekking proved that morphic sequences are closed under transduction and in particular morphic images. We present a simple proof of this fact, and use the construction in the proof to show that non-erasing transductions preserve a condition called alpha-substitutivity. Roughly, a sequence is alpha-substitutive if the sequence can be obtained as the limit of iterating a substitution with dominant eigenvalue alpha. Our results culminate in the following fact: for multiplicatively independent real numbers alpha and beta, if v is an alpha-substitutive sequence and w is a beta-substitutive sequence, then v and w have no common non-erasing transducts except for the ultimately periodic sequences. We rely on Cobham's theorem for substitutions, a recent result of Durand.

The final coalgebra for the finite power-set functor was described by Worrell who also proved that the final chain converges in ω+ω steps. We describe the step ω as the set of saturated trees, a concept equivalent to the modally saturated trees introduced by K. Fine in the 1970s in his study of modal logic. And for the bounded power-set functors P_λ, where λ is an infinite regular cardinal, we prove that the construction needs precisely λ+ω steps. We also generalize Worrell’s result to M-labeled trees for a commutative monoid M, yielding a final coalgebra for the corresponding functor ℳ_f studied by H.-P. Gumm and T. Schröder. We describe the final chain of the power-set functor by introducing the concept of i-saturated tree for all ordinals i, and then prove that for i of cofinality ω, the i-th step in the final chain consists of all i-saturated, strongly extensional trees.

We combine ideas coming from several fields, including modal logic, coalgebra, and set theory. Modally saturated trees were introduced by K. Fine in 1975. We give a new purely combinatorial formulation of modally saturated trees, and we prove that they form the limit of the final omega-op-chain of the finite power-set functor Pf. From that, we derive an alternative proof of J. Worrell's description of the final coalgebra as the coalgebra of all strongly extensional, finitely branching trees. In the other direction, we represent the final coalgebra for Pf in terms of certain maximal consistent sets in the modal logic K. We also generalize Worrell's result to M-labeled trees for a commutative monoid M, yielding a final coalgebra for the corresponding functor Mf studied by H. P. Gumm and T. Schröder. We introduce the concept of an i-saturated tree for all ordinals i, and then prove that the i-th step in the final chain of the power set functor consists of all i-saturated trees. This leads to a new description of the final coalgebra for the restricted power-set functors Plambda (of subsets of cardinality smaller than lambda).

This paper provides a general account of the notion of recursive program schemes, studying both uninterpreted and interpreted solutions. It can be regarded as the category-theoretic version of the classical area of algebraic semantics. The overall assumptions needed are small indeed: working only in categories with "enough final coalgebras" we show how to formulate, solve, and study recursive program schemes. Our general theory is algebraic and so avoids using ordered, or metric structures. Our work generalizes the previous approaches which do use this extra structure by isolating the key concepts needed to study substitution in infinite trees, including second-order substitution. As special cases of our interpreted solutions we obtain the usual denotational semantics using complete partial orders, and the one using complete metric spaces. Our theory also encompasses implicitly defined objects which are not usually taken to be related to recursive program schemes. For example, the classical Cantor two-thirds set falls out as an interpreted solution (in our sense) of a recursive program scheme., this version includes the corrections from the corrigendum in Theoret. Comput. Sci. 403 (2008), 409-415