2 Search Results for "Hendriks, Dimitri"

Document
DOI: 10.4230/LIPIcs.RTA.2015.143
A Coinductive Framework for Infinitary Rewriting and Equational Reasoning

Authors: Jörg Endrullis, Helle Hvid Hansen, Dimitri Hendriks, Andrew Polonsky, and Alexandra Silva

Published in: LIPIcs, Volume 36, 26th International Conference on Rewriting Techniques and Applications (RTA 2015)

Abstract
We present a coinductive framework for defining infinitary analogues of equational reasoning and rewriting in a uniform way. The setup captures rewrite sequences of arbitrary ordinal length, but it has neither the need for ordinals nor for metric convergence. This makes the framework especially suitable for formalizations in theorem provers.
Cite as

Jörg Endrullis, Helle Hvid Hansen, Dimitri Hendriks, Andrew Polonsky, and Alexandra Silva. A Coinductive Framework for Infinitary Rewriting and Equational Reasoning. In 26th International Conference on Rewriting Techniques and Applications (RTA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 36, pp. 143-159, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{endrullis_et_al:LIPIcs.RTA.2015.143,
  author =	{Endrullis, J\"{o}rg and Hansen, Helle Hvid and Hendriks, Dimitri and Polonsky, Andrew and Silva, Alexandra},
  title =	{{A Coinductive Framework for Infinitary Rewriting and Equational Reasoning}},
  booktitle =	{26th International Conference on Rewriting Techniques and Applications (RTA 2015)},
  pages =	{143--159},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-85-9},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{36},
  editor =	{Fern\'{a}ndez, Maribel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2015.143},
  URN =		{urn:nbn:de:0030-drops-51949},
  doi =		{10.4230/LIPIcs.RTA.2015.143},
  annote =	{Keywords: infinitary rewriting, coinduction}
}
Document
DOI: 10.4230/LIPIcs.RTA.2010.85
Unique Normal Forms in Infinitary Weakly Orthogonal Rewriting

Authors: Joerg Endrullis, Clemens Grabmayer, Dimitri Hendriks, Jan Willem Klop, and Vincent van Oostrom

Published in: LIPIcs, Volume 6, Proceedings of the 21st International Conference on Rewriting Techniques and Applications (2010)

Abstract
We present some contributions to the theory of infinitary rewriting for weakly orthogonal term rewrite systems, in which critical pairs may occur provided they are trivial. We show that the infinitary unique normal form property (UNinf) fails by a simple example of a weakly orthogonal TRS with two collapsing rules. By translating this example, we show that UNinf also fails for the infinitary lambda-beta-eta-calculus. As positive results we obtain the following: Infinitary confluence, and hence UNinf, holds for weakly orthogonal TRSs that do not contain collapsing rules. To this end we refine the compression lemma. Furthermore, we consider the triangle and diamond properties for infinitary developments in weakly orthogonal TRSs, by refining an earlier cluster-analysis for the finite case.
Cite as

Joerg Endrullis, Clemens Grabmayer, Dimitri Hendriks, Jan Willem Klop, and Vincent van Oostrom. Unique Normal Forms in Infinitary Weakly Orthogonal Rewriting. In Proceedings of the 21st International Conference on Rewriting Techniques and Applications. Leibniz International Proceedings in Informatics (LIPIcs), Volume 6, pp. 85-102, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{endrullis_et_al:LIPIcs.RTA.2010.85,
  author =	{Endrullis, Joerg and Grabmayer, Clemens and Hendriks, Dimitri and Klop, Jan Willem and van Oostrom, Vincent},
  title =	{{Unique Normal Forms in Infinitary Weakly Orthogonal Rewriting}},
  booktitle =	{Proceedings of the 21st International Conference on Rewriting Techniques and Applications},
  pages =	{85--102},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-18-7},
  ISSN =	{1868-8969},
  year =	{2010},
  volume =	{6},
  editor =	{Lynch, Christopher},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2010.85},
  URN =		{urn:nbn:de:0030-drops-26469},
  doi =		{10.4230/LIPIcs.RTA.2010.85},
  annote =	{Keywords: Weakly orthogonal term rewrite systems, unique normal form property, infinitary rewriting, infinitary lambda-beta-eta-calculus,}
}
  • Refine by Author
  • 2 Hendriks, Dimitri
  • 1 Endrullis, Joerg
  • 1 Endrullis, Jörg
  • 1 Grabmayer, Clemens
  • 1 Hansen, Helle Hvid
  • Show More...

  • Refine by Classification

  • Refine by Keyword
  • 2 infinitary rewriting
  • 1 Weakly orthogonal term rewrite systems
  • 1 coinduction
  • 1 infinitary lambda-beta-eta-calculus,
  • 1 unique normal form property

  • Refine by Type
  • 2 document

  • Refine by Publication Year
  • 1 2010
  • 1 2015

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