Search Results

Documents authored by Dahlqvist, Fredrik

Document
DOI: 10.4230/LIPIcs.CSL.2022.16
An Internal Language for Categories Enriched over Generalised Metric Spaces

Authors: Fredrik Dahlqvist and Renato Neves

Published in: LIPIcs, Volume 216, 30th EACSL Annual Conference on Computer Science Logic (CSL 2022)

Abstract
Programs with a continuous state space or that interact with physical processes often require notions of equivalence going beyond the standard binary setting in which equivalence either holds or does not hold. In this paper we explore the idea of equivalence taking values in a quantale 𝒱, which covers the cases of (in)equations and (ultra)metric equations among others. Our main result is the introduction of a 𝒱-equational deductive system for linear λ-calculus together with a proof that it is sound and complete (in fact, an internal language) for a class of enriched autonomous categories. In the case of inequations, we get an internal language for autonomous categories enriched over partial orders. In the case of (ultra)metric equations, we get an internal language for autonomous categories enriched over (ultra)metric spaces. We use our results to obtain examples of inequational and metric equational systems for higher-order programs that contain real-time and probabilistic behaviour.
Cite as

Fredrik Dahlqvist and Renato Neves. An Internal Language for Categories Enriched over Generalised Metric Spaces. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 16:1-16:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{dahlqvist_et_al:LIPIcs.CSL.2022.16,
  author =	{Dahlqvist, Fredrik and Neves, Renato},
  title =	{{An Internal Language for Categories Enriched over Generalised Metric Spaces}},
  booktitle =	{30th EACSL Annual Conference on Computer Science Logic (CSL 2022)},
  pages =	{16:1--16:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-218-1},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{216},
  editor =	{Manea, Florin and Simpson, Alex},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2022.16},
  URN =		{urn:nbn:de:0030-drops-157362},
  doi =		{10.4230/LIPIcs.CSL.2022.16},
  annote =	{Keywords: \lambda-calculus, enriched category theory, quantale, equational theory}
}
Document
(Co)algebraic pearls
DOI: 10.4230/LIPIcs.CALCO.2021.13
How to Write a Coequation ((Co)algebraic pearls)

Authors: Fredrik Dahlqvist and Todd Schmid

Published in: LIPIcs, Volume 211, 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)

Abstract
There is a large amount of literature on the topic of covarieties, coequations and coequational specifications, dating back to the early seventies. Nevertheless, coequations have not (yet) emerged as an everyday practical specification formalism for computer scientists. In this review paper, we argue that this is partly due to the multitude of syntaxes for writing down coequations, which seems to have led to some confusion about what coequations are and what they are for. By surveying the literature, we identify four types of syntaxes: coequations-as-corelations, coequations-as-predicates, coequations-as-equations, and coequations-as-modal-formulas. We present each of these in a tutorial fashion, relate them to each other, and discuss their respective uses.
Cite as

Fredrik Dahlqvist and Todd Schmid. How to Write a Coequation ((Co)algebraic pearls). In 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 211, pp. 13:1-13:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{dahlqvist_et_al:LIPIcs.CALCO.2021.13,
  author =	{Dahlqvist, Fredrik and Schmid, Todd},
  title =	{{How to Write a Coequation}},
  booktitle =	{9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)},
  pages =	{13:1--13:25},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-212-9},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{211},
  editor =	{Gadducci, Fabio and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.13},
  URN =		{urn:nbn:de:0030-drops-153686},
  doi =		{10.4230/LIPIcs.CALCO.2021.13},
  annote =	{Keywords: Coalgebra, coequation, covariety}
}
Document
DOI: 10.4230/LIPIcs.CALCO.2017.9
The Positivication of Coalgebraic Logics

Authors: Fredrik Dahlqvist and Alexander Kurz

Published in: LIPIcs, Volume 72, 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017)

Abstract
We present positive coalgebraic logic in full generality, and show how to obtain a positive coalgebraic logic from a boolean one. On the model side this involves canonically computing a endofunctor T': Pos->Pos from an endofunctor T: Set->Set, in a procedure previously defined by the second author et alii called posetification. On the syntax side, it involves canonically computing a syntax-building functor L': DL->DL from a syntax-building functor L: BA->BA, in a dual procedure which we call positivication. These operations are interesting in their own right and we explicitly compute posetifications and positivications in the case of several modal logics. We show how the semantics of a boolean coalgebraic logic can be canonically lifted to define a semantics for its positive fragment, and that weak completeness transfers from the boolean case to the positive case.
Cite as

Fredrik Dahlqvist and Alexander Kurz. The Positivication of Coalgebraic Logics. In 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 72, pp. 9:1-9:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{dahlqvist_et_al:LIPIcs.CALCO.2017.9,
  author =	{Dahlqvist, Fredrik and Kurz, Alexander},
  title =	{{The Positivication of Coalgebraic Logics}},
  booktitle =	{7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017)},
  pages =	{9:1--9:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-033-0},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{72},
  editor =	{Bonchi, Filippo and K\"{o}nig, Barbara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2017.9},
  URN =		{urn:nbn:de:0030-drops-80425},
  doi =		{10.4230/LIPIcs.CALCO.2017.9},
  annote =	{Keywords: Coalgebraic logic, coalgebras, enriched category theory, boolean algebra, distributive lattice, positive modal logic, monotone modal logic}
}
Document
Invited Paper
DOI: 10.4230/LIPIcs.CONCUR.2016.1
Bayesian Inversion by Omega-Complete Cone Duality (Invited Paper)

Authors: Fredrik Dahlqvist, Vincent Danos, Ilias Garnier, and Ohad Kammar

Published in: LIPIcs, Volume 59, 27th International Conference on Concurrency Theory (CONCUR 2016)

Abstract
The process of inverting Markov kernels relates to the important subject of Bayesian modelling and learning. In fact, Bayesian update is exactly kernel inversion. In this paper, we investigate how and when Markov kernels (aka stochastic relations, or probabilistic mappings, or simply kernels) can be inverted. We address the question both directly on the category of measurable spaces, and indirectly by interpreting kernels as Markov operators: - For the direct option, we introduce a typed version of the category of Markov kernels and use the so-called "disintegration of measures". Here, one has to specialise to measurable spaces borne from a simple class of topological spaces -e.g. Polish spaces (other choices are possible). Our method and result greatly simplify a recent development in Ref. [4]. - For the operator option, we use a cone version of the category of Markov operators (kernels seen as predicate transformers). That is to say, our linear operators are not just continuous, but are required to satisfy the stronger condition of being $\om$-chain-continuous. Prior work shows that one obtains an adjunction in the form of a pair of contravariant and inverse functors between the categories of $L_1$- and $L_\infty$-cones [3]. Inversion, seen through the operator prism, is just adjunction. No topological assumption is needed. - We show that both categories (Markov kernels and $\om$-chain-continuous Markov operators) are related by a family of contravariant functors $T_p$ for $1\leq p\leq\infty$. The $T_p$'s are Kleisli extensions of (duals of) conditional expectation functors introduced in Ref. [3]. - With this bridge in place, we can prove that both notions of inversion agree when both defined: if $f$ is a kernel, and $f\dg$ its direct inverse, then $T_\infty(f)\dg=T_1(f\dg)$.
Cite as

Fredrik Dahlqvist, Vincent Danos, Ilias Garnier, and Ohad Kammar. Bayesian Inversion by Omega-Complete Cone Duality (Invited Paper). In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 1:1-1:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{dahlqvist_et_al:LIPIcs.CONCUR.2016.1,
  author =	{Dahlqvist, Fredrik and Danos, Vincent and Garnier, Ilias and Kammar, Ohad},
  title =	{{Bayesian Inversion by Omega-Complete Cone Duality}},
  booktitle =	{27th International Conference on Concurrency Theory (CONCUR 2016)},
  pages =	{1:1--1:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-017-0},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{59},
  editor =	{Desharnais, Jos\'{e}e and Jagadeesan, Radha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2016.1},
  URN =		{urn:nbn:de:0030-drops-61909},
  doi =		{10.4230/LIPIcs.CONCUR.2016.1},
  annote =	{Keywords: probabilistic models, bayesian learning, markov operators}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2016.23
Robustly Parameterised Higher-Order Probabilistic Models

Authors: Fredrik Dahlqvist, Vincent Danos, and Ilias Garnier

Published in: LIPIcs, Volume 59, 27th International Conference on Concurrency Theory (CONCUR 2016)

Abstract
We present a method for constructing robustly parameterised families of higher-order probabilistic models. Parameter spaces and models are represented by certain classes of functors in the category of Polish spaces. Maps from parameter spaces to models (parameterisations) are continuous and natural transformations between such functors. Naturality ensures that parameterised models are invariant by change of granularity -- ie that parameterisations are intrinsic. Continuity ensures that models are robust with respect to their parameterisation. Our method allows one to build models from a set of basic functors among which the Giry probabilistic functor, spaces of cadlag trajectories (in continuous and discrete time), multisets and compact powersets. These functors can be combined by guarded composition, product and coproduct. Parameter spaces range over the polynomial closure of Giry-like functors. Thus we obtain a class of robust parameterised models which includes the Dirichlet process, various point processes (random sequences with values in Polish spaces) and other classical objects of probability theory. By extending techniques developed in prior work, we show how to reduce the questions of existence, uniqueness, naturality, and continuity of a parameterised model to combinatorial questions only involving finite spaces.
Cite as

Fredrik Dahlqvist, Vincent Danos, and Ilias Garnier. Robustly Parameterised Higher-Order Probabilistic Models. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 23:1-23:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{dahlqvist_et_al:LIPIcs.CONCUR.2016.23,
  author =	{Dahlqvist, Fredrik and Danos, Vincent and Garnier, Ilias},
  title =	{{Robustly Parameterised Higher-Order Probabilistic Models}},
  booktitle =	{27th International Conference on Concurrency Theory (CONCUR 2016)},
  pages =	{23:1--23:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-017-0},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{59},
  editor =	{Desharnais, Jos\'{e}e and Jagadeesan, Radha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2016.23},
  URN =		{urn:nbn:de:0030-drops-61737},
  doi =		{10.4230/LIPIcs.CONCUR.2016.23},
  annote =	{Keywords: Probability, category theory, Giry monad}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact