3 Search Results for "Plotkin, Gordon"


Document
Tensor of Quantitative Equational Theories

Authors: Giorgio Bacci, Radu Mardare, Prakash Panangaden, and Gordon Plotkin

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


Abstract
We develop a theory for the commutative combination of quantitative effects, their tensor, given as a combination of quantitative equational theories that imposes mutual commutation of the operations from each theory. As such, it extends the sum of two theories, which is just their unrestrained combination. Tensors of theories arise in several contexts; in particular, in the semantics of programming languages, the monad transformer for global state is given by a tensor. We show that under certain assumptions on the quantitative theories the free monad that arises from the tensor of two theories is the categorical tensor of the free monads on the theories. As an application, we provide the first algebraic axiomatizations of labelled Markov processes and Markov decision processes. Apart from the intrinsic interest in the axiomatizations, it is pleasing they are obtained compositionally by means of the sum and tensor of simpler quantitative equational theories.

Cite as

Giorgio Bacci, Radu Mardare, Prakash Panangaden, and Gordon Plotkin. Tensor of Quantitative Equational Theories. In 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 211, pp. 7:1-7:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{bacci_et_al:LIPIcs.CALCO.2021.7,
  author =	{Bacci, Giorgio and Mardare, Radu and Panangaden, Prakash and Plotkin, Gordon},
  title =	{{Tensor of Quantitative Equational Theories}},
  booktitle =	{9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)},
  pages =	{7:1--7:17},
  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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.7},
  URN =		{urn:nbn:de:0030-drops-153628},
  doi =		{10.4230/LIPIcs.CALCO.2021.7},
  annote =	{Keywords: Quantitative equational theories, Tensor, Monads, Quantitative Effects}
}
Document
Reverse Derivative Categories

Authors: Robin Cockett, Geoffrey Cruttwell, Jonathan Gallagher, Jean-Simon Pacaud Lemay, Benjamin MacAdam, Gordon Plotkin, and Dorette Pronk

Published in: LIPIcs, Volume 152, 28th EACSL Annual Conference on Computer Science Logic (CSL 2020)


Abstract
The reverse derivative is a fundamental operation in machine learning and automatic differentiation [Martín Abadi et al., 2015; Griewank, 2012]. This paper gives a direct axiomatization of a category with a reverse derivative operation, in a similar style to that given by [Blute et al., 2009] for a forward derivative. Intriguingly, a category with a reverse derivative also has a forward derivative, but the converse is not true. In fact, we show explicitly what a forward derivative is missing: a reverse derivative is equivalent to a forward derivative with a dagger structure on its subcategory of linear maps. Furthermore, we show that these linear maps form an additively enriched category with dagger biproducts.

Cite as

Robin Cockett, Geoffrey Cruttwell, Jonathan Gallagher, Jean-Simon Pacaud Lemay, Benjamin MacAdam, Gordon Plotkin, and Dorette Pronk. Reverse Derivative Categories. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 18:1-18:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)


Copy BibTex To Clipboard

@InProceedings{cockett_et_al:LIPIcs.CSL.2020.18,
  author =	{Cockett, Robin and Cruttwell, Geoffrey and Gallagher, Jonathan and Lemay, Jean-Simon Pacaud and MacAdam, Benjamin and Plotkin, Gordon and Pronk, Dorette},
  title =	{{Reverse Derivative Categories}},
  booktitle =	{28th EACSL Annual Conference on Computer Science Logic (CSL 2020)},
  pages =	{18:1--18:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-132-0},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{152},
  editor =	{Fern\'{a}ndez, Maribel and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2020.18},
  URN =		{urn:nbn:de:0030-drops-116611},
  doi =		{10.4230/LIPIcs.CSL.2020.18},
  annote =	{Keywords: Reverse Derivatives, Cartesian Reverse Differential Categories, Categorical Semantics, Cartesian Differential Categories, Dagger Categories, Automatic Differentiation}
}
Document
A convenient category of domains

Authors: Ingo Battenfeld, Matthias Schröder, and Alex Simpson

Published in: Dagstuhl Seminar Proceedings, Volume 6341, Computational Structures for Modelling Space, Time and Causality (2007)


Abstract
We motivate and define a category of "topological domains", whose objects are certain topological spaces, generalising the usual $omega$-continuous dcppos of domain theory. Our category supports all the standard constructions of domain theory, including the solution of recursive domain equations. It also supports the construction of free algebras for (in)equational theories, provides a model of parametric polymorphism, and can be used as the basis for a theory of computability. This answers a question of Gordon Plotkin, who asked whether it was possible to construct a category of domains combining such properties.

Cite as

Ingo Battenfeld, Matthias Schröder, and Alex Simpson. A convenient category of domains. In Computational Structures for Modelling Space, Time and Causality. Dagstuhl Seminar Proceedings, Volume 6341, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2007)


Copy BibTex To Clipboard

@InProceedings{battenfeld_et_al:DagSemProc.06341.2,
  author =	{Battenfeld, Ingo and Schr\"{o}der, Matthias and Simpson, Alex},
  title =	{{A convenient category of domains}},
  booktitle =	{Computational Structures for Modelling Space, Time and Causality},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2007},
  volume =	{6341},
  editor =	{Ralph Kopperman and Prakash Panangaden and Michael B. Smyth and Dieter Spreen},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.06341.2},
  URN =		{urn:nbn:de:0030-drops-8945},
  doi =		{10.4230/DagSemProc.06341.2},
  annote =	{Keywords: Domain theory, topology of datatypes}
}
  • Refine by Author
  • 2 Plotkin, Gordon
  • 1 Bacci, Giorgio
  • 1 Battenfeld, Ingo
  • 1 Cockett, Robin
  • 1 Cruttwell, Geoffrey
  • Show More...

  • Refine by Classification
  • 1 Theory of computation → Equational logic and rewriting
  • 1 Theory of computation → Program semantics
  • 1 Theory of computation → Semantics and reasoning

  • Refine by Keyword
  • 1 Automatic Differentiation
  • 1 Cartesian Differential Categories
  • 1 Cartesian Reverse Differential Categories
  • 1 Categorical Semantics
  • 1 Dagger Categories
  • Show More...

  • Refine by Type
  • 3 document

  • Refine by Publication Year
  • 1 2007
  • 1 2020
  • 1 2021

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