Iterative theories, which were introduced by Calvin Elgot, formalise potentially infinite computations as unique solutions of recursive equations. One the main results Elgot and his coauthors is a description free iterative theory all rational trees. Their algebraic proof this fact extremely complicated. In our paper we show that starting with 'iterative algebras', is, algebras admitting solution systems flat equations, obtained algebras. The (coalgebraic) present dramatically simpler than...

Stream circuits are a convenient graphical way to represent streams (or stream functions) computed by finite dimensional linear systems. We present sound and complete expression calculus that allows us reason about the semantic equivalence of closed circuits. For our proof soundness completeness we build on recent ideas Bonsangue, Rutten Silva. They have provided "Kleene theorem'' for coalgebras endofunctors category sets. The key ingredient is syntactic characterization final locally...

Coalgebras provide a uniform framework to study dynamical systems, including several types of automata. In this paper, we make use the coalgebraic view on systems investigate, in way, under which conditions calculi that are sound and complete with respect behavioral equivalence can be extended coarser language equivalence, arises from generalised powerset construction determinises coalgebras. We show soundness completeness established by proving expressions modulo axioms calculus form...

Denotational semantics can be based on algebras with additional structure (order, metric, etc.) which makes it possible to interpret recursive specifications. It was the idea of Elgot base denotational iterative theories instead, i.e., in abstract specifications are required have unique solutions. Later Bloom and Esik studied iteration a specified solution has obey certain axioms. We propose so-called as convenient for present paper. An algebra is an every system flat equations. That...

Models of concurrent systems employ a wide variety semantics inducing various notions process equivalence, ranging from linear-time such as trace equivalence to branching-time strong bisimilarity. Many these generalize system types beyond standard transition systems, featuring, for example, weighted, probabilistic, or game-based transitions; this motivates the search suitable coalgebraic abstractions that cover orthogonal dimensions generality, i.e. are generic both in type and notion...

Compositionality proofs in higher-order languages are notoriously involved, and general semantic frameworks guaranteeing compositionality hard to come by. In particular, Turi Plotkin’s bialgebraic abstract GSOS framework, which has been successfully applied obtain off-the-shelf results for first-order languages, so far does not apply languages. the present work, we develop a theory of specifications effect transferring core principles framework setting. our theory, operational semantics is...

Automata over infinite alphabets have emerged as a convenient computational model for processing structures involving data, such nonces in cryptographic protocols or data values XML documents. We introduce active learning methods bar automata, species of automata that process finite words represented strings, which are with explicit name binding letters. Bar pleasant algorithmic properties. develop framework every algorithm standard deterministic nondeterministic can be used to learn query...

Bloom and Ésik's concept of iteration theory summarises all equational properties that has in common applications, for example, domain theory, where to every system recursive equations, the least solution is assigned. This paper shows coalgebraic approach iteration, more appropriate a functorial (called Elgot theory). These theories have particularly simple axiomatisation, well-known examples are functorial. proved be monadic over category sets context (or, generally, finitary endofunctors...

For endofunctors of varieties preserving intersections, a new description the final coalgebra and initial algebra is presented: former consists all well-pointed coalgebras. These are pointed coalgebras having no proper subobject quotient. The that well-founded in sense Osius Taylor. And algebras precisely Finally, iterative finite Numerous examples discussed e.g. automata, graphs, labeled transition systems.

Eilenberg's variety theorem, a centerpiece of algebraic automata theory, establishes bijective correspondence between varieties languages and pseudovarieties monoids. In the present paper this result is generalized to an abstract pair categories: we introduce in category C, prove that they correspond monoids closed monoidal D, provided C D are dual on level finite objects. By suitable choices these categories our uniformly covers theorem three variants due Pin, Polák Reutenauer,...

Higher-order abstract GSOS is a recent extension of Turi and Plotkin's framework Mathematical Operational Semantics to higher-order languages. The fundamental well-behavedness property all specifications within the that coalgebraic strong (bi)similarity on their operational model congruence. In present work, we establish corresponding congruence theorem for weak similarity, which shown instantiate well-known concepts such as Abramsky's applicative similarity λ-calculus. On way, develop...

Every finitary endofunctor of $\Set$ is proved to generate a free iterative theory in the sense Elgot. This work based on coalgebras, specifically parametric corecursion, and proof presented for categories more general than just $\Set$.

For finitary set functors preserving inverse images, recursive coalgebras A of Paul Taylor are proved to be precisely those for which the system described by always halts in finitely many steps.

Terminal coalgebras for a functor serve as semantic domains state-based systems of various types. For example, behaviors CCS processes, streams, infinite trees, formal languages and non-well-founded sets form terminal coalgebras. We present uniform account the semantics recursive definitions in by combining two ideas: (1) abstract GSOS rules l specify additional algebraic operations on coalgebra; (2) are also initial completely iterative algebras (cias). show that an rule leads to new...

Logical relations constitute a key method for reasoning about contextual equivalence of programs in higher-order languages.They are usually developed on per-case basis, with new theory required each variation the language or desired notion equivalence.In present paper we introduce general construction (step-indexed) logical at level Higher-Order Mathematical Operational Semantics, highly parametric categorical framework modeling operational semantics higherorder languages.Our main result...