# On repetitive right application of B-terms

## TL;DR

This paper explores the cyclical behavior of B-terms under repetitive right application, providing conditions, examples, and an efficient algorithm to detect such properties, advancing understanding of their structural characteristics.

## Contribution

It offers a sound and complete axiomatization for analyzing B-term properties and introduces a canonical form and algorithm for cycle detection.

## Key findings

- Some B-terms have the property of circulation under repetitive right application.
- There are infinitely many B-terms that do not have this property.
- A canonical representation and efficient algorithm for cycle detection are proposed.

## 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 circulates or not. We discuss conditions for B-terms to 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 does 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.