Document Open Access Logo

Weakening the Axiom of Overlap in Infinitary Lambda Calculus

Authors Paula Severi, Fer-Jan de Vries



PDF
Thumbnail PDF

File

LIPIcs.RTA.2011.313.pdf
  • Filesize: 0.55 MB
  • 16 pages

Document Identifiers

Author Details

Paula Severi
Fer-Jan de Vries

Cite AsGet BibTex

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)
https://doi.org/10.4230/LIPIcs.RTA.2011.313

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.
Keywords
  • Infinitary Lambda Calculus
  • Confluence
  • Normalization

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
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