Document Open Access Logo

Confluence of an Extension of Combinatory Logic by Boolean Constants

Author Lukasz Czajka

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSCD.2017.14.pdf
  • Filesize: 0.5 MB
  • 16 pages

Document Identifiers

Subject Classification

Keywords
  • combinatory logic
  • conditional linearization
  • unique normal form property
  • confluence

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

We show confluence of a conditional term rewriting system CL-pc^1, which is an extension of Combinatory Logic by Boolean constants. This solves problem 15 from the RTA list of open problems. The proof has been fully formalized in the Coq proof assistant.

Cite As Get BibTex

Lukasz Czajka. Confluence of an Extension of Combinatory Logic by Boolean Constants. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 14:1-14:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017) https://doi.org/10.4230/LIPIcs.FSCD.2017.14

Author Details

Lukasz Czajka

References

  1. F. Baader and T. Nipkow. Term Rewriting and All That. Cambridge University Press, 1999. Google Scholar
  2. P. Chew. Unique normal forms in term rewriting systems with repeated variables. In STOC '81, pages 7-18. ACM, 1981. Google Scholar
  3. Ł. Czajka and C. Kaliszyk. Hammer for Coq: Automation for dependent type theory. Submitted. Available at http://cl-informatik.uibk.ac.at/cek/coqhammer/, 2017.
  4. R. C. de Vrijer. Conditional linearization. Indagationes Mathematicae, 10(1):145-159, 1999. Google Scholar
  5. N. Dershowitz, J.-P. Jouannaud, and J. W. Klop. Open problems in rewriting. In RTA '91, pages 445-456, 1991. Google Scholar
  6. S. Kahrs and C. Smith. Non-omega-overlapping TRSs are UN. In FSCD 2016, pages 22:1-22:17, 2016. Google Scholar
  7. J. W. Klop. Combinatory reduction systems, volume 127 of Mathematical Centre Tracts. Amsterdam, 1980. Google Scholar
  8. J. W. Klop and R. C. de Vrijer. Unique normal forms for lambda calculus with surjective pairing. Inf. and Comp., 80(2):97-113, 1989. Google Scholar
  9. K. Mano and M. Ogawa. Unique normal form property of compatible term rewriting systems: a new proof of Chew’s theorem. Theor. Comp. Sci., 258(1):169-208, 2001. Google Scholar
  10. K. Støvring. Extending the extensional lambda calculus with surjective pairing is conservative. Logical Methods in Computer Science, 2(2), 2006. Google Scholar
  11. Terese. Term Rewriting Systems. Cambridge University Press, 2003. Google Scholar
  12. Y. Toyama and M. Oyamaguchi. Church-Rosser property and unique normal form property of non-duplicating term rewriting systems. In CTRS-94, pages 316-331, 1995. Google Scholar
  13. R. Verma. Unique normal forms for nonlinear term rewriting systems: Root overlaps. In FCT '97, pages 452-462. Springer, 1997. Google Scholar
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact