3 Search Results for "Alvarez-Picallo, Mario"

Document
DOI: 10.4230/LIPIcs.CSL.2023.6
Functorial String Diagrams for Reverse-Mode Automatic Differentiation

Authors: Mario Alvarez-Picallo, Dan Ghica, David Sprunger, and Fabio Zanasi

Published in: LIPIcs, Volume 252, 31st EACSL Annual Conference on Computer Science Logic (CSL 2023)

Abstract
We formulate a reverse-mode automatic differentiation (RAD) algorithm for (applied) simply typed lambda calculus in the style of Pearlmutter and Siskind [Barak A. Pearlmutter and Jeffrey Mark Siskind, 2008], using the graphical formalism of string diagrams. Thanks to string diagram rewriting, we are able to formally prove for the first time the soundness of such an algorithm. Our approach requires developing a calculus of string diagrams with hierarchical features in the spirit of functorial boxes, in order to model closed monoidal (and cartesian closed) structure. To give an efficient yet principled implementation of the RAD algorithm, we use foliations of our hierarchical string diagrams.
Cite as

Mario Alvarez-Picallo, Dan Ghica, David Sprunger, and Fabio Zanasi. Functorial String Diagrams for Reverse-Mode Automatic Differentiation. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 6:1-6:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{alvarezpicallo_et_al:LIPIcs.CSL.2023.6,
  author =	{Alvarez-Picallo, Mario and Ghica, Dan and Sprunger, David and Zanasi, Fabio},
  title =	{{Functorial String Diagrams for Reverse-Mode Automatic Differentiation}},
  booktitle =	{31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
  pages =	{6:1--6:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-264-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{252},
  editor =	{Klin, Bartek and Pimentel, Elaine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.6},
  URN =		{urn:nbn:de:0030-drops-174674},
  doi =		{10.4230/LIPIcs.CSL.2023.6},
  annote =	{Keywords: string diagrams, automatic differentiation, hierarchical hypergraphs}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2022.29
Rewriting for Monoidal Closed Categories

Authors: Mario Alvarez-Picallo, Dan Ghica, David Sprunger, and Fabio Zanasi

Published in: LIPIcs, Volume 228, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)

Abstract
This paper develops a formal string diagram language for monoidal closed categories. Previous work has shown that string diagrams for freely generated symmetric monoidal categories can be viewed as hypergraphs with interfaces, and the axioms of these categories can be realized by rewriting systems. This work proposes hierarchical hypergraphs as a suitable formalization of string diagrams for monoidal closed categories. We then show double pushout rewriting captures the axioms of these closed categories.
Cite as

Mario Alvarez-Picallo, Dan Ghica, David Sprunger, and Fabio Zanasi. Rewriting for Monoidal Closed Categories. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 29:1-29:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{alvarezpicallo_et_al:LIPIcs.FSCD.2022.29,
  author =	{Alvarez-Picallo, Mario and Ghica, Dan and Sprunger, David and Zanasi, Fabio},
  title =	{{Rewriting for Monoidal Closed Categories}},
  booktitle =	{7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)},
  pages =	{29:1--29:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-233-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{228},
  editor =	{Felty, Amy P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2022.29},
  URN =		{urn:nbn:de:0030-drops-163108},
  doi =		{10.4230/LIPIcs.FSCD.2022.29},
  annote =	{Keywords: string diagrams, rewriting, hierarchical hypergraph, monoidal closed category}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2020.32
The Difference λ-Calculus: A Language for Difference Categories

Authors: Mario Alvarez-Picallo and C.-H. Luke Ong

Published in: LIPIcs, Volume 167, 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)

Abstract
Cartesian difference categories are a recent generalisation of Cartesian differential categories which introduce a notion of "infinitesimal" arrows satisfying an analogue of the Kock-Lawvere axiom, with the axioms of a Cartesian differential category being satisfied only "up to an infinitesimal perturbation". In this work, we construct a simply-typed calculus in the spirit of the differential λ-calculus equipped with syntactic "infinitesimals" and show how its models correspond to difference λ-categories, a family of Cartesian difference categories equipped with suitably well-behaved exponentials.
Cite as

Mario Alvarez-Picallo and C.-H. Luke Ong. The Difference λ-Calculus: A Language for Difference Categories. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 32:1-32:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{alvarezpicallo_et_al:LIPIcs.FSCD.2020.32,
  author =	{Alvarez-Picallo, Mario and Ong, C.-H. Luke},
  title =	{{The Difference \lambda-Calculus: A Language for Difference Categories}},
  booktitle =	{5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)},
  pages =	{32:1--32:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-155-9},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{167},
  editor =	{Ariola, Zena M.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.32},
  URN =		{urn:nbn:de:0030-drops-123549},
  doi =		{10.4230/LIPIcs.FSCD.2020.32},
  annote =	{Keywords: Cartesian difference categories, Cartesian differential categories, Change actions, Differential lambda-calculus, Difference lambda-calculus}
}
  • Refine by Author
  • 3 Alvarez-Picallo, Mario
  • 2 Ghica, Dan
  • 2 Sprunger, David
  • 2 Zanasi, Fabio
  • 1 Ong, C.-H. Luke

  • Refine by Classification
  • 2 Theory of computation → Categorical semantics
  • 1 Mathematics of computing → Automatic differentiation
  • 1 Theory of computation → Equational logic and rewriting
  • 1 Theory of computation → Lambda calculus
  • 1 Theory of computation → Type theory

  • Refine by Keyword
  • 2 string diagrams
  • 1 Cartesian difference categories
  • 1 Cartesian differential categories
  • 1 Change actions
  • 1 Difference lambda-calculus
  • Show More...

  • Refine by Type
  • 3 document

  • Refine by Publication Year
  • 1 2020
  • 1 2022
  • 1 2023

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 Imprint Privacy Contact