eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2015-10-28
35
0
0
10.4230/LIPIcs.CALCO.2015
article
LIPIcs, Volume 35, CALCO'15, Complete Volume
Moss, Lawrence S.
Sobocinski, Pawel
LIPIcs, Volume 35, CALCO'15, Complete Volume
https://drops.dagstuhl.de/storage/00lipics/lipics-vol035-calco2015/LIPIcs.CALCO.2015/LIPIcs.CALCO.2015.pdf
Theory of Computation, Logics and Meanings of Programs, Semantics of Programming Languages
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2015-10-28
35
i
xii
10.4230/LIPIcs.CALCO.2015.i
article
Front Matter, Table of Contents, Preface, List of Authors
Moss, Lawrence S.
Sobocinski, Pawel
Front Matter, Table of Contents, Preface, List of Authors
https://drops.dagstuhl.de/storage/00lipics/lipics-vol035-calco2015/LIPIcs.CALCO.2015.i/LIPIcs.CALCO.2015.i.pdf
Front Matter
Table of Contents
Preface
List of Authors
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2015-10-28
35
1
16
10.4230/LIPIcs.CALCO.2015.1
article
Syntactic Monoids in a Category
Adamek, Jiri
Milius, Stefan
Urbat, Henning
The syntactic monoid of a language is generalized to the level of a symmetric monoidal closed category D. This allows for a uniform treatment of several notions of syntactic algebras known in the literature, including the syntactic monoids of Rabin and Scott (D = sets), the syntactic semirings of Polák (D = semilattices), and the syntactic associative algebras of Reutenauer (D = vector spaces). Assuming that D is a commutative variety of algebras, we prove that the syntactic D-monoid of a language L can be constructed as a quotient of a free D-monoid modulo the syntactic congruence of L, and that it is isomorphic to the transition D-monoid of the minimal automaton for L in D. Furthermore, in the case where the variety D is locally finite, we characterize the regular languages as precisely the languages with finite syntactic D-monoids.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol035-calco2015/LIPIcs.CALCO.2015.1/LIPIcs.CALCO.2015.1.pdf
Syntactic monoid
transition monoid
algebraic automata theory
duality
coalgebra
algebra
symmetric monoidal closed category
commutative variety
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2015-10-28
35
17
34
10.4230/LIPIcs.CALCO.2015.17
article
Extensions of Functors From Set to V-cat
Balan, Adriana
Kurz, Alexander
Velebil, Jiri
We show that for a commutative quantale V every functor from Set to V-cat has an enriched left-Kan extension. As a consequence, coalgebras over Set are subsumed by coalgebras over V-cat. Moreover, one can build functors on V-cat by equipping Set-functors with a metric.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol035-calco2015/LIPIcs.CALCO.2015.17/LIPIcs.CALCO.2015.17.pdf
enriched category
quantale
final coalgebra
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2015-10-28
35
35
49
10.4230/LIPIcs.CALCO.2015.35
article
Towards Trace Metrics via Functor Lifting
Baldan, Paolo
Bonchi, Filippo
Kerstan, Henning
König, Barbara
We investigate the possibility of deriving metric trace semantics in a coalgebraic framework. First, we generalize a technique for systematically lifting functors from the category Set of sets to the category PMet of pseudometric spaces, by identifying conditions under which also natural transformations, monads and distributive laws can be lifted. By exploiting some recent work on an abstract determinization, these results enable the derivation of trace metrics starting from coalgebras in Set. More precisely, for a coalgebra in Set we determinize it, thus obtaining a coalgebra in the Eilenberg-Moore category of a monad. When the monad can be lifted to PMet, we can equip the final coalgebra with a behavioral distance. The trace distance between two states of the original coalgebra is the distance between their images in the determinized coalgebra through the unit of the monad. We show how our framework applies to nondeterministic automata and probabilistic automata.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol035-calco2015/LIPIcs.CALCO.2015.35/LIPIcs.CALCO.2015.35.pdf
trace metric
monad lifting
pseudometric
coalgebra
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2015-10-28
35
50
65
10.4230/LIPIcs.CALCO.2015.50
article
A Fibrational Approach to Automata Theory
Chen, Liang-Ting
Urbat, Henning
For predual categories C and D we establish isomorphisms between opfibrations representing local varieties of languages in C, local pseudovarieties of D-monoids, and finitely generated profinite D-monoids. The global sections of these opfibrations are shown to correspond to varieties of languages in C, pseudovarieties of D-monoids, and profinite equational theories of D-monoids, respectively. As an application, a new proof of Eilenberg's variety theorem along with several related results is obtained, covering uniformly varieties of languages and their coalgebraic modifications, Straubing's C-varieties, and fully invariant local varieties.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol035-calco2015/LIPIcs.CALCO.2015.50/LIPIcs.CALCO.2015.50.pdf
Eilenberg’s variety theorem
duality
coalgebra
Grothendieck fibration
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2015-10-28
35
66
85
10.4230/LIPIcs.CALCO.2015.66
article
Canonical Coalgebraic Linear Time Logics
Cirstea, Corina
We extend earlier work on linear time fixpoint logics for coalgebras with branching, by showing how propositional operators arising from the choice of branching monad can be canonically added to these logics. We then consider two semantics for the uniform modal fragments of such logics: the previously-proposed, step-wise semantics and a new semantics akin to those of path-based logics. We prove that the two semantics are equivalent, and show that the canonical choice made for resolving branching in these logics is crucial for this property. We also state conditions under which similar, non-canonical logics enjoy the same property - this applies both to the choice of a branching modality and to the choice of linear time modalities. Our logics allow reasoning about linear time behaviour in systems with non-deterministic, probabilistic or weighted branching. In all these cases, the logics enhanced with propositional operators gain in expressiveness. Another contribution of our work is a reformulation of fixpoint semantics, which applies to any coalgebraic modal logic whose semantics arises from a one-step semantics.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol035-calco2015/LIPIcs.CALCO.2015.66/LIPIcs.CALCO.2015.66.pdf
coalgebra
linear time logic
fixpoint logic
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2015-10-28
35
86
100
10.4230/LIPIcs.CALCO.2015.86
article
An Intensionally Fully-abstract Sheaf Model for pi
Eberhart, Clovis
Hirschowitz, Tom
Seiller, Thomas
Following previous work on CCS, we propose a compositional model for the pi-calculus in which processes are interpreted as sheaves on certain simple sites. We define an analogue of fair testing equivalence in the model and show that our interpretation is intensionally fully abstract for it. That is, the interpretation preserves and reflects fair testing equivalence; and furthermore, any strategy is fair testing equivalent to the interpretation of some process. The central part of our work is the construction of our sites, whose heart is a combinatorial presentation of pi-calculus traces in the spirit of string diagrams. As in previous work, the sheaf condition is analogous to innocence in Hyland-Ong/Nickau games.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol035-calco2015/LIPIcs.CALCO.2015.86/LIPIcs.CALCO.2015.86.pdf
concurrency
sheaves
causal models
games
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2015-10-28
35
101
115
10.4230/LIPIcs.CALCO.2015.101
article
Partial Higher-dimensional Automata
Fahrenberg, Uli
Legay, Axel
We propose a generalization of higher-dimensional automata, partial HDA. Unlike HDA, and also extending event structures and Petri nets, partial HDA can model phenomena such as priorities or the disabling of an event by another event. Using open maps and unfoldings, we introduce a natural notion of (higher-dimensional) bisimilarity for partial HDA and relate it to history-preserving bisimilarity and split bisimilarity. Higher-dimensional bisimilarity has a game characterization and is decidable in polynomial time.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol035-calco2015/LIPIcs.CALCO.2015.101/LIPIcs.CALCO.2015.101.pdf
higher-dimensional automata
bisimulation
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2015-10-28
35
116
129
10.4230/LIPIcs.CALCO.2015.116
article
A Recipe for State-and-Effect Triangles
Jacobs, Bart
In the semantics of programming languages one can view programs as state transformers, or as predicate transformers. Recently the author has introduced 'state-and-effect' triangles which captures this situation categorically, involving an adjunction between state- and predicate-transformers. The current paper exploits a classical result in category theory, part of Jon Beck's monadicity theorem, to systematically construct such a state-and-effect triangle from an adjunction. The power of this construction is illustrated in many examples, both for the Boolean and probabilistic (quantitative) case.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol035-calco2015/LIPIcs.CALCO.2015.116/LIPIcs.CALCO.2015.116.pdf
Duality
predicate transformer
state transformer
state-and-effect triangle
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2015-10-28
35
130
155
10.4230/LIPIcs.CALCO.2015.130
article
Towards Concept Analysis in Categories: Limit Inferior as Algebra, Limit Superior as Coalgebra
Kataoka, Toshiki
Pavlovic, Dusko
While computer programs and logical theories begin by declaring the concepts of interest, be it as data types or as predicates, network computation does not allow such global declarations, and requires concept mining and concept analysis to extract shared semantics for different network nodes. Powerful semantic analysis systems have been the drivers of nearly all paradigm shifts on the web. In categorical terms, most of them can be described as bicompletions of enriched matrices, generalizing the Dedekind-MacNeille-style completions from posets to suitably enriched categories. Yet it has been well known for more than 40 years that ordinary categories themselves in general do not permit such completions. Armed with this new semantical view of Dedekind-MacNeille completions, and of matrix bicompletions, we take another look at this ancient mystery. It turns out that simple categorical versions of the limit superior and limit inferior operations characterize a general notion of Dedekind-MacNeille completion, that seems to be appropriate for ordinary categories, and boils down to the more familiar enriched versions when the limits inferior and superior coincide. This explains away the apparent gap among the completions of ordinary categories, and broadens the path towards categorical concept mining and analysis, opened in previous work.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol035-calco2015/LIPIcs.CALCO.2015.130/LIPIcs.CALCO.2015.130.pdf
concept analysis
semantic indexing
category
completion
algebra
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2015-10-28
35
156
170
10.4230/LIPIcs.CALCO.2015.156
article
Codensity Liftings of Monads
Katsumata, Shin-ya
Sato, Tetsuya
We introduce a method to lift monads on the base category of a fibration to its total category using codensity monads. This method, called codensity lifting, is applicable to various fibrations which were not supported by the categorical >>-lifting. After introducing the codensity lifting, we illustrate some examples of codensity liftings of monads along the fibrations from the category of preorders, topological spaces and extended psuedometric spaces to the category of sets, and also the fibration from the category of binary relations between measurable spaces. We next study the liftings of algebraic operations to the codensity-lifted monads. We also give a characterisation of the class of liftings (along posetal fibrations with fibred small limits) as a limit of a certain large diagram.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol035-calco2015/LIPIcs.CALCO.2015.156/LIPIcs.CALCO.2015.156.pdf
Monads
Lifting
Fibration
Giry Monad
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2015-10-28
35
171
189
10.4230/LIPIcs.CALCO.2015.171
article
A First-order Logic for String Diagrams
Kissinger, Aleks
Quick, David
Equational reasoning with string diagrams provides an intuitive means of proving equations between morphisms in a symmetric monoidal category. This can be extended to proofs of infinite families of equations using a simple graphical syntax called !-box notation. While this does greatly increase the proving power of string diagrams, previous attempts to go beyond equational reasoning have been largely ad hoc, owing to the lack of a suitable logical framework for diagrammatic proofs involving !-boxes. In this paper, we extend equational reasoning with !-boxes to a fully-fledged first order logic with conjunction, implication, and universal quantification over !-boxes. This logic, called !L, is then rich enough to properly formalise an induction principle for !-boxes. We then build a standard model for !L and give an example proof of a theorem for non-commutative bialgebras using !L, which is unobtainable by equational reasoning alone.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol035-calco2015/LIPIcs.CALCO.2015.171/LIPIcs.CALCO.2015.171.pdf
string diagrams
compact closed monoidal categories
abstract tensor systems
first-order logic
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2015-10-28
35
190
204
10.4230/LIPIcs.CALCO.2015.190
article
Presenting Morphisms of Distributive Laws
Klin, Bartek
Nachyla, Beata
A format for well-behaved translations between structural operational specifications is derived from a notion of distributive law morphism, previously studied by Power and Watanabe.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol035-calco2015/LIPIcs.CALCO.2015.190/LIPIcs.CALCO.2015.190.pdf
coalgebra
bialgebra
distributive law
structural operational semantics
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2015-10-28
35
205
220
10.4230/LIPIcs.CALCO.2015.205
article
Approximation of Nested Fixpoints – A Coalgebraic View of Parametric Dataypes
Kurz, Alexander
Pardo, Alberto
Petrisan, Daniela
Severi, Paula
de Vries, Fer-Jan
The question addressed in this paper is how to correctly approximate infinite data given by systems of simultaneous corecursive definitions. We devise a categorical framework for reasoning about regular datatypes, that is, datatypes closed under products, coproducts and fixpoints. We argue that the right methodology is on one hand coalgebraic (to deal with possible nontermination and infinite data) and on the other hand 2-categorical (to deal with parameters in a disciplined manner). We prove a coalgebraic version of Bekic lemma that allows us to reduce simultaneous fixpoints to a single fix point. Thus a possibly infinite object of interest is regarded as a final coalgebra of a many-sorted polynomial functor and can be seen as a limit of finite approximants. As an application, we prove correctness of a generic function that calculates the approximants on a large class of data types.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol035-calco2015/LIPIcs.CALCO.2015.205/LIPIcs.CALCO.2015.205.pdf
coalgebra
Bekic lemma
infinite data
functional programming
type theory
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2015-10-28
35
221
237
10.4230/LIPIcs.CALCO.2015.221
article
Final Coalgebras from Corecursive Algebras
Levy, Paul Blain
We give a technique to construct a final coalgebra in which each element is a set of formulas of modal logic. The technique works for both the finite and the countable powerset functors. Starting with an injectively structured, corecursive algebra, we coinductively obtain a suitable subalgebra called the "co-founded part". We see—first with an example, and then in the general setting of modal logic on a dual adjunction—that modal theories form an injectively structured, corecursive algebra, so that this construction may be applied. We also obtain an initial algebra in a similar way.
We generalize the framework beyond Set to categories equipped with a suitable factorization system, and look at the examples of Poset and Set-op .
https://drops.dagstuhl.de/storage/00lipics/lipics-vol035-calco2015/LIPIcs.CALCO.2015.221/LIPIcs.CALCO.2015.221.pdf
coalgebra
modal logic
bisimulation
category theory
factorization system
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2015-10-28
35
238
252
10.4230/LIPIcs.CALCO.2015.238
article
Uniform Interpolation for Coalgebraic Fixpoint Logic
Marti, Johannes
Seifan, Fatemeh
Venema, Yde
We use the connection between automata and logic to prove that a wide class of coalgebraic fixpoint logics enjoys uniform interpolation. To this aim, first we generalize one of the central results in coalgebraic automata theory, namely closure under projection, which is known to hold for weak-pullback preserving functors, to a more general class of functors, i.e., functors with quasifunctorial lax extensions. Then we will show that closure under projection implies definability of the bisimulation quantifier in the language of coalgebraic fixpoint logic, and finally we prove the uniform interpolation theorem.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol035-calco2015/LIPIcs.CALCO.2015.238/LIPIcs.CALCO.2015.238.pdf
mu-calculus
uniform interpolation
coalgebra
automata
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2015-10-28
35
253
269
10.4230/LIPIcs.CALCO.2015.253
article
Generic Trace Semantics and Graded Monads
Milius, Stefan
Pattinson, Dirk
Schröder, Lutz
Models of concurrent systems employ a wide variety of semantics inducing various notions of process equivalence, ranging from linear-time semantics such as trace equivalence to branching-time semantics such as strong bisimilarity. Many of these generalize to system types beyond standard transition systems, featuring, for example, weighted, probabilistic, or game-based transitions; this motivates the search for suitable coalgebraic abstractions of process equivalence that cover these orthogonal dimensions of generality, i.e. are generic both in the system type and in the notion of system equivalence. In recent joint work with Kurz, we have proposed a parametrization of system equivalence over an embedding of the coalgebraic type functor into a monad. In the present paper, we refine this abstraction to use graded monads, which come with a notion of depth that corresponds, e.g., to trace length or bisimulation depth. We introduce a notion of graded algebras and show how they play the role of formulas in trace logics.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol035-calco2015/LIPIcs.CALCO.2015.253/LIPIcs.CALCO.2015.253.pdf
transition systems
monads
coalgebra
trace logics
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2015-10-28
35
270
289
10.4230/LIPIcs.CALCO.2015.270
article
Open System Categorical Quantum Semantics in Natural Language Processing
Piedeleu, Robin
Kartsaklis, Dimitri
Coecke, Bob
Sadrzadeh, Mehrnoosh
Originally inspired by categorical quantum mechanics (Abramsky and Coecke, LiCS'04), the categorical compositional distributional model of natural language meaning of Coecke, Sadrzadeh and Clark provides a conceptually motivated procedure to compute the meaning of a sentence, given its grammatical structure within a Lambek pregroup and a vectorial representation of the meaning of its parts. Moreover, just like CQM allows for varying the model in which we interpret quantum axioms, one can also vary the model in which we interpret word meaning.
In this paper we show that further developments in categorical quantum mechanics are relevant to natural language processing too. Firstly, Selinger's CPM-construction allows for explicitly taking into account lexical ambiguity and distinguishing between the two inherently different notions of homonymy and polysemy. In terms of the model in which we interpret word meaning, this means a passage from the vector space model to density matrices. Despite this change of model, standard empirical methods for comparing meanings can be easily adopted, which we demonstrate by a small-scale experiment on real-world data. Secondly, commutative classical structures as well as their non-commutative counterparts that arise in the image of the CPM-construction allow for encoding relative pronouns, verbs and adjectives, and finally, iteration of the CPM-construction, something that has no counterpart in the quantum realm, enables one to accommodate both entailment and ambiguity.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol035-calco2015/LIPIcs.CALCO.2015.270/LIPIcs.CALCO.2015.270.pdf
category theory
density matrices
distributional models
semantics
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2015-10-28
35
290
303
10.4230/LIPIcs.CALCO.2015.290
article
Modules Over Monads and Their Algebras
Pirog, Maciej
Wu, Nicolas
Gibbons, Jeremy
Modules over monads (or: actions of monads on endofunctors) are structures in which a monad interacts with an endofunctor, composed either on the left or on the right. Although usually not explicitly identified as such, modules appear in many contexts in programming and semantics. In this paper, we investigate the elementary theory of modules. In particular, we identify the monad freely generated by a right module as a generalisation of Moggi's resumption monad and characterise its algebras, extending previous results by Hyland, Plotkin and Power, and by Filinski and Stovring. Moreover, we discuss a connection between modules and algebraic effects: left modules have a similar feeling to Eilenberg–Moore algebras, and can be seen as handlers that are natural in the variables, while right modules can be seen as functions that run effectful computations in an appropriate context (such as an initial state for a stateful computation).
https://drops.dagstuhl.de/storage/00lipics/lipics-vol035-calco2015/LIPIcs.CALCO.2015.290/LIPIcs.CALCO.2015.290.pdf
monad
module over monad
algebraic data types
resumptions
free object
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2015-10-28
35
304
319
10.4230/LIPIcs.CALCO.2015.304
article
Revisiting the Institutional Approach to Herbrand’s Theorem
Tutu, Ionut
Fiadeiro, José Luiz
More than a decade has passed since Herbrand’s theorem was first generalized to arbitrary institutions, enabling in this way the development of the logic-programming paradigm over formalisms beyond the conventional framework of relational first-order logic. Despite the mild assumptions of the original theory, recent developments have shown that the institution-based approach cannot capture constructions that arise when service-oriented computing is presented as a form of logic programming, thus prompting the need for a new perspective on Herbrand’s theorem founded instead upon a concept of generalized substitution system. In this paper, we formalize the connection between the institution- and the substitution-system-based approach to logic programming by investigating a number of features of institutions, like the existence of a quantification space or of representable substitutions, under which they give rise to suitable generalized substitution systems. Building on these results, we further show how the original institution independent versions of Herbrand’s theorem can be obtained as concrete instances of a more general result.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol035-calco2015/LIPIcs.CALCO.2015.304/LIPIcs.CALCO.2015.304.pdf
Institution theory
Substitution systems
Herbrand’s theorem
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2015-10-28
35
320
335
10.4230/LIPIcs.CALCO.2015.320
article
Coalgebraic Infinite Traces and Kleisli Simulations
Urabe, Natsuki
Hasuo, Ichiro
Kleisli simulation is a categorical notion introduced by Hasuo to verify finite trace inclusion. They allow us to give definitions of forward and backward simulation for various types of systems. A generic categorical theory behind Kleisli simulation has been developed and it guarantees the soundness of those simulations wrt. finite trace semantics. Moreover, those simulations can be aided by forward partial execution (FPE) - a categorical transformation of systems previously introduced by the authors.
In this paper, we give Kleisli simulation a theoretical foundation that assures its soundness also wrt. infinite trace. There, following Jacobs' work, infinite trace semantics is characterized as the "largest homomorphism." It turns out that soundness of forward simulations is rather straightforward; that of backward simulation holds too, although it requires certain additional conditions and its proof is more involved. We also show that FPE can be successfully employed in the infinite trace setting to enhance the applicability of Kleisli simulations as witnesses of trace inclusion. Our framework is parameterized in the monad for branching as well as in the functor for linear-time behaviors; for the former we use the powerset monad (for nondeterminism) as well as the sub-Giry monad (for probability).
https://drops.dagstuhl.de/storage/00lipics/lipics-vol035-calco2015/LIPIcs.CALCO.2015.320/LIPIcs.CALCO.2015.320.pdf
category theory
coalgebra
simulation
verification
trace semantics
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2015-10-28
35
336
351
10.4230/LIPIcs.CALCO.2015.336
article
Finitary Corecursion for the Infinitary Lambda Calculus
Milius, Stefan
Wißmann, Thorsten
Kurz et al. have recently shown that infinite lambda-trees with finitely many free variables modulo alpha-equivalence form a final coalgebra for a functor on the category of nominal sets. Here we investigate the rational fixpoint of that functor. We prove that it is formed by all rational lambda-trees, i.e. those lambda-trees which have only finitely many subtrees (up to isomorphism). This yields a corecursion principle that allows the definition of operations such as substitution on rational lambda-trees.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol035-calco2015/LIPIcs.CALCO.2015.336/LIPIcs.CALCO.2015.336.pdf
rational trees
infinitary lambda calculus
coinduction