Daniela Petrisan's Publications
In journals
- Automata and minimization.
Thomas Colcombet, Daniela Petrisan, SIGLOG News 4(2): 4-27 (2017)
[link]
[abstract]
Already in
the seventies, strong results illustrating the intimate
relationship between category theory and automata theory
have been described and are still investigated. In this
column, we provide a uniform presentation of the basic
concepts that underlie minimization results in automata
theory. We then use this knowledge for introducing a new
model of automata that is an hybrid of deterministic
finite automata and automata weighted over a
field. These automata are very natural, and enjoy
minimization result by design.
The presentation of this paper is indeed categorical in
essence, but it assumes no prior knowledge from the
reader. It is also non-conventional in that it is
neither algebraic, nor co-algebraic oriented.
- A general account of coinduction up-to,
F. Bonchi, D. Petrisan, D. Pous, J. Rot, Acta Informatica, (2016)
[link]
[abstract]
[bibtex]
@Article{BPPR2016,
author={Bonchi, Filippo
and Petri{\c{s}}an, Daniela
and Pous, Damien
and Rot, Jurriaan},
title={A general account of coinduction up-to},
journal=[Acta Informatica},
year={2016},
pages={1--64},
issn={1432-0525},
doi={10.1007/s00236-016-0271-4},
url={http://dx.doi.org/10.1007/s00236-016-0271-4},
}
Bisimulation up-to enhances the coinductive proof
method for bisimilarity, providing efficient proof techniques
for checking properties of different kinds of systems. We
prove the soundness of such techniques in a fibrational
setting, building on the seminal work of Hermida and
Jacobs. This allows us to systematically obtain up-to
techniques not only for bisimilarity but for a large class of
coinductive predicates modeled as coalgebras. The fact that
bisimulations up to context can be safely used in any language
specified by GSOS rules can also be seen as an instance of our
framework, using the well-known observation by Turi and
Plotkin that such languages form bialgebras. In the second
part of the paper, we provide a new categorical treatment of
weak bisimilarity on labeled transition systems and we prove
the soundness of up-to context for weak bisimulations of
systems specified by cool rule formats, as defined by Bloom to
ensure congruence of weak bisimilarity. The weak transition
systems obtained from such cool rules give rise to lax
bialgebras, rather than to bialgebras. Hence, to reach our
goal, we extend the categorical framework developed in the
first part to an ordered setting.
- Relation lifting, with an application to the many-valued cover modality,
M. Bílková, A. Kurz, D. Petrisan, J. Velebil, Logical Methods in Computer Science 9(4), (2013)
[link]
[abstract]
[bibtex]
@article{BKPV13,
author = {Marta B\'{\i}lkov{\'a} and
Alexander Kurz and
Daniela Petri{\c s}an and
J{\' i}{\v r}{\' i} Velebil},
title = {Relation lifting, with an application to the many-valued
cover modality},
journal = {Logical Methods in Computer Science},
volume = {9},
number = {4},
year = {2013},
}
We introduce basic notions and results about relation liftings
on categories enriched in a commutative quantale. We derive
two necessary and sufficient conditions for a 2-functor T to
admit a functorial relation lifting: one is the existence of a
distributive law of T over the "powerset monad" on
categories, one is the preservation by T of
"exactness" of certain squares. Both
characterisations are generalisations of the
"classical" results known for set functors: the
first characterisation generalises the existence of a
distributive law over the genuine powerset monad, the second
generalises preservation of weak pullbacks. The results
presented in this paper enable us to compute predicate
liftings of endofunctors of, for example, generalised
(ultra)metric spaces. We illustrate this by studying the
coalgebraic cover modality in this setting.
- Nominal Coalgebraic Data Types with Applications to Lambda Calculus,
A. Kurz, D. Petrisan, P. Severi, F. de Vries, Logical Methods in Computer Science 9(4), (2013)
[link]
[abstract]
[bibtex]
@article{KPSV13,
author = {Alexander Kurz and
Daniela Petrisan and
Paula Severi and
Fer-Jan de Vries},
title = {Nominal Coalgebraic Data Types with Applications to Lambda
Calculus},
journal = {Logical Methods in Computer Science},
volume = {9},
number = {4},
year = {2013},
}
We investigate final coalgebras in nominal sets. This allows
us to define types of infinite data with binding for which all
constructions automatically respect alpha equivalence. We give
applications to the infinitary lambda calculus.
- On Universal Algebra over Nominal Sets.
A. Kurz, D. Petrisan, Mathematical Structures in Computer Science, Volume
20 (2): 285-318 (2010).
[link]
[abstract]
[bibtex]
@article{KP10a,
author = {Alexander Kurz and
Daniela Petrisan},
title = {On universal algebra over nominal sets},
journal = {Mathematical Structures in Computer Science},
volume = {20},
number = {2},
year = {2010},
pages = {285-318},
}
We
investigate universal algebra over the category Nom of nominal
sets. Using the fact that Nom is a full reflective subcategory
of a monadic category, we obtain an HSP-like theorem for
algebras over nominal sets. We isolate a "uniform"
fragment of our equational logic, which corresponds to the
nominal logics present in the literature. We give semantically
invariant translations of theories for nominal algebra and NEL
into "uniform" theories, and systematically prove
HSP theorems for models of these theories.
- Presenting Functors on Many-Sorted Varieties and Applications.
A. Kurz, D. Petrisan, Information and Computation. 208(12): 1421-1446 (2010)
[link]
[abstract]
[bibtex]
@article{KP10b,
author = {Alexander Kurz and
Daniela Petrisan},
title = {Presenting functors on many-sorted varieties and applications},
journal = {Inf. Comput.},
volume = {208},
number = {12},
year = {2010},
pages = {1421-1446}
}
This paper studies several applications of the
notion of a presentation of a functor by
operations and equations. We show that the
technically straightforward generalisation of
this notion from the one-sorted to the
many-sorted case has several interesting
consequences. First, it can be applied to give
equational logic for the binding algebras
modelling abstract syntax. Second, it provides a
categorical approach to algebraic semantics of
first-order logic. Third, this notion links the
uniform treatment of logics for coalgebras of an
arbitrary type T with concrete syntax and proof
systems. Analysing the many-sorted case is
essential for modular completeness proofs of
coalgebraic logics.
In conferences
- Automata in the Category of Glued Vector Spaces
Thomas Colcombet, Daniela Petrisan, MFCS 2017
[link]
[abstract]
In this
paper we adopt a category-theoretic approach to the
conception of automata classes enjoying minimization by
design. The main instantiation of our construction is a
new class of automata that are hybrid between
deterministic automata and automata weighted over a
field.
- Automata minimization: a functorial approach
Thomas Colcombet, Daniela Petrisan, CALCO 2017
[link]
[abstract]
In this
paper we regard languages and their acceptors - such as
deterministic or weighted automata, transducers, or
monoids - as functors from input categories that
specify the type of the languages and of the machines
to categories that specify the type of outputs. Our
results are as follows: a) We provide sufficient
conditions on the output category so that minimization
of the corresponding automata is guaranteed. b) We show
how to lift adjunctions between the categories for
output values to adjunctions between categories of
automata. c) We show how this framework can be applied
to several phenomena in automata theory, starting with
determinization and minimization (previously studied
from a coalgebraic and duality theoretic
perspective). We apply in particular these techniques
to Choffrut’s minimization algorithm for subsequential
transducers and revisit Brzozowski’s minimization
algorithm.
- Quantifiers on languages and codensity monads,
Mai Gehrke, Daniela Petrisan, Luca Reggio, . LICS 2017
[link]
[abstract]
[arxiv long version]
This
paper contributes to the techniques of topoalgebraic
recognition for languages beyond the regular setting as
they relate to logic on words. In particular, we
provide a general construction on recognisers
corresponding to adding one layer of various kinds of
quantifiers and prove a related Reutenauer-type
theorem. Our main tools are codensity monads and
duality theory. Our construction yields, in particular,
a new characterisation of the profinite monad of the
free S-semimodule monad for finite and commutative
semirings S, which generalises our earlier insight that
the Vietoris monad on Boolean spaces is the codensity
monad of the finite powerset functor.
- The Schutzenberger Product for Syntactic Spaces. ,
M. Gehrke, D. Petrisan, L. Reggio, ICALP 2016
[link]
[abstract]
Starting from Boolean algebras of languages closed under
quotients and using duality theoretic insights, we derive the
notion of Boolean spaces with internal monoids as recognisers
for arbitrary formal languages of finite words over finite
alphabets. This leads to recognisers and syntactic spaces in a
setting that is well-suited for applying tools from Stone
duality as applied in semantics. The main focus of the paper
is the development of topo-algebraic constructions pertinent
to the treatment of languages given by logic formulas. In
particular, using the standard semantic view of quantification
as projection, we derive a notion of Schützenberger product
for Boolean spaces with internal monoids. This makes heavy use
of the Vietoris construction - and its dual functor - which is
central to the coalgebraic treatment of classical modal
logic. We show that the unary Schützenberger product for
spaces yields a recogniser for the language of all models of
the formula EXISTS x.phi(x), when applied to a recogniser for
the language of all models of phi(x). Further, we generalise
global and local versions of the theorems of Schützenberger
and Reutenauer characterising the languages recognised by the
binary Schützenberger product. Finally, we provide an
equational characterisation of Boolean algebras obtained by
local Schützenberger product with the one element space based
on an Egli-Milner type condition on generalised factorisations
of ultrafilters on words.
- Lax Bialgebras and Up-To Techniques
for Weak Bisimulations,
F. Bonchi, D. Petrisan, D. Pous, J. Rot, CONCUR 2015
[abstract]
Up-to techniques are useful tools for optimising proofs of
behavioural equivalence of processes. Bisimulations up-to
context can be safely used in any language specified by GSOS
rules. We showed this result in a previous paper by exploiting
the well-known observation by Turi and Plotkin that such
languages form bialgebras. In this paper, we prove the
soundness of up-to contextual closure for weak bisimilations
of systems specified by cool rule formats, as defined by Bloom
to ensure congruence of weak bisimilarity. However, the weak
transition systems obtained from such cool rules give rise to
lax bialgebras, rather than to bialgebras. Hence, to reach
our goal, we extend our previously developed categorical
framework to an ordered enriched setting.
- Nominal techniques for variables with interleaving scopes,
D. Ghica, M.J. Gabbay, D. Petrisan. CSL 2015
-
Nominal Kleene Coalgebra,
D. Kozen, K. Mamouras, D. Petrisan, A. Silva, ICALP 2015
[abstract]
[long version]
We develop the coalgebraic theory of nominal Kleene algebra,
including an alternative language-theoretic semantics, a
nominal extension of the Brzozowski derivative, and a
bisimulation-based decision procedure for the equational
theory.
-
Approximation of Nested Fixpoints -- A Coalgebraic View of Parametric Dataypes,
A. Kurz, A. Pardo, D. Petrisan, P. Severi and F-J. de Vries, CALCO 2015
[abstract]
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 non-termination and infinite data) and on the other
hand 2-categorical (to deal with parameters in a disciplined
manner). We prove a coalgebraic version of Beki{\v c} 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.
-
Coinduction up-to in a fibrational setting,
F. Bonchi, D. Petrisan, D. Pous, J. Rot, CSL-LICS 2014
[link]
[arxiv link]
[abstract]
[bibtex]
@inproceedings{DBLP:conf/csl/BonchiPPR14,,
author = {Filippo Bonchi and
Daniela Petrisan and
Damien Pous and
Jurriaan Rot},
title = {Coinduction up-to in a fibrational setting},
booktitle = {Joint Meeting of the Twenty-Third {EACSL} Annual Conference on Computer
Science Logic {(CSL)} and the Twenty-Ninth Annual {ACM/IEEE} Symposium
on Logic in Computer Science (LICS), {CSL-LICS} '14, Vienna, Austria,
July 14 - 18, 2014},
pages = {20},
year = {2014},
url = {http://doi.acm.org/10.1145/2603088.2603149},
doi = {10.1145/2603088.2603149},
}
Bisimulation up-to enhances the coinductive proof method for
bisimilarity, providing efficient proof techniques for
checking properties of different kinds of systems. We prove
the soundness of such techniques in a fibrational setting,
building on the seminal work of Hermida and Jacobs. This
allows us to systematically obtain up-to techniques not only
for bisimilarity but for a large class of coinductive
predicates modelled as coalgebras. By tuning the parameters of
our framework, we obtain novel techniques for unary predicates
and nominal automata, a variant of the GSOS rule format for
similarity, and a new categorical treatment of weak
bisimilarity.
- An Alpha-Corecursion Principle for the Infinitary Lambda Calculus.
A. Kurz, D. Petrisan, P. Severi, F. de Vries, CMCS 2012.
[link]
[abstract]
[bibtex]
@inproceedings{KPSV12,
author = {Alexander Kurz and
Daniela Petrisan and
Paula Severi and
Fer-Jan de Vries},
title = {An Alpha-Corecursion Principle for the Infinitary Lambda
Calculus},
booktitle = {CMCS},
editor = {Dirk Pattinson and
Lutz Schroder},
year = {2012},
pages = {130-149},
ee = {http://dx.doi.org/10.1007/978-3-642-32784-1_8},
}
Gabbay and Pitts proved that lambda-terms up to
alpha-equivalence constitute an initial algebra for a certain
endofunctor on the category of nominal sets. We show that the
terms of the infinitary lambda-calculus form the final
coalgebra for the same functor. This allows us to give a
corecursion principle for alpha-equivalence classes of finite
and infinite terms. As an application, we give corecursive
definitions of substitution and of infinite normal forms
(Böhm, Lévy-Longo and Berarducci trees).
- Stone duality for nominal Boolean algebras with `new'.
M. Gabbay, T. Litak, D. Petrisan, CALCO 2011.
[link]
[abstract]
[bibtex]
@inproceedings{GLP11,
author = {Murdoch James Gabbay and
Tadeusz Litak and
Daniela Petrisan},
title = {Stone Duality for Nominal Boolean Algebras with `new'},
booktitle = {CALCO},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {6859},
year = {2011},
pages = {192-207},
ee = {http://dx.doi.org/10.1007/978-3-642-22944-2_14},
}
We
define Boolean algebras over nominal sets with a function
symbol И mirroring the И ‘fresh name’ quantifier (Banonas),
and dual notions of nominal topology and Stone space. We prove
a representation theorem over fields of nominal sets, and
extend this to a Stone duality.
- Relation Liftings on Preorders.
M. Bilkova, A. Kurz, D. Petrisan, J. Velebil, CALCO 2011.
[link]
[abstract]
[bibtex]
@inproceedings{BKPV11,
author = {Marta B\'{\i}lkov{\'a} and
Alexander Kurz and
Daniela Petrisan and
Jiri Velebil},
title = {Relation Liftings on Preorders and Posets},
booktitle = {CALCO},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {6859},
year = {2011},
pages = {115-129},
ee = {http://dx.doi.org/10.1007/978-3-642-22944-2_9}
}
The category Rel(Set) of sets and relations can be described
as a category of spans and as the Kleisli category for the
powerset monad. A set-functor can be lifted to a functor on
Rel(Set) iff it preserves weak pullbacks. We show that these
results extend to the enriched setting, if we replace sets by
posets or preorders. Preservation of weak pullbacks becomes
preservation of exact lax squares. As an application we
present Moss’s coalgebraic over posets.
- A Duality Theorem for
Real C* Algebras.
A.M. Moshier, D. Petrisan, CALCO 2009.
[link]
[abstract]
[bibtex]
@inproceedings{MP09,
author = {M. Andrew Moshier and
Daniela Petrisan},
title = {A Duality Theorem for Real {\it C}$^{\mbox{*}}$ Algebras},
booktitle = {CALCO},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {5728},
year = {2009},
pages = {284-299},
ee = {http://dx.doi.org/10.1007/978-3-642-03741-2_20},
}
The
full subcategory of proximity lattices equipped with some
additional structure (a certain form of negation) is
equivalent to the category of compact Hausdorff spaces. Using
the Stone-Gelfand-Naimark duality, we know that the category
of proximity lattices with negation is dually equivalent to
the category of real C* algebras. The aim of this paper is to
give a new proof for this duality, avoiding the construction
of spaces. We prove that the category of C* algebras is
equivalent to the category of skew frames with negation, which
appears in the work of Moshier and Jung on the bitopological
nature of Stone duality.
- Functorial Coalgebraic Logic:
The case of many-sorted varieties.
A. Kurz, D. Petrisan, CMCS 2008.
[link]
[abstract]
[bibtex]
@article{KP08,
author = {Alexander Kurz and
Daniela Petrisan},
title = {Functorial Coalgebraic Logic: The Case of Many-sorted Varieties},
journal = {Electr. Notes Theor. Comput. Sci.},
volume = {203},
number = {5},
year = {2008},
pages = {175-194},
ee = {http://dx.doi.org/10.1016/j.entcs.2008.05.025},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
Following earlier work, a modal logic for T-coalgebras is a
functor L on a suitable variety. Syntax and proof system of
the logic are given by presentations of the functor. This
paper makes two contributions. First, a previous result
characterizing those functors that have presentations is
generalized from endofunctors on one-sorted varieties to
functors between many-sorted varieties. This yields an
equational logic for the presheaf semantics of higher-order
abstract syntax. As another application, we show how the move
to functors between many-sorted varieties allows to modularly
combine syntax and proof systems of different logics. Second,
we show how to associate to any set-functor T a complete
(finitary) logic L consisting of modal operators and Boolean
connectives.
Preprints
- Algebraic Theories over Nominal Sets,
A. Kurz, D. Petrisan, J. Velebil.
[arxiv link]
[abstract]
We
investigate the foundations of a theory of algebraic data
types with variable binding inside classical universal
algebra. In the first part, a category-theoretic study of
monads over the nominal sets of Gabbay and Pitts leads us to
introduce new notions of finitary based monads and uniform
monads. In a second part we spell out these notions in the
language of universal algebra, show how to recover the logics
of Gabbay-Mathijssen and Clouston-Pitts, and apply classical
results from universal algebra.
Thesis
My PhD thesis Investigations into Algebra and Topology over
Nominal Sets is available here.