# On properties of $B$-terms

## TL;DR

This paper explores the cyclic properties of $B$-terms, providing conditions for when they cycle under right application, and introduces an efficient algorithm to detect such cycles.

## Contribution

It offers a sound and complete axiomatization for identifying cyclic $B$-terms and presents an algorithm for detecting cycles in their canonical representations.

## Key findings

- Existence of infinitely many non-cyclic $B$-terms.
- Examples of cyclic $B$-terms.
- An efficient algorithm for cycle detection.

## Abstract

$B$-terms are built from the $B$ combinator alone defined by $B\equiv\lambda 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.