On repetitive right application of b-terms

Mirai Ikebuchi, Keisuke Nakano

Research output: Chapter in Book/Report/Conference proceedingConference contribution

1 Citation (Scopus)

Abstract

B-terms are built from the B combinator alone defined by B = ?f.?g.?x.f (g x), which is well-known as a function composition operator. This paper investigates an interesting property of B-terms, that is, whether repetitive right applications of a B-term cycles or not. We discuss conditions for B-terms to have and not to have the property through a sound and complete equational axiomatization. Specifically, we give examples of B-terms which have the property and show that there are infinitely many B-terms which do not have the property. Also, we introduce a canonical representation of B-terms that is useful to detect cycles, or equivalently, to prove the property, with an e cient algorithm.

Original languageEnglish
Title of host publication3rd International Conference on Formal Structures for Computation and Deduction, FSCD 2018
EditorsHelene Kirchner
PublisherSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
ISBN (Electronic)9783959770774
DOIs
Publication statusPublished - 2018 Jul 1
Event3rd International Conference on Formal Structures for Computation and Deduction, FSCD 2018 - Oxford, United Kingdom
Duration: 2018 Jul 92018 Jul 12

Publication series

NameLeibniz International Proceedings in Informatics, LIPIcs
Volume108
ISSN (Print)1868-8969

Other

Other3rd International Conference on Formal Structures for Computation and Deduction, FSCD 2018
Country/TerritoryUnited Kingdom
CityOxford
Period18/7/918/7/12

Keywords

  • B combinator
  • Combinatory logic
  • Lambda calculus

ASJC Scopus subject areas

  • Software

Fingerprint

Dive into the research topics of 'On repetitive right application of b-terms'. Together they form a unique fingerprint.

Cite this