共查询到20条相似文献,搜索用时 15 毫秒
1.
Philip Wadler 《LISP and Symbolic Computation》1994,7(1):39-55
Moggi's use of monads to factor semantics is used to model the composable continuations of Danvy and Filinski. This yields some insights into the type systems proposed by Murthy and by Danvy and Filinski. Interestingly, modelling some aspects of composable continuations requires a structure that is almost, but not quite, a monad. 相似文献
2.
3.
[4] describes a modal logic for coalgebras of certain polynomial endofunctors on Set. This logic is here generalised to endofunctors on categories of sorted sets. The structure of the endofunctors considered is then exploited in order to define ways of moving from (coalgebras of) one endofunctor to (coalgebras of) another, and to equip them with translations between the associated modal languages. Furthermore, the resulting translations are shown to preserve and reflect the satisfaction of modal formulae by coalgebras. 相似文献
4.
Alessandra Palmigiano 《Electronic Notes in Theoretical Computer Science》2003,82(1):221-236
Positive Modal Logic is the restriction of the modal local consequence relation defined by the class of all Kripke models to the propositional negation-free modal language. The class of positive modal algebras is the one canonically associated with PML according to the theory of the algebraization of logics. In [4], a Priestley-style duality is established between the category of positive modal algebras and the category of K+-spaces. In this paper, we establish a categorical equivalence between the category K+ of K+-spaces and the category Coalg(V) of coalgebras of a suitable endofunctor V on the category of Priestley spaces. 相似文献
5.
基于组件的软件开发能够有效提高软件开发的质量与效率.但在一些安全关键的领域,由于形式化模型与方法的缺乏,使得基于组件的开发方法不能成功应用.为了得到一套完整的形式化模型用于描述软件组件及其组成的系统,首先必须对软件组件的形式化语意进行定义.文中提出了一种基于共代数概念的语意,使得满足接口和组件规约的组件对应于一个具体的共代数,并由此推导出了接口和组件的功能契约的形式语意以及接口依赖的共代数语意.通过对一个简单的堆栈进行规约,体现了这种方法的可应用性. 相似文献
6.
《Information and Computation》2006,204(4):588-609
We give a coalgebraic formulation of timed processes and their operational semantics. We model time by a monoid called a “time domain”, and we model processes by “timed transition systems”, which amount to partial monoid actions of the time domain or, equivalently, coalgebras for an “evolution comonad” generated by the time domain. All our examples of time domains satisfy a partial closure property, yielding a distributive law of a monad for total monoid actions over the evolution comonad, and hence a distributive law of the evolution comonad over a dual comonad for total monoid actions. We show that the induced coalgebras are exactly timed transition systems with delay operators. We then integrate our coalgebraic formulation of time qua timed transition systems into Turi and Plotkin’s formulation of structural operational semantics in terms of distributive laws. We combine timing with action via the more general study of the combination of two arbitrary sorts of behaviour whose operational semantics may interact. We give a modular account of the operational semantics for a combination induced by that of each of its components. Our study necessitates the investigation of products of comonads. In particular, we characterise when a monad lifts to the category of coalgebras for a product comonad, providing constructions with which one can readily calculate. 相似文献
7.
The bisimulation “up-to-…” technique provides an effective way to relieve the amount of work in proving bisimilarity of two processes. This paper develops a fresh and direct approach to generalize this set-theoretic “up-to-...” principle to the setting of coalgebra theory. The notion of consistent function is introduced, as a generalization of Sangiorgi's sound function. Then, in order to prove that there are only bisimilar pairs in a relation, it is sufficient to find a morphism from it to the “lifting” of its image under some consistent function. One example is given showing that every self-bisimulation in normed BPA is just such a relation. What's more, we investigate the connection between span-bisimulation and ref-bisimulation. As a result, λ-bisimulation turns out to be covered by our new principle. 相似文献
8.
This paper gives a fresh look at my previous work on “epistemic actions” and information updates in distributed systems, from a coalgebraic perspective. I show that the “relational” semantics of epistemic programs, given in [BMS2] in terms of epistemic updates, can be understood in terms of functors on the category of coalgebras and natural transformations associated to them. Then, I introduce a new, alternative, more refined semantics for epistemic programs: programs as “epistemic coalgebras”. I argue for the advantages of this second semantics, from a semantic, heuristic, syntactical and proof-theoretic point of view. Finally, as a step towards a generalization, I show these concepts make sense for other functors, and that apparently unrelated concepts, such as Bayesian belief updates and process transformations, can be seen to arise in the same way as our “epistemic actions”. 相似文献
9.
Furio Honsell Marina Lenisa Rekha Redamalla 《Electronic Notes in Theoretical Computer Science》2006,135(3):73
We extend the Reichel-Jacobs coalgebraic account of specification and refinement of objects and classes in Object Oriented Programming to (generalized) binary methods. These are methods that take more than one parameter of a class type. Class types include sums and (possibly infinite) products type constructors. We study and compare two solutions for modeling generalized binary methods, which use purely covariant functors. In the first solution, which applies when we already have a class implementation, we reduce the behaviour of a generalized binary method to that of a bunch of unary methods. These are obtained by freezing the types of the extra class parameters to constant types. The bisimulation behavioural equivalence induced on objects by this model amounts to the greatest congruence w.r.t method application. Alternatively, we treat binary methods as graphs instead of functions, thus turning contravariant occurrences in the functor into covariant ones. 相似文献
10.
This paper relates labelled transition systems and coalgebras with the motivation of comparing and combining their complementary contributions to the theory of concurrent systems. The well-known mismatch between these two notions concerning the morphisms is resolved by extending the coalgebraic framework by lax cohomomorphisms.
Enriching both labelled transition systems and coalgebras with algebraic structure for an algebraic specification, the correspondence is lost again. This motivates the introduction of lax coalgebras, where the coalgebra structure is given by a lax homomorphism. The resulting category of lax coalgebras and lax cohomomorphisms for a suitable endofunctor is shown to be isomorphic to the category of structured transition systems, where both states and transitions form algebras.
The framework is also presented on a more abstract categorical level using monads and comonads, extending the bialgebraic approach introduced by Turi and Plotkin. 相似文献
11.
Coalgebraic theories of sequences in PVS 总被引:1,自引:0,他引:1
12.
13.
Kleene Algebra with Tests is an extension of Kleene Algebra, the algebra of regular expressions, which can be used to reason about programs. We develop a coalgebraic theory of Kleene Algebra with Tests, along the lines of the coalgebraic theory of regular expressions based on deterministic automata. Since the known automata-theoretic presentation of Kleene Algebra with Tests does not lend itself to a coalgebraic theory, we define a new interpretation of Kleene Algebra with Tests expressions and a corresponding automata-theoretic presentation. One outcome of the theory is a coinductive proof principle, that can be used to establish equivalence of our Kleene Algebra with Tests expressions. 相似文献
14.
The algebra of infinite trees is, as proved by C. Elgot, completely iterative, i.e., all ideal recursive equations are uniquely solvable. This is proved here to be a general coalgebraic phenomenon: let H be an endofunctor such that for every object X a final coalgebra, TX, of H(_) + X exists. Then TX is an object-part of a monad which is completely iterative. Moreover, a similar contruction of a “completely iterative monoid” is possible in every monoidal category satisfying mild side conditions. 相似文献
15.
16.
Neil Ghani Christoph Lüth Federico de Marchi John Power 《Electronic Notes in Theoretical Computer Science》2001,44(1)
Whilst the relationship between initial algebras and monads is well-understood, the relationship between final coalgebras and comonads is less well explored. This paper shows that the problem is more subtle and that final coalgebras can just as easily form monads as comonads and dually, that initial algebras form both monads and comonads.In developing these theories we strive to provide them with an associated notion of syntax. In the case of initial algebras and monads this corresponds to the standard notion of algebraic theories consisting of signatures and equations: models of such algebraic theories are precisely the algebras of the representing monad. We attempt to emulate this result for the coalgebraic case by defining a notion cosignature and coequation and then proving the models of this syntax are precisely the coalgebras of the representing comonad. 相似文献
17.
18.
Hiroshi Watanabe Koki Nishizawa Osamu Takaki 《Electronic Notes in Theoretical Computer Science》2006,164(1):177-194
The Cone of Influence Reduction is a fundamental abstraction technique for reducing the size of models used in symbolic model checking. We develop coalgebraic representations of systems as composites of state transition maps and connectors. These representations include synchronous systems, asynchronous systems, asynchronous systems with synchronization by channels, and those with shared variables, probabilistic synchronous systems and so on. We schematically show the cone of influence reduction using these coalgebraic representations, which give a unified framework for providing the technique for various kinds of systems. 相似文献
19.
Coalgebras can be seen as a natural abstraction of Kripke frames. In the same sense, coalgebraic logics are generalised modal logics. In this paper, we give an overview of the basic tools, techniques and results that connect coalgebras and modal logic. We argue that coalgebras unify the semantics of a large range of different modal logics (such as probabilistic, graded, relational, conditional) and discuss unifying approaches to reasoning at this level of generality. We review languages defined in terms of the so-called cover modality, languages induced by predicate liftings as well as their common categorical abstraction, and present (abstract) results on completeness, expressiveness and complexity in these settings, both for basic languages as well as a number of extensions, such as hybrid languages and fixpoints. 相似文献