Search Results

Documents authored by Severi, Paula

Document
DOI: 10.4230/LIPIcs.CALCO.2015.205
Approximation of Nested Fixpoints – A Coalgebraic View of Parametric Dataypes

Authors: Alexander Kurz, Alberto Pardo, Daniela Petrisan, Paula Severi, and Fer-Jan de Vries

Published in: LIPIcs, Volume 35, 6th Conference on Algebra and Coalgebra in Computer Science (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 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.
Cite as

Alexander Kurz, Alberto Pardo, Daniela Petrisan, Paula Severi, and Fer-Jan de Vries. Approximation of Nested Fixpoints – A Coalgebraic View of Parametric Dataypes. In 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 35, pp. 205-220, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{kurz_et_al:LIPIcs.CALCO.2015.205,
  author =	{Kurz, Alexander and Pardo, Alberto and Petrisan, Daniela and Severi, Paula and de Vries, Fer-Jan},
  title =	{{Approximation of Nested Fixpoints – A Coalgebraic View of Parametric Dataypes}},
  booktitle =	{6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015)},
  pages =	{205--220},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-84-2},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{35},
  editor =	{Moss, Lawrence S. and Sobocinski, Pawel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2015.205},
  URN =		{urn:nbn:de:0030-drops-55351},
  doi =		{10.4230/LIPIcs.CALCO.2015.205},
  annote =	{Keywords: coalgebra, Bekic lemma, infinite data, functional programming, type theory}
}
Document
DOI: 10.4230/LIPIcs.RTA.2012.288
Meaningless Sets in Infinitary Combinatory Logic

Authors: Paula Severi and Fer-Jan de Vries

Published in: LIPIcs, Volume 15, 23rd International Conference on Rewriting Techniques and Applications (RTA'12) (2012)

Abstract
In this paper we study meaningless sets in infinitary combinatory logic. So far only a handful of meaningless sets were known. We show that there are uncountably many meaningless sets. As an application to the semantics of finite combinatory logics, we show that there exist uncountably many combinatory algebras that are not a lambda algebra. We also study ways of weakening the axioms of meaningless sets to get, not only sufficient, but also necessary conditions for having confluence and normalisation.
Cite as

Paula Severi and Fer-Jan de Vries. Meaningless Sets in Infinitary Combinatory Logic. In 23rd International Conference on Rewriting Techniques and Applications (RTA'12). Leibniz International Proceedings in Informatics (LIPIcs), Volume 15, pp. 288-304, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{severi_et_al:LIPIcs.RTA.2012.288,
  author =	{Severi, Paula and de Vries, Fer-Jan},
  title =	{{Meaningless Sets in Infinitary Combinatory Logic}},
  booktitle =	{23rd International Conference on Rewriting Techniques and Applications (RTA'12)},
  pages =	{288--304},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-38-5},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{15},
  editor =	{Tiwari, Ashish},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2012.288},
  URN =		{urn:nbn:de:0030-drops-34993},
  doi =		{10.4230/LIPIcs.RTA.2012.288},
  annote =	{Keywords: Infinitary Rewriting, Combinatory Logic, Meaningless Sets, Confluence, Normalisation}
}
Document
DOI: 10.4230/LIPIcs.RTA.2011.313
Weakening the Axiom of Overlap in Infinitary Lambda Calculus

Authors: Paula Severi and Fer-Jan de Vries

Published in: LIPIcs, Volume 10, 22nd International Conference on Rewriting Techniques and Applications (RTA'11) (2011)

Abstract
In this paper we present a set of necessary and sufficient conditions on a set of lambda terms to serve as the set of meaningless terms in an infinitary bottom extension of lambda calculus. So far only a set of sufficient conditions was known for choosing a suitable set of meaningless terms to make this construction produce confluent extensions. The conditions covered the three main known examples of sets of meaningless terms. However, the much later construction of many more examples of sets of meaningless terms satisfying the sufficient conditions renewed the interest in the necessity question and led us to reconsider the old conditions. The key idea in this paper is an alternative solution for solving the overlap between beta reduction and bottom reduction. This allows us to reformulate the Axiom of Overlap, which now determines together with the other conditions a larger class of sets of meaningless terms. We show that the reformulated conditions are not only sufficient but also necessary for obtaining a confluent and normalizing infinitary lambda beta bottom calculus. As an interesting consequence of the necessity proof we obtain for infinitary lambda calculus with beta and bot reduction that confluence implies normalization.
Cite as

Paula Severi and Fer-Jan de Vries. Weakening the Axiom of Overlap in Infinitary Lambda Calculus. In 22nd International Conference on Rewriting Techniques and Applications (RTA'11). Leibniz International Proceedings in Informatics (LIPIcs), Volume 10, pp. 313-328, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{severi_et_al:LIPIcs.RTA.2011.313,
  author =	{Severi, Paula and de Vries, Fer-Jan},
  title =	{{Weakening the Axiom of Overlap in Infinitary Lambda Calculus}},
  booktitle =	{22nd International Conference on Rewriting Techniques and Applications (RTA'11)},
  pages =	{313--328},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-30-9},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{10},
  editor =	{Schmidt-Schauss, Manfred},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2011.313},
  URN =		{urn:nbn:de:0030-drops-31312},
  doi =		{10.4230/LIPIcs.RTA.2011.313},
  annote =	{Keywords: Infinitary Lambda Calculus, Confluence, Normalization}
}
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