License: Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license (CC BY-NC-ND 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.RTA.2011.313
URN: urn:nbn:de:0030-drops-31312
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2011/3131/
Go to the corresponding LIPIcs Volume Portal

Severi, Paula ; de Vries, Fer-Jan

Weakening the Axiom of Overlap in Infinitary Lambda Calculus

pdf-format:
24.pdf (0.6 MB)

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.

BibTeX - Entry

@InProceedings{severi_et_al:LIPIcs:2011:3131,
  author =	{Paula Severi and Fer-Jan de Vries},
  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 =	{Manfred Schmidt-Schau{\ss}},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2011/3131},
  URN =		{urn:nbn:de:0030-drops-31312},
  doi =		{10.4230/LIPIcs.RTA.2011.313},
  annote =	{Keywords: Infinitary Lambda Calculus, Confluence, Normalization}
}

Keywords: Infinitary Lambda Calculus, Confluence, Normalization
Collection: 22nd International Conference on Rewriting Techniques and Applications (RTA'11)
Issue Date: 2011
Date of publication: 26.04.2011

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI