TY - JOUR

T1 - On properties of B-terms

AU - Ikebuchi, Mirai

AU - Nakano, Keisuke

N1 - Funding Information:
We are grateful to Johannes Waldmann and Sebastian Maneth for their fruitful comments on this work at an earlier stage. This work was partially supported by JSPS KAKENHI Grant Number JP17K00007.

PY - 2020

Y1 - 2020

N2 - B-terms are built from the B combinator alone defined by B ≡ λfgx.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 cyclic property and show that there are infinitely many B-terms which do not have the property. Also, we introduce another interesting property about a canonical representation of B-terms that is useful to detect cycles, or equivalently, to prove the cyclic property, with an efficient algorithm.

AB - B-terms are built from the B combinator alone defined by B ≡ λfgx.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 cyclic property and show that there are infinitely many B-terms which do not have the property. Also, we introduce another interesting property about a canonical representation of B-terms that is useful to detect cycles, or equivalently, to prove the cyclic property, with an efficient algorithm.

KW - B combinator

KW - Combinatory logic

KW - Lambda calculus

UR - http://www.scopus.com/inward/record.url?scp=85086886735&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85086886735&partnerID=8YFLogxK

U2 - 10.23638/LMCS-16(2:8)2020

DO - 10.23638/LMCS-16(2:8)2020

M3 - Article

AN - SCOPUS:85086886735

VL - 16

SP - 1

EP - 23

JO - Logical Methods in Computer Science

JF - Logical Methods in Computer Science

SN - 1860-5974

IS - 2

M1 - 8

ER -