2026-07-23T13:57:36Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:9188 2024-03-06T10:43:34Z ddc:004 open_access

On Repetitive Right Application of B-Terms Ikebuchi, Mirai Nakano, Keisuke Combinatory logic B combinator Lambda calculus B-terms are built from the B combinator alone defined by B == lambda f.lambda g.lambda 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 efficient algorithm. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Mirai Ikebuchi and Keisuke Nakano 2018 Is Part Of LIPIcs, Volume 108, 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSCD.2018.18 urn:nbn:de:0030-drops-91882 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.18 eng https://creativecommons.org/licenses/by/3.0/legalcode