1628 LABEL:LastPageFeb. 01, 2019Jun. 02, 2020 Nd/.style=solid node,
label=left:#1, minimum size=4pt

# On properties of $B$-terms

Mirai Ikebuchi  Massachusetts Institute of Technology, Cambridge, MA, USA
<EMAIL_ADDRESS>and  Keisuke Nakano  Tohoku University, Sendai, Miyagi, Japan
<EMAIL_ADDRESS>
###### 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.

###### Key words and phrases:

Combinatory logic, B combinator, Lambda calculus

## Introduction

The ‘bluebird’ combinator $B=\lambda{fgx}.~{}f(g~{}x)$ is well known [Sch24,
Cur30a, Smu12] as a bracketing combinator or composition operator, which has a
principal type $(\alpha\to\beta)\to(\gamma\to\alpha)\to\gamma\to\beta$. A
function $B~{}f~{}g$ (also written as $f\circ g$) takes a single argument $x$
and returns the term $f(g~{}x)$. In the general case that $g$ takes $n$
arguments, the composition can be given by $\lambda{x_{1}}\dots
x_{n}.\,f(g~{}x_{1}~{}\dots~{}x_{n})$. We call it the _$n$ -argument
composition_ of $f$ and $g$. Interestingly, the function can be given as
$B^{n}\,f~{}g$ where $e^{n}$ stands for the $n$-fold composition
$\underbrace{e\circ\dots\circ e}_{n}$ of the function $e$, or equivalently
defined by $e^{n}\,x=\underbrace{e~{}(\dots(e}_{n}~{}x))$. This fact can be
shown by an easy induction.

Now we consider the $2$-argument composition expressed as
$B^{2}=\lambda{fgxy}.\,f(g~{}x~{}y)$. From the definition, we have
$B^{2}=B\circ B=B~{}B~{}B$. Note that function application is considered left-
associative, that is, $f~{}a~{}b=(f~{}a)~{}b$. Thus $B^{2}$ is expressed as a
term in which all applications nest to the left, never to the right. We call
such terms flat [Oka03]. We write $X_{\left(k\right)}$ for the flat term
defined by
$\underbrace{X~{}X~{}X~{}\dots~{}X}_{k}=\underbrace{(\dots((X~{}X)~{}X)\dots)~{}X}_{k}$
(that can be written as $I\,X^{\text{\raisebox{1.80835pt}{\texttildelow}}k}$
in Barendregt’s notation [Bar84]). Using this notation, we can write
$B^{2}=B_{\left(3\right)}$.

Okasaki [Oka03] investigated facts about flatness. For example, he shows that
there is no universal combinator $X$ that can represent any combinator by
$X_{\left(k\right)}$ with some $k$. We shall delve into the case of $X=B$.
Consider the $n$-argument composition operator $B^{n}$. We have already seen
that $B^{2}$ is $\beta\eta$-equivalent to the flat term $B_{\left(3\right)}$.
For $n=3$, using
$\underline{f}~{}(\underline{\underline{g}}~{}x)=B~{}f~{}g~{}x$, we have

$\displaystyle B^{3}$ $\displaystyle=B~{}B^{2}~{}B$
$\displaystyle=\underline{B}~{}(\underline{\underline{B~{}B}}~{}B)~{}B$
$\displaystyle=\underline{B~{}B}~{}(\underline{\underline{B}}~{}B)~{}B~{}B$
$\displaystyle=\underline{B}~{}(\underline{\underline{B}}~{}B)~{}B~{}B~{}B~{}B$
$\displaystyle=B~{}B~{}B~{}B~{}B~{}B~{}B~{}B\text{,}$

and thus $B^{3}=B_{\left(8\right)}$. How about the $4$-argument composition
$B^{4}$? In fact, there is no integer $k$ such that $B^{4}=B_{\left(k\right)}$
with respect to $\beta\eta$-equality. Moreover, for any $n>3$, there does not
exist $k$ such that $B^{n}=B_{\left(k\right)}$. This surprising fact is proved
by a quite simple method; listing all $B_{\left(k\right)}$s for $k=1,2,\dots$
and checking that none of them is equivalent to $B^{n}$. An easy computation
gives
$B_{\left(6\right)}=B_{\left(10\right)}=\lambda{xyzwv}.~{}x~{}(y~{}z)~{}(w~{}v)$,
and hence $B_{\left(i\right)}=B_{\left(i+4\right)}$ for every $i\geq 6$. Then,
by computing $B_{\left(k\right)}$s only for $k\in\\{1,2,\dots,6\\}$, we can
check that $B_{\left(k\right)}$ is not $\beta\eta$-equivalent to $B^{n}$ with
$n>3$ for $k\in\\{1,2,\dots\\}$. Thus we conclude that there is no integer $k$
such that $B^{n}=B_{\left(k\right)}$.

This is the starting point of our research. We say that a combinator $X$ has
the $\rho$-property if there exist two distinct integers $i$ and $j$ such that
$X_{\left(i\right)}=X_{\left(j\right)}$. In this case, we have
$X_{\left(i+k\right)}=X_{\left(j+k\right)}$ for any $k\geq 0$ (à la _finite
monogenic semigroup_ [Lja68]). Fig. 1 shows a computation graph of
$B_{\left(k\right)}$. The $\rho$-property is named after the shape of the
graph.

$B_{\left(1\right)}$$B_{\left(2\right)}$$B_{\left(3\right)}$$B_{\left(4\right)}$$B_{\left(5\right)}$$B_{\left(6\right)}$$(=B_{\left(10\right)}=B_{\left(14\right)}=\dots)$$B_{\left(7\right)}$$(=B_{\left(11\right)}=B_{\left(15\right)}=\dots)$$B_{\left(9\right)}$$(=B_{\left(13\right)}=B_{\left(17\right)}=\dots)$$B_{\left(8\right)}$$(=B_{\left(12\right)}=B_{\left(16\right)}=\dots)$
Figure 1. $\rho$-property of the $B$ combinator

This paper discusses the $\rho$-property of combinatory terms, particularly
terms built from $B$ alone. We call such terms $B$-terms and $\mathbf{CL}(B)$
denotes the set of all $B$-terms. For example, the $B$-term $B~{}B$ enjoys the
$\rho$-property with $(B~{}B)_{\left(52\right)}=(B~{}B)_{\left(32\right)}$ and
so does $B~{}(B~{}B)$ with
$(B~{}(B~{}B))_{\left(294\right)}=(B~{}(B~{}B))_{\left(258\right)}$ as
reported in [Nak08]. Several combinators other than $B$-terms can be found to
enjoy the $\rho$-property, for example, $K=\lambda{xy}.~{}x$ and
$C=\lambda{xyz}.~{}x~{}z~{}y$ because of
$K_{\left(3\right)}=K_{\left(1\right)}$ and
$C_{\left(4\right)}=C_{\left(3\right)}$. They are less interesting in the
sense that the cycle starts immediately and its size is very small, comparing
with $B$-terms like $B~{}B$ and $B~{}(B~{}B)$. As we will see later,
$B~{}(B~{}(B~{}(B~{}(B~{}(B~{}B)))))(\equiv B^{6}~{}B)$ has the
$\rho$-property with the cycle of size more than $3\times 10^{11}$ which
starts after more than $2\times 10^{12}$ repetitive right applications. This
is why the $\rho$-property of $B$-terms is intensively discussed in the
present paper. A general definition of the $\rho$-property is presented in
Section 1.

The contributions of the paper are two-fold. One is to give a characterization
of $\mathbf{CL}(B)$ (Section 2) and another is to provide a sufficient
condition for the $\rho$-property and anti-$\rho$-property of $B$-terms
(Section 3). In the former, we introduce a canonical representation of
$B$-terms and establish a sound and complete equational axiomatization for
$\mathbf{CL}(B)$. In the latter, the $\rho$-property of $B^{n}B$ with $n\leq
6$ is shown with an efficient algorithm and the anti-$\rho$-property for
$B$-terms of particular forms is proved.

This paper extends and refines our paper presented in FSCD 2018 [IN18].
Compared to our previous work, we have made several improvements. First, we
add relationships to the existing work, the Curry’s compositive normal form
and the Thompson’s group. Second, we report progress on proving and disproving
the $\rho$-property of $B$-terms. For proving the $\rho$-property, we add more
precise information on the implementation of our $\rho$-property checker. For
disproving the $\rho$-property, we introduce another proof method for a
specific $B$-term and expand the set of $B$-terms which are known not to have
the $\rho$-property. Furthermore, we discuss other possible approaches for
further steps to show a conjecture by the second author [Nak08].

##  1\. The $\rho$-property of terms

The $\rho$-property of a combinator $X$ is that
$X_{\left(i\right)}=X_{\left(i+j\right)}$ holds for some $i,j\geq 1$. We adopt
$\beta\eta$-equality of corresponding $\lambda$-terms for the equality of
combinatory terms in this paper. We could use another equality, for example,
induced by the axioms of combinatory logic. The choice of equality is not
essential here, e.g., $B_{\left(9\right)}$ and $B_{\left(13\right)}$ are equal
even up to the combinatory axiom of $B$, as well as $\beta\eta$-equality. (See
Section 4 for more details.) Furthermore, for simplicity, we only deal with
the case where $X_{\left(n\right)}$ is normalizable for all $n$. If
$X_{\left(n\right)}$ is not normalizable, it is much more difficult to check
equivalence with the other terms. This restriction does not affect the results
of the paper because all $B$-terms are normalizing.

Let us write $\rho(X)=(i,j)$ if a combinator $X$ has the $\rho$-property due
to $X_{\left(i\right)}=X_{\left(i+j\right)}$ with minimum positive integers
$i$ and $j$. For example, we have $\rho(B)=(6,4)$, $\rho(C)=(3,1)$,
$\rho(K)=(1,2)$ and $\rho(I)=(1,1)$. Besides them, several combinators
introduced in Smullyan’s book [Smu12] have the $\rho$-property:

$\displaystyle\rho(D)$ $\displaystyle=(32,20)$ where
$D=\lambda{xyzw}.\,x~{}y~{}(z~{}w)$ $\displaystyle\rho(F)$
$\displaystyle=(3,1)$ where $F=\lambda{xyz}.\,z~{}y~{}x$
$\displaystyle\rho(R)$ $\displaystyle=(3,1)$ where
$R=\lambda{xyz}.\,y~{}z~{}x$ $\displaystyle\rho(T)$ $\displaystyle=(2,1)$
where $T=\lambda{xy}.\,y~{}x$ $\displaystyle\rho(V)$ $\displaystyle=(3,1)$
where $V=\lambda{xyz}.\,z~{}x~{}y$.

Except for the $B$ and $D~{}(=B~{}B)$ combinators, the property is ‘trivial’
in the sense that the loop starts early and the size of the cycle is very
small.

On the other hand, the combinators $S=\lambda{xyz}.\,x~{}z~{}(y~{}z)$ and
$O=\lambda{xy}.\,y~{}(x~{}y)$ in the book do not have the $\rho$-property
since their right application expands the $\lambda$-terms as illustrated by

$\displaystyle S_{\left(2n+1\right)}$
$\displaystyle=\lambda{xy}.\,\underbrace{x~{}y~{}(x~{}y~{}(\dots(x~{}y}_{n}~{}(\lambda
z.x~{}z~{}(y~{}z)))\dots))\text{,}$ $\displaystyle O_{\left(n+1\right)}$
$\displaystyle=\lambda x.\underbrace{x~{}(x~{}(\dots(x~{}}_{n}~{}(\lambda
y.y~{}(x~{}y))\text{.}$

The definition of the $\rho$-property is naturally extended from single
combinators to terms obtained by combining several combinators. We found by
computation that several $B$-terms have the $\rho$-property as shown below.

$\displaystyle\rho(B^{0}B)$ $\displaystyle=(6,4)$ $\displaystyle\rho(B^{4}B)$
$\displaystyle=(191206,431453)$ $\displaystyle\rho(B^{1}B)$
$\displaystyle=(32,20)$ $\displaystyle\rho(B^{5}B)$
$\displaystyle=(766241307,234444571)$ $\displaystyle\rho(B^{2}B)$
$\displaystyle=(258,36)$ $\displaystyle\rho(B^{6}B)$
$\displaystyle=(2641033883877,339020201163)$ $\displaystyle\rho(B^{3}B)$
$\displaystyle=(4240,5796)$

The details will be shown in Section 3.1.

From his observation on repetitive right applications for several $B$-terms,
Nakano [Nak08] has conjectured as follows.

######  Conjecture 1.

A $B$-term $e$ has the $\rho$-property if and only if $e$ is a monomial, i.e.,
$e$ is equivalent to $B^{n}B$ with $n\geq 0$.

The definition of _monomial_ will be given in Section 2.3 in the context of a
canonical representation of $B$-terms. The “if” part of the conjecture for
$n\leq 6$ is shown by the above results; the “only if” part will be shown for
specific $B$ terms which will be discussed Section 3.2. Note that the
$\rho$-property of $X$ can be rephrased in terms of the set generated by right
application, that is, the finiteness of the set
$\\{\mathit{nf}(X_{\left(n\right)})\mid n\geq 1\\}$ where $\mathit{nf}(e)$
represents the normal form of $e$. Conjecture 1 claims that for any $B$-term
$e$, the finiteness of the set $\\{\mathit{nf}(e_{\left(n\right)})\mid n\geq
1\\}$ is decidable since so is the word problem of $B$-terms.

##  2\. Checking equivalence of $B$-terms

The set of all $B$-terms, $\mathbf{CL}(B)$, is closed under application by
definition, that is, the repetitive right application of a $B$-term always
generates a sequence of $B$-terms. Hence, the $\rho$-property can be decided
by checking ‘equivalence’ among generated $B$-terms, where the equivalence
should be checked through $\beta\eta$-equivalence of their corresponding
$\lambda$-terms in accordance with the definition of the $\rho$-property. It
would be useful if we have a fast algorithm for deciding equivalence over
$B$-terms.

In this section, we give a characterization of the $B$-terms to efficiently
decide their equivalence. We introduce a method for deciding equivalence of
$B$-terms without calculating the corresponding $\lambda$-terms. To this end,
we first investigate equivalence over $B$-terms with examples and then present
an equation system as a characterization of $B$-terms so as to decide
equivalence between two $B$-terms. Based on the equation system, we introduce
a canonical representation of $B$-terms. The representation makes it easy to
observe the growth caused by repetitive right application of $B$-terms, which
will be later used for proving the anti-$\rho$-property of $B^{2}$. We believe
that this representation will be helpful to prove the $\rho$-property or the
anti-$\rho$-property for the other $B$-terms.

###  2.1. Equivalence over $B$-terms

Two $B$-terms are said to be _equivalent_ if their corresponding
$\lambda$-terms are $\beta\eta$-equivalent. For instance, $B~{}B~{}(B~{}B)$
and $B~{}(B~{}B)~{}B~{}B$ are equivalent. This can be shown by the definition
$B~{}x~{}y~{}z=x~{}(y~{}z)$. For another (non-trivial) instance,
$B~{}B~{}(B~{}B)$ and $B~{}(B~{}(B~{}B))~{}B$ are equivalent. This is
illustrated by the fact that they are equivalent to
$\lambda{xyzwv}.\,x~{}(y~{}z)~{}(w~{}v)$ where $B$ is replaced with
$\lambda{xyz}.\,x~{}(y~{}z)$ or the other way around at the $=_{\beta}$
equation. Similarly, it is hard to directly show equivalence between the two
$B$-terms, $B~{}(B~{}B)~{}(B~{}B)$ and $B~{}(B~{}B~{}B)$, which requires long
calculation like:

$\displaystyle B~{}B~{}(B~{}B)$ $\displaystyle=_{\eta}\lambda
x.B~{}B~{}(B~{}B)~{}x$ $\displaystyle=_{\beta}\lambda x.B~{}(B~{}B~{}x)$
$\displaystyle=_{\eta}\lambda{xy}.B~{}(B~{}B~{}x)~{}y$
$\displaystyle=_{\eta}\lambda{xyz}.B~{}(B~{}B~{}x)~{}y~{}z$
$\displaystyle=_{\beta}\lambda{xyz}.B~{}B~{}x~{}(y~{}z)$
$\displaystyle=_{\beta}\lambda{xyz}.B~{}(x~{}(y~{}z))$
$\displaystyle=_{\beta}\lambda{xyz}.B~{}(B~{}x~{}y~{}z)$
$\displaystyle=_{\beta}\lambda{xyz}.B~{}B~{}(B~{}x~{}y)~{}z$
$\displaystyle=_{\eta}\lambda{xy}.B~{}B~{}(B~{}x~{}y)$
$\displaystyle=_{\beta}\lambda{xy}.B~{}(B~{}B)~{}(B~{}x)~{}y$
$\displaystyle=_{\eta}\lambda x.B~{}(B~{}B)~{}(B~{}x)$
$\displaystyle=_{\beta}\lambda x.B~{}(B~{}(B~{}B))~{}B~{}x$
$\displaystyle=_{\eta}B~{}(B~{}(B~{}B))~{}B\mbox{.}$

This kind of equality makes it hard to investigate the $\rho$-property of
$B$-terms. To solve this annoying issue, we will introduce a canonical
representation of $B$-terms in Section 2.3.

###  2.2. Equational axiomatization for $B$-terms

Equality between two $B$-terms can be decided through their canonical
representation introduced in Section 2.3. The representation is based on a
sound and complete equation system as described in the next theorem.

######  Theorem 2.

Two $B$-terms are $\beta\eta$-equivalent if and only if their equality is
derived from the following equations:

$\displaystyle B~{}x~{}y~{}z$ $\displaystyle=x~{}(y~{}z)$ (B1) $\displaystyle
B~{}(B~{}x~{}y)$ $\displaystyle=B~{}(B~{}x)~{}(B~{}y)$ (B2) $\displaystyle
B~{}B~{}(B~{}x)$ $\displaystyle=B~{}(B~{}(B~{}x))~{}B$ (B3)

The proof of the “if” part, which corresponds to the soundness of the equation
system (B1), (B2), and (B3), is given here. We will later prove the “only if”
part with the uniqueness of the canonical representation of $B$-terms.

######  Proof 2.1.

Equation (B1) is immediate from the definition of $B$. Equations (B2) and (B3)
are shown by

$\displaystyle B~{}(B~{}e_{1}~{}e_{2})$
$\displaystyle=\lambda{xy}.\,B~{}(B~{}e_{1}~{}e_{2})~{}x~{}y$ $\displaystyle
B~{}B~{}(B~{}e_{1})$ $\displaystyle=\lambda x.\,B~{}B~{}(B~{}e_{1})~{}x$
$\displaystyle=\lambda{xy}.\,B~{}e_{1}~{}e_{2}~{}(x~{}y)$
$\displaystyle=\lambda x.\,B~{}(B~{}e_{1}~{}x)$
$\displaystyle=\lambda{xy}.\,e_{1}~{}(e_{2}~{}(x~{}y))$
$\displaystyle=\lambda{xyz}.\,B~{}e_{1}~{}x(y~{}z)$
$\displaystyle=\lambda{xy}.\,e_{1}~{}(B~{}e_{2}~{}x~{}y)$
$\displaystyle=\lambda{xyz}.\,e_{1}~{}(x~{}(y~{}z))$ $\displaystyle=\lambda
x.\,B~{}e_{1}~{}(B~{}e_{2}~{}x)$
$\displaystyle=\lambda{xyz}.\,e_{1}~{}(B~{}x~{}y~{}z)$
$\displaystyle=B~{}(B~{}e_{1})~{}(B~{}e_{2})$
$\displaystyle=\lambda{xy}.\,B~{}e_{1}~{}(B~{}x~{}y)$ $\displaystyle=\lambda
x.\,B~{}(B~{}e_{1})~{}(B~{}x)$ $\displaystyle=B~{}(B~{}(B~{}e_{1}))~{}B$

where the $\alpha$-renaming is implicitly used.

Equation (B2) has been employed by Statman [Sta11] to show that no
$B\omega$-term can be a fixed-point combinator where $\omega=\lambda
x.\,x~{}x$. This equation exposes an interesting feature of the $B$
combinator. Write equation (B2) as

$\displaystyle B~{}(e_{1}\circ e_{2})=(B~{}e_{1})\circ(B~{}e_{2})$ (B2’)

by replacing every $B$ combinator with $\circ$ infix operator if it has
exactly two arguments. The equation is a distributive law of $B$ over $\circ$,
which will be used to obtain the canonical representation of $B$-terms.
Equation (B3) is also used for the same purpose as the form of

$\displaystyle B\circ(B~{}e_{1})=(B~{}(B~{}e_{1}))\circ B\text{.}$ (B3’)

We also have a natural equation
$B~{}e_{1}~{}(B~{}e_{2}~{}e_{3})=B~{}(B~{}e_{1}~{}e_{2})~{}e_{3}$ which
represents associativity of function composition, i.e., $e_{1}\circ(e_{2}\circ
e_{3})=(e_{1}\circ e_{2})\circ e_{3}$. This is shown with equations (B1) and
(B2) by

$B~{}e_{1}~{}(B~{}e_{2}~{}e_{3})=B~{}(B~{}e_{1})~{}(B~{}e_{2})~{}e_{3}=B~{}(B~{}e_{1}~{}e_{2})~{}e_{3}.$

###  2.3. Canonical representation of $B$-terms

To decide equality between two $B$-terms, it does not suffice to compute their
normal forms under the definition of $B$, $B~{}x~{}y~{}z\to x~{}(y~{}z)$. This
is because two distinct normal forms may be equal up to
$\beta\eta$-equivalence, e.g., $B~{}B~{}(B~{}B)$ and $B~{}(B~{}(B~{}B))~{}B$.
We introduce a canonical representation of $B$-terms, which makes it easy to
check equivalence of $B$-terms. We will eventually find that for any $B$-term
$e$ there exists a unique finite non-empty weakly-decreasing sequence of non-
negative integers $n_{1}\geq n_{2}\geq\dots\geq n_{k}$ such that $e$ is
equivalent to $(B^{n_{1}}B)\circ(B^{n_{2}}B)\circ\dots\circ(B^{n_{k}}B)$.
Ignoring the inequality condition gives _polynomials_ introduced by Statman
[Sta11]. We will use these _decreasing polynomials_ for our canonical
representation as presented later. A similar result is found in [Cur30b] as
discussed later.

First, we explain how this canonical form is obtained from a $B$-term. We only
need to consider $B$-terms in which every $B$ has at most two arguments. One
can reduce the arguments of $B$ to less than three by repeatedly rewriting
occurrences of $B~{}e_{1}~{}e_{2}~{}e_{3}~{}e_{4}~{}\dots~{}e_{n}$ into
$e_{1}~{}(e_{2}~{}e_{3})~{}e_{4}~{}\dots~{}e_{n}$. The rewriting procedure
always terminates because it reduces the number of $B$. Thus, every $B$-term
in $\mathbf{CL}(B)$ is equivalent to a $B$-term built by the syntax

$\displaystyle e$ $\displaystyle::=B~{}\mid~{}B~{}e~{}\mid~{}e~{}\circ~{}e$
(1)

where $e_{1}\circ e_{2}$ denotes $B~{}e_{1}~{}e_{2}$. We prefer to use the
infix operator $\circ$ instead of $B$ that has two arguments because
associativity of $B$, that is,
$B~{}e_{1}~{}(B~{}e_{2}~{}e_{3})=B~{}(B~{}e_{1}~{}e_{2})~{}e_{3}$ can be
implicitly assumed. This simplifies the further discussion on $B$-terms. We
will deal with only $B$-terms in syntax (1) from now on. The $\circ$ operator
has lower precedence than application in this paper, e.g., terms $B~{}B\circ
B$ and $B\circ B~{}B$ represent $(B~{}B)\circ B$ and $B\circ(B~{}B)$,
respectively.

The syntactic restriction by (1) does not suffice to proffer a canonical
representation of $B$-terms. For example, both of the two $B$-terms $B\circ
B~{}B$ and $B~{}(B~{}B)\circ B$ are given in the form of (1), but we can see
that they are equivalent using (B3’).

A _polynomial form of $B$-terms_ is obtained by putting a restriction on the
syntax so that no $B$ combinator occurs outside of the $\circ$ operator while
syntax (1) allows the $B$ combinators and the $\circ$ operators to occur in an
arbitrary position. The restricted syntax is given as

$\displaystyle e::=e_{B}~{}\mid~{}e\circ e\qquad e_{B}::=B~{}\mid B~{}e_{B}$

where terms in $e_{B}$ have a form of $B(\dots(B(B~{}B))\dots)$, that is
$B^{n}B$ with some $n$, called _monomial_. The syntax can be simply rewritten
into $e\mathbin{::=}B^{n}B~{}\mid~{}e\circ e$, which is called _polynomial_.

A $B$-term $B^{n}B$ is called _monomial_. A _polynomial_ is a $B$-term given
in the form of

$\displaystyle(B^{n_{1}}B)\circ(B^{n_{2}}B)\circ\dots\circ(B^{n_{k}}B)$

where $k>0$ and $n_{1},\dots,n_{k}\geq 0$ are integers. In particular, a
polynomial is called _decreasing_ when $n_{1}\geq n_{2}\geq\dots\geq n_{k}$.
The _length_ of a polynomial $P$ is the number of monomials in $P$, i.e., the
length of the polynomial above is $k$. The numbers $n_{1},n_{2},\dots,n_{k}$
are called _degrees_.

In the rest of this subsection, we prove that for any $B$-term $e$ there
exists a unique decreasing polynomial equivalent to $e$. First, we show that
$e$ has an equivalent polynomial.

[[Sta11]] For any $B$-term $e$, there exists a polynomial equivalent to $e$.

######  Proof 2.2.

We prove the statement by induction on the structure of $e$. In the case of
$e\equiv B$, the term itself is polynomial. In the case of $e\equiv
B~{}e_{1}$, assume that $e_{1}$ has equivalent polynomial
$(B^{n_{1}}B)\circ(B^{n_{2}}B)\circ\dots\circ(B^{n_{k}}B)$. Repeatedly
applying equation (B2’) to $B~{}e_{1}$, we obtain a polynomial equivalent to
$B~{}e_{1}$ as
$(B^{n_{1}+1}B)\circ(B^{n_{2}+1}B)\circ\dots\circ(B^{n_{k}+1}B)$. In the case
of $e\equiv e_{1}\circ e_{2}$, assume that $e_{1}$ and $e_{2}$ have equivalent
polynomials $P_{1}$ and $P_{2}$, respectively. A polynomial equivalent to $e$
is given by $P_{1}\circ P_{2}$.

Next, we show that for any polynomial $P$ there exists a decreasing polynomial
equivalent to $P$. A key equation of the proof is

$\displaystyle(B^{m}B)\circ(B^{n}B)$
$\displaystyle=(B^{n+1}B)\circ(B^{m}B)\quad\text{when~{}$m<n$,}$ (2)

which is shown by

$\displaystyle(B^{m}B)\circ(B^{n}B)$ $\displaystyle=B^{m}(B\circ(B^{n-m}B))$
$\displaystyle=B^{m}(B\circ(B~{}(B^{n-m-1}B)))$
$\displaystyle=B^{m}((B(B(B^{n-m-1}B)))\circ B)$
$\displaystyle=(B^{n+1}B)\circ(B^{m}B)$

using equations (B2’) and (B3’).

######  Lemma 3.

Any polynomial $P$ has an equivalent decreasing polynomial $P^{\prime}$ such
that

  * •

the length of $P$ and $P^{\prime}$ are equal, and

  * •

the lowest degrees of $P$ and $P^{\prime}$ are equal.

######  Proof 2.3.

We prove the statement by induction on the length of $P$. When the length is
1, that is, $P$ is a monomial, $P$ itself is decreasing and the statement
holds. When the length $k$ of $P$ is greater than 1, take $P_{1}$ such that
$P\equiv P_{1}\circ(B^{n}B)$. From the induction hypothesis, there exists a
decreasing polynomial
$P_{1}^{\prime}\equiv(B^{n_{1}}B)\circ(B^{n_{2}}B)\circ\dots\circ(B^{n_{k-1}}B)$
equivalent to $P_{1}$, and the lowest degree of $P_{1}$ is $n_{k-1}$. If
$n_{k-1}\geq n$, then $P^{\prime}\equiv P_{1}^{\prime}\circ(B^{n}~{}B)$ is
decreasing and equivalent to $P$. Since the lowest degrees of $P$ and
$P^{\prime}$ are $n$, the statement holds. If $n_{k-1}<n$, $P$ is equivalent
to

$\displaystyle(B^{n_{1}}~{}B)\circ\dots\circ(B^{n_{k-1}}B)\circ(B^{n}B)$
$\displaystyle=(B^{n_{1}}B)\circ\dots\circ(B^{n+1}B)\circ(B^{n_{k-1}}B)$

due to equation (2). Putting the last term as $P_{2}\circ(B^{n_{k-1}}B)$, the
length of $P_{2}$ is $k-1$ and the lowest degree of $P_{2}$ is greater than or
equal to $n_{k-1}$. From the induction hypothesis, $P_{2}$ has an equivalent
decreasing polynomial $P_{2}^{\prime}$ of length $k-1$ and the lowest degree
of $P_{2}^{\prime}$ greater than or equal to $n_{k-1}$. Thereby we obtain a
decreasing polynomial $P_{2}^{\prime}\circ(B^{n_{k-1}}B)$ equivalent to $P$
and the statement holds.

Consider a $B$-term $e=B~{}(B~{}B~{}B)~{}(B~{}B)~{}B$. First, applying
equation (B1),

$\displaystyle e$
$\displaystyle=B~{}(B~{}B~{}B)~{}(B~{}B)~{}(B~{}B)=B~{}B~{}B~{}(B~{}B~{}(B~{}B))=B~{}(B~{}(B~{}B~{}(B~{}B)))$

so that every $B$ has at most two arguments. Then replacing each two-argument
$B$ to the infix $\circ$ operator, obtain $B~{}(B~{}(B\circ(B~{}B)))$.
Applying equation (B2’), we have

$\displaystyle B~{}(B~{}(B\circ(B~{}B)))$
$\displaystyle=B~{}((B~{}B)\circ(B~{}(B~{}B)))$
$\displaystyle=(B~{}(B~{}B))\circ(B~{}(B~{}(B~{}B)))$
$\displaystyle=(B^{2}B)\circ(B^{3}B)\text{.}$

Applying equation (2), we obtain the decreasing polynomial
$(B^{4}B)\circ(B^{2}B)$ equivalent to $e$.

Every $B$-term has at least one equivalent decreasing polynomial as shown so
far. To conclude this subsection, we show the uniqueness of decreasing
polynomial equivalent to any $B$-term, that is, every $B$-term $e$ has no two
distinct decreasing polynomials equivalent to $e$.

The proof is based on the idea that $B$-terms correspond to unlabeled binary
trees. Let $M$ be a term which is constructed from variables
$x_{1},\dots,x_{k}$ and their applications. Then we can show that if the
$\lambda$-term $\lambda x_{1}.\dots x_{k}.\,M$ is in $\mathbf{CL}(B)$, then
$M$ is obtained by putting parentheses to some positions in the sequence
$x_{1}~{}\dots~{}x_{k}$. More precisely, we have the following lemma.

######  Lemma 4.

Every $B$-term is $\beta\eta$-equivalent to a $\lambda$-term of the form
$\lambda x_{1}.\dots x_{k}.~{}M$ with some $k>2$ where $M$ satisfies the
following two conditions: (1) $M$ consists of only the variables
$x_{1},\dots,x_{k}$ and their applications, and (2) for every subterm of $M$
which is in the form of $M_{1}~{}M_{2}$, if $M_{1}$ has a variable $x_{i}$,
then $M_{2}$ does not have any variable $x_{j}$ with $j\leq i$.

######  Proof 2.4.

We prove the statement by induction. In the case of $e\equiv B$, $e$ is
equivalent to $\lambda{x_{1}x_{2}x_{3}}.\,x_{1}(x_{2}x_{3})$, the statement
holds. In the case of $e\equiv B~{}e_{1}$, $e$ is equivalent to
$\lambda{x_{1}x_{2}}.\,e_{1}~{}(x_{1}~{}x_{2})$. From the induction
hypothesis, $e_{1}$ is equivalent to $\lambda{x_{1}x_{2}}\dots
x_{k}.\,e_{1}^{\prime}$ where $e_{1}^{\prime}$ satisfies the conditions (1)
and (2). Then, we can see that
$e_{1}^{\prime}\left[(x_{1}~{}x_{2})/x_{1}\right]$ also satisfies the
conditions (1) and (3).

From this lemma, we see that we do not need to specify variables in $M$ and we
can simply write like
$\star~{}\star~{}(\star~{}\star)=~{}x_{1}~{}x_{2}~{}(x_{3}~{}x_{4})$. Formally
speaking, every $\lambda$-term in $\mathbf{CL}(B)$ uniquely corresponds to a
term built from $\star$ alone by the map $(\lambda x_{1}\dots
x_{k}.\,M)\mapsto M[\star/x_{1},\dots,\star/x_{k}]$. We say an unlabeled
binary tree (or simply, binary tree) for a term built from $\star$ alone since
every term built from $\star$ alone can be seen as an unlabeled binary tree.
(A term $\star$ corresponds to a leaf and $t_{1}~{}t_{2}$ corresponds to the
tree with left subtree $t_{1}$ and right subtree $t_{2}$.) To specify the
applications in binary trees, we write $\langle t_{1},t_{2}\rangle$ for the
application $t_{1}~{}t_{2}$. For example, $B$-terms
$B=\lambda{xyz}.\,x~{}(y~{}z)$ and $B~{}B=\lambda{xyzw}.\,x~{}y~{}(z~{}w)$ are
represented by $\langle\star,\langle\star,\star\rangle\rangle$ and
$\langle\langle\star,\star\rangle,\langle\star,\star\rangle\rangle$,
respectively.

We will present an algorithm for constructing the corresponding decreasing
polynomial from a given binary tree. First let us define a function
$\mathcal{L}_{i}$ with integer $i$ which maps binary trees to lists of
integers:

$\displaystyle\mathcal{L}_{i}(\star)$ $\displaystyle=[~{}]$
$\displaystyle\mathcal{L}_{i}(\langle t_{1},t_{2}\rangle)$
$\displaystyle=\mathcal{L}_{i+\left|\\!\left|t_{1}\right|\\!\right|}(t_{2})\mathbin{{+}\mspace{-8.0mu}{+}}\mathcal{L}_{i}(t_{1})\mathbin{{+}\mspace{-8.0mu}{+}}[i]$

where $\mathbin{+\\!\\!\\!+}$ concatenates two lists and
$\left|\\!\left|t\right|\\!\right|$ denotes the number of leaves. For example,
$\mathcal{L}_{0}(\langle\langle\star,\star\rangle,\langle\star,\star\rangle\rangle)=[2,0,0]$
and
$\mathcal{L}_{1}(\langle\langle\star,\langle\star,\star\rangle\rangle,\langle\star,\langle\star,\star\rangle\rangle\rangle)=[4,4,2,1,1]$.
Informally, the $\mathcal{L}_{i}$ function returns a list of integers which is
obtained by labeling both leaves and nodes in the following steps. First each
leaf of a given tree is labeled by $i,i+1,i+2,\dots$ in left-to-right order.
Then each internal node of the tree is labeled by the same label as its
leftmost descendant leaf. The $\mathcal{L}_{i}$ functions return a list of
labels of internal nodes in decreasing order. Figure 2 shows three examples of
labeled binary trees obtained by this labeling procedure for $i=-1$. Let
$t_{j}$ ($j=1,2,3$) be the unlabeled binary tree corresponding to $e_{j}$.
From the labeled binary trees in Figure 2, we have
$\mathcal{L}_{-1}(t_{1})=[1,-1,-1]$, $\mathcal{L}_{-1}(t_{2})=[3,1,1,-1,-1]$,
and $\mathcal{L}_{-1}(t_{3})=[5,2,2,2,0,-1,-1,-1]$. One may notice that a
binary tree $t_{3}^{\prime}$ corresponding $\eta$-equivalent terms of $e_{3}$
is obtained by removing the leaf 7 and its root. From
$\mathcal{L}_{-1}(t_{3}^{\prime})\mathbin{{+}\mspace{-8.0mu}{+}}[-1]=\mathcal{L}_{-1}(t_{3})$,
we have $\mathcal{L}(t_{3}^{\prime})=\mathcal{L}(t_{3})$. It is easy to show
that the $\mathcal{L}$ function returns the same values for $\eta$-equivalent
$B$-terms. The length of the list equals the number of nodes, that is, smaller
by one than the number of variables in the $\lambda$-term.

[ ,for tree=s sep=4pt, circle, draw, minimum size=1.5em, inner sep=0pt, font=
,Nd=$-1\\!$, [ ,Nd=$-1\\!$, [$-1$] [$0$] ] [ ,Nd=$1\\!$, [$1$] [$2$] ] ]

(a) Binary tree $t_{1}$ for $\lambda$-term $e_{1}$

[ ,for tree=s sep=10pt, circle, draw, minimum size=1.5em, inner sep=0pt, font=
,Nd=$-1\\!$, [ ,for tree=s sep=4pt ,Nd=$-1\\!$, [$-1$] [$0$] ] [ ,for tree=s
sep=4pt ,Nd=$1\\!$, [ ,Nd=$1\\!\\!\\!\;$, [$1$] [$2$] ] [ ,Nd=$3\\!$, [$3$]
[$4$] ] ] ]

(b) Binary tree $t_{2}$ for $\lambda$-term $e_{2}$

[ ,for tree=s sep=128pt, circle, draw, minimum size=1.5em, inner sep=0pt,
font= ,Nd=$-1\,$, [ ,for tree=s sep=14pt ,Nd=$-1$, [ ,Nd=$-1\\!$, [$-1$] [
,for tree=s sep=4pt ,Nd=$0\\!$, [$0$] [$1$] ] ] [ ,Nd=$2\,$, [ ,for tree=s
sep=16pt ,Nd=$2\\!$, [ ,for tree=s sep=4pt ,Nd=$2\\!$, [$2$] [$3$] ] [$4$] ] [
,for tree=s sep=4pt ,Nd=$5\\!$, [$5$] [$6$] ] ] ] [$7$] ]

(c) Binary tree $t_{3}$ for $\lambda$-term $e_{3}$

$\displaystyle\text{where}\;\,\quad e_{1}$
$\displaystyle=\lambda{x_{1}x_{2}x_{3}x_{4}}.\,x_{1}~{}x_{2}~{}(x_{3}~{}x_{4})$
$\displaystyle e_{2}$
$\displaystyle=\lambda{x_{1}x_{2}x_{3}x_{4}x_{5}x_{6}}.\,x_{1}~{}x_{2}~{}(x_{3}~{}x_{4}~{}(x_{5}~{}x_{6}))$
$\displaystyle e_{3}$
$\displaystyle=\lambda{x_{1}x_{2}x_{3}x_{4}x_{5}x_{6}x_{7}x_{8}x_{9}}.\,x_{1}~{}(x_{2}~{}x_{3})~{}(x_{4}~{}x_{5}~{}x_{6}~{}(x_{7}~{}x_{8}))~{}x_{9}$
$\displaystyle(=_{\eta}\lambda{x_{1}x_{2}x_{3}x_{4}x_{5}x_{6}x_{7}x_{8}}.\,x_{1}~{}(x_{2}~{}x_{3})~{}(x_{4}~{}x_{5}~{}x_{6}~{}(x_{7}~{}x_{8})))$
$\displaystyle\text{and}\quad\mathcal{L}(t_{1})$ $\displaystyle=[1]$
$\displaystyle\mathcal{L}(t_{2})$ $\displaystyle=[3,1,1]$
$\displaystyle\mathcal{L}(t_{3})$ $\displaystyle=[5,2,2,2,0]$

Figure 2. Labeled binary trees

$\mathcal{L}$ is the function which takes a binary tree $t$ and returns the
list of non-negative integers in $\mathcal{L}_{-1}(t)$, that is, the list
obtained by excluding trailing all $-1$’s in $\mathcal{L}_{-1}(t)$.

The following lemma claims that the $\mathcal{L}$ function computes a list of
degrees of a decreasing polynomial corresponding to a given $\lambda$-term.

######  Lemma 5.

A decreasing polynomial
$(B^{n_{1}}B)\circ(B^{n_{2}}B)\circ\dots\circ(B^{n_{k}}B)$ is
$\beta\eta$-equivalent to the $\lambda$-term $e\in\mathbf{CL}(B)$
corresponding to a binary tree $t$ such that
$\mathcal{L}(t)=[n_{1},n_{2},\dots,n_{k}]$.

######  Proof 2.5.

We prove the statement by induction on the length of the polynomial $P$.

When $P\equiv B^{n}B$ with $n\geq 0$, it is found to be equivalent to the
$\lambda$-term

$\lambda{x_{1}x_{2}x_{3}}\dots
x_{n+1}x_{n+2}x_{n+3}.\,x_{1}~{}x_{2}~{}x_{3}~{}\dots~{}x_{n+1}~{}(x_{n+2}~{}x_{n+3})$

by induction on $n$. This $\lambda$-term corresponds to the binary tree
$t=\langle\langle\dots\langle\langle\star,\underbrace{\star\rangle,\star\rangle,\dots,\star\rangle}_{n~{}{\rm
leaves}},\langle\star,\star\rangle\rangle$. Then we have that
$\mathcal{L}(t)=[n]$ holds from
$\mathcal{L}_{-1}(t)=[n,\underbrace{-1,-1,\dots,-1}_{n+1}]$.

When $P\equiv P^{\prime}\circ(B^{n}B)$ with
$P^{\prime}\equiv(B^{n_{1}}B)\circ\dots\circ(B^{n_{k}}B)$, $k\geq 1$ and
$n_{1}\geq\dots\geq n_{k}\geq n\geq 0$, there exists a $\lambda$-term
$\beta\eta$-equivalent to $P^{\prime}$ corresponding to a binary tree
$t^{\prime}$ such that $\mathcal{L}(t^{\prime})=[n_{1},\dots,n_{k}]$ from the
induction hypothesis. The binary tree $t^{\prime}$ must have the form of
$\langle\langle\langle\dots\langle\langle\star,\underbrace{\star\rangle,\star\rangle,\dots,\star\rangle}_{n_{k}~{}{\rm
leaves}},t_{1}\rangle,\dots,t_{m}\rangle$ with $m\geq 1$ and some trees
$t_{1},\dots,t_{m}$, otherwise $\mathcal{L}(t^{\prime})$ would contain an
integer smaller than $n_{k}$. From the definition of $\mathcal{L}$ and
$\mathcal{L}_{i}$, we have

$\displaystyle\mathcal{L}(t^{\prime})$
$\displaystyle=\mathcal{L}_{s_{m}}(t_{m})\mathbin{{+}\mspace{-8.0mu}{+}}\dots\mathbin{{+}\mspace{-8.0mu}{+}}\mathcal{L}_{s_{1}}(t_{1})$
(3)

where $s_{j}=n_{k}+1+\sum_{i=1}^{j-1}\left|\\!\left|t_{i}\right|\\!\right|$.
Additionally, the structure of $t^{\prime}$ implies $P^{\prime}=\lambda
x_{1}.\dots x_{l}.\,\allowbreak
x_{1}~{}x_{2}~{}\dots~{}x_{n_{k}+1}~{}e_{1}\dots e_{m}$ where $e_{i}$
corresponds to a binary tree $t_{i}$ for $i=1,\dots,m$. From
$B^{n}~{}B=\lambda y_{1}.\dots y_{n+3}.\,\allowbreak y_{1}~{}y_{2}\dots
y_{n+1}~{}(y_{n+2}~{}y_{n+3})$, we compute a $\lambda$-term
$\beta\eta$-equivalent to $P\equiv P^{\prime}\circ(B^{n}B)$ by

$\displaystyle P$ $\displaystyle=\lambda x.~{}P^{\prime}(B^{n}B~{}x)$
$\displaystyle=\lambda x.~{}(\lambda x_{1}\dots x_{l}.~{}x_{1}~{}x_{2}\dots
x_{n_{k}+1}~{}e_{1}~{}\dots~{}e_{m})$ $\displaystyle\qquad\qquad(\lambda
y_{2}\dots y_{n+3}.~{}x~{}y_{2}\dots y_{n+1}~{}(y_{n+2}~{}y_{n+3}))$
$\displaystyle=\lambda{xx_{2}}\dots x_{l}.~{}(\lambda y_{2}\dots
y_{n+3}.~{}x~{}y_{2}\dots y_{n+1}~{}(y_{n+2}~{}y_{n+3}))~{}x_{2}\dots
x_{n_{k}+1}~{}e_{1}\dots e_{m}$ $\displaystyle=\lambda{xx_{2}}\dots x_{l}.\,$
$\displaystyle\qquad(\lambda{y_{n+1}y_{n+2}y_{n+3}}.~{}x~{}x_{2}\dots
x_{n}~{}y_{n+1}~{}(y_{n+2}~{}y_{n+3}))~{}x_{n+1}\dots x_{n_{k}+1}~{}e_{1}\dots
e_{m}$

where $n_{k}\geq n$ is taken into account. We split the proof into four cases:
(i) $n_{k}=n$ and $m=1$, (ii) $n_{k}=n$ and $m>1$, (iii) $n_{k}=n+1$, and (iv)
$n_{k}>n+1$. In the case (i) where $n_{k}=n$ and $m=1$, we have

$\displaystyle P$ $\displaystyle=\lambda{xx_{2}}\dots
x_{l}y_{n+3}.~{}x~{}x_{2}\dots x_{n}~{}x_{n+1}~{}(e_{1}~{}y_{n+3})\text{.}$

whose corresponding binary tree $t$ is
$\langle\langle\dots\langle\langle\star,\underbrace{\star\rangle,\star\rangle,\dots,\star\rangle}_{\mbox{$n$
leaves}},\langle t_{1},\star\rangle\rangle$. From equation (3),
$\mathcal{L}(t)=\mathcal{L}_{n+1}(t_{1})\mathbin{+\\!\\!\\!+}[n+1]=\mathcal{L}(t^{\prime})\mathbin{+\\!\\!\\!+}[n+1]=[n_{1},\dots,n_{k},n+1]$,
thus the statement holds. In the case (ii) where $n_{k}=n$ and $m>1$, we have

$\displaystyle P$ $\displaystyle=\lambda{xx_{2}}\dots x_{l}.~{}x~{}x_{2}\dots
x_{n}~{}x_{n+1}~{}(e_{1}~{}e_{2})~{}e_{3}\dots e_{m}\text{.}$

whose corresponding binary tree $t$ is
$\langle\langle\langle\dots\langle\langle\star,\underbrace{\star\rangle,\star\rangle,\dots,\star\rangle}_{\mbox{$n$
leaves}},\langle t_{1},t_{2}\rangle,t_{3}\rangle,\dots,t_{m}\rangle$. Hence,
$\mathcal{L}(t)=\mathcal{L}(t^{\prime})\mathbin{+\\!\\!\\!+}[n+1]$ holds again
from equation (3). In the case (iii) where $n_{k}=n+1$, we have

$\displaystyle P=\lambda{xx_{2}}\dots x_{l}.~{}x~{}x_{2}\dots
x_{n}~{}x_{n+1}~{}(x_{n+2}~{}e_{1})~{}e_{2}\dots e_{m}\text{, or}$

whose corresponding binary tree $t$ is
$\langle\langle\langle\dots\langle\langle\star,\underbrace{\star\rangle,\star\rangle,\dots,\star\rangle}_{\mbox{$n$
leaves}},\langle\star,t_{1}\rangle,t_{2}\rangle,\dots,t_{m}\rangle$. Hence,
$\mathcal{L}(t)=\mathcal{L}(t^{\prime})\mathbin{+\\!\\!\\!+}[n+1]$ holds from
equation (3). In the case (iv) where $n_{k}\geq n+2$, we have

$\displaystyle P=\lambda{xx_{2}}\dots x_{l}.~{}x~{}x_{2}\dots
x_{n}~{}x_{n+1}~{}(x_{n+2}~{}x_{n+3})~{}\dots~{}e_{1}\dots e_{m}\text{,}$

whose corresponding binary tree $t$ is
$\langle\langle\langle\dots\langle\langle\star,\underbrace{\star\rangle,\star\rangle,\dots,\star\rangle}_{\mbox{$n$
leaves}},\langle\star,\star\rangle,\dots,t_{1}\rangle,\dots,t_{m}\rangle$.
Hence, $\mathcal{L}(t)=\mathcal{L}(t^{\prime})\mathbin{+\\!\\!\\!+}[n+1]$
holds from equation (3).

Consider the $\lambda$-terms $e_{1},e_{2},e_{3}$ given in Figure 2. The
$\lambda$-terms $e_{1}$, $e_{2}$, and $e_{3}$ given in Figure 2 are
$\beta\eta$-equivalent to $B^{1}B$, $(B^{3}B)\circ(B^{1}B)\circ(B^{1}B)$, and
$(B^{5}B)\circ(B^{2}B)\circ(B^{2}B)\circ(B^{2}B)\circ(B^{0}B)$, respectively,
since $\mathcal{L}(t_{1})=[1]$, $\mathcal{L}(t_{2})=[3,1,1]$,
$\mathcal{L}(t_{3})=[5,2,2,2,0]$. (Recall $t_{j}$ ($j=1,2,3$) is the unlabeled
binary tree corresponding to $e_{j}$)

We conclude the uniqueness of decreasing polynomials for $B$-terms shown in
the following theorem.

######  Theorem 6.

Every $B$-term $e$ has a unique decreasing polynomial.

######  Proof 2.6.

For any given $B$-term $e$, we can find a decreasing polynomial for $e$ from
Lemma 2.3 and Lemma 3. Since no other decreasing polynomial can be equivalent
to $e$ from Lemma 5, the present statement holds.

This theorem implies that the decreasing polynomial of $B$-terms can be used
as their _canonical representation_ , which is effectively derived as shown in
Lemma 2.3 and Lemma 3.

As a corollary of the theorem, we can show the “only if” statement of Theorem
2, which corresponds to the completeness of the equation system.

######  Proof 2.7 (Proof of Theorem 2).

Let $e_{1}$ and $e_{2}$ be equivalent $B$-terms, that is, their
$\lambda$-terms are $\beta\eta$-equivalent. From Theorem 6, their decreasing
polynomials are the same. Since the decreasing polynomial is derived from
$e_{1}$ and $e_{2}$ by equations (B1), (B2), and (B3) according to the proofs
of Lemma 2.3 and Lemma 3, equivalence between $e_{1}$ and $e_{2}$ is also
derived from these equations.

##### Comparison with Curry’s compositive normal form

Curry [Cur30b] has introduced a similar normal form for terms built from
regular combinators111 A regular combinator is a combinator in which no lambda
abstraction occurs inside function application. , including $B$-terms. Curry’s
normal form is called  _compositive_ [Pip89] since it is given as a
composition of four special terms, a $K$-term, $W$-term, $C$-term, and
$B$-term. A $B$-term in Curry’s normal form is expressed by

$(B^{n_{1}}B^{m_{1}})\circ(B^{n_{2}}B^{m_{2}})\circ\dots\circ(B^{n_{k}}B^{m_{k}})$

where $k>0$, $n_{1}>n_{2}>\dots>n_{k}\geq 0$ and $m_{i}>0$ for any
$i=1,\dots,k$. Since we have

$B^{n}B^{m}=B^{n}(\underbrace{B\circ\dots\circ
B}_{m})=\underbrace{(B^{n}B)\circ\dots\circ(B^{n}B)}_{m}$

because of equation (B2’), the form is equivalent to

$\underbrace{(B^{n_{1}}B)\circ\dots\circ(B^{n_{1}}B)}_{m_{1}}\circ\underbrace{(B^{n_{2}}B)\circ\dots\circ(B^{n_{2}}B)}_{m_{2}}\circ\dots\circ\underbrace{(B^{n_{k}}B)\circ\dots\circ(B^{n_{k}}B)}_{m_{k}}$

which gives a decreasing polynomial. Curry informally proved the uniqueness of
the normal form by an observation that $B^{n}B^{m}=\lambda x_{0}.\dots
x_{n+m+1}.x_{0}\dots x_{n}~{}(x_{n+1}\dots x_{n+m+1})$, while we have shown
the exact correspondence between a $B$-terms as a lambda term and its normal
form in decreasing polynomial representation.

###  2.4. Relationship with Thompson’s Group

In this subsection, we explore a relationship between polynomials and
_Thompson’s group_ $F$ [MT73]. Thompson’s group $F$ is defined to be the group
generated by formal elements $x_{n}$ ($n=0,1,\dots$) with relations
$x_{m}x_{n}=x_{n}x_{m+1}$ for any $m>n$. Consider the map

$f:\mathbf{CL}(B)\ni(B^{n_{1}}B)\circ\dots\circ(B^{n_{k}}B)\mapsto
x_{n_{1}}^{-1}\dots x_{n_{k}}^{-1}\in F.$

The map $f$ is well-defined since for any $m>n$,

$f((B^{n}B)\circ(B^{m}B))=x_{n}^{-1}x_{m}^{-1}=(x_{m}x_{n})^{-1}=(x_{n}x_{m+1})^{-1}=x_{m+1}^{-1}x_{n}^{-1}=f((B^{m+1}B)\circ(B^{n}B)).$

We can think of $(\mathbf{CL}(B),\circ)$ as a semigroup since $(X\circ Y)\circ
Z=X\circ(Y\circ Z)$ for any $X,Y,Z\in\mathbf{CL}(B)$, and
$f:\mathbf{CL}(B)\rightarrow F$ is a semigroup homomorphism under this
semigroup structure of $\mathbf{CL}(B)$. By definition, $f$ is a semigroup
isomorphism between $\mathbf{CL}(B)$ and the subsemigroup $N$ of $F$ generated
by $x_{n}^{-1}$ ($n=0,1,\dots$).

It is known [Bel04] that every element of $N$ corresponds to an infinite
sequence of binary trees $(t_{0},t_{1},\dots)$ (called a binary forest) where
there exists $k_{0}$ such that $t_{k}=\star$ for any $k\geq k_{0}$. The binary
forest representation of an element of $N$ is defined inductively as follows.

  1. (1)

The binary forest representation of $x_{n}^{-1}$ is
$(\underbrace{\star,\dots,\star}_{n},\langle\star,\star\rangle,\star,\dots)$.

  2. (2)

If $y\in N$ corresponds to the binary forest $(t_{0},t_{1},\dots)$,
$yx_{n}^{-1}$ corresponds to the binary forest

$(t_{0},t_{1},\dots,t_{n-1},\langle t_{n},t_{n+1}\rangle,t_{n+2},\dots).$

We can see the binary forests corresponding to $x_{n}^{-1}x_{m}^{-1}$ and
$x_{m+1}^{-1}x_{n}^{-1}$ are equal to each other for any $n,m$. (In fact,
[Bel04] gave forest representations for the elements in the submonoid of $F$
generated by $x_{n}$ ($n=0,1,\dots$), not $x_{n}^{-1}$). We show the binary
forest representation of $x_{n_{1}}^{-1}\dots x_{n_{k}}^{-1}$ can be obtained
from the binary tree corresponding to the $\lambda$-term of
$(B^{n_{1}}B)\circ\dots\circ(B^{n_{k}}B)$.

######  Theorem 7.

Let
$\langle\dots\langle\langle\star,t_{1}\rangle,t_{2}\rangle\dots,t_{k}\rangle$
be the binary tree corresponding to the $\lambda$-term of the polynomial
$(B^{n_{1}}B)\circ\dots\circ(B^{n_{k}}B)$. Then, the binary forest
representation of
$f((B^{n_{1}}B)\circ\dots\circ(B^{n_{k}}B))=x_{n_{1}}^{-1}\dots
x_{n_{k}}^{-1}$ is given by

$(t_{1},t_{2},\dots,t_{k},\star,\star,\dots).$

######  Proof 2.8.

We prove the theorem by induction on $k$. For binary trees
$t_{1},t_{2},\dots,t_{m}$, we write $\varphi(t_{1},t_{2},\dots,t_{m})$ for the
binary tree
$\langle\dots\langle\langle\star,t_{1}\rangle,t_{2}\rangle,\dots,t_{m}\rangle$.
Since the binary tree corresponding to the $\lambda$-term of $B^{n}B$ is given
by $\varphi(\underbrace{\star,\dots,\star}_{n},\langle\star,\star\rangle)$,
the statement holds for the binary forest representations of
$x_{n}=f(B^{n}B)$. Suppose $n_{1}\geq\dots\geq n_{k}\geq n_{k+1}$. Then, the
binary forest representation of $x_{n_{1}}^{-1}\dots
x_{n_{k}}^{-1}x_{n_{k+1}}^{-1}$ is in the form of
$(\underbrace{\star,\dots,\star}_{n_{k+1}},\langle
t_{1},t_{2}\rangle,t_{3},\dots,t_{m},\star,\dots)$. The binary tree
$t=\varphi(\underbrace{\star,\dots,\star}_{n_{k+1}},\langle
t_{1},t_{2}\rangle,t_{3},\dots,t_{m})$ satisfies
$\mathcal{L}(t)=[n_{1},\dots,n_{k},n_{k+1}]$ if the binary tree
$t^{\prime}=\varphi(\underbrace{\star,\dots,\star}_{n_{k+1}},t_{1},t_{2},t_{3},\dots,t_{m})$
satisfies $\mathcal{L}(t^{\prime})=[n_{1},\dots,n_{k}]$. By Lemma 5, $t$ is
the binary tree corresponding to the $\lambda$-term of
$(B^{n_{1}}B)\circ\dots\circ(B^{n_{k+1}}B)$, and this implies the desired
result.

##  3\. Results on the $\rho$-property of $B$-terms

In this section we show several approaches to if- and only-if-parts of
Conjecture 1 for their special cases. For $B$-terms having the
$\rho$-property, we introduce an efficient implementation to compute the entry
point and the size of the cycle. For $B$-terms not having the $\rho$-property,
we give two methods for proving that they do not have it.

###  3.1. $B$-terms having the $\rho$-property

As shown in Section 1, we can check that $B$-terms equivalent to $B^{n}B$ with
$n\leq 6$ have the $\rho$-property by computing $(B^{n}B)_{\left(i\right)}$
for each $i$. However, it is not easy to check it by computer without an
efficient implementation because we should compute all
$(B^{6}B)_{\left(i\right)}$ with $i\leq
2980054085040~{}(=2641033883877+339020201163)$ to know
$\rho(B^{6}B)=(2641033883877,339020201163)$. A naive implementation which
computes terms of $(B^{6}B)_{\left(i\right)}$ for all $i$ and stores all of
them has no hope to detect the $\rho$-property.

We introduce an efficient procedure to find the $\rho$-property of $B$-terms
which can successfully compute $\rho(B^{6}B)$. The procedure is based on two
orthogonal ideas, Floyd’s cycle-finding algorithm [Knu97] and an efficient
right application algorithm over decreasing polynomials presented in Section
2.3.

The first idea, Floyd’s cycle-finding algorithm (also called the tortoise and
the hare algorithm), enables us to detect the cycle with constant memory
usage, that is, the history of all terms $X_{\left(i\right)}$ does not need to
be stored to check the $\rho$-property of the $X$ combinator. The key to this
algorithm is the fact that there are two distinct integers $i$ and $j$ with
$X_{\left(i\right)}=X_{\left(j\right)}$ if and only if there is an integer $m$
with $X_{\left(m\right)}=X_{\left(2m\right)}$, where the latter requires to
compare $X_{\left(i\right)}$ and $X_{\left(2i\right)}$ from smaller $i$ and
store only these two terms for the next comparison between
$X_{\left(i+1\right)}=X_{\left(i\right)}X$ and
$X_{\left(2i+2\right)}=X_{\left(2i\right)}XX$ when $X_{\left(i\right)}\neq
X_{\left(2i\right)}$. The following procedure computes the entry point and the
size of the cycle if $X$ has the $\rho$-property.

  1. (1)

Find the smallest $m$ such that $X_{\left(m\right)}=X_{\left(2m\right)}$.

  2. (2)

Find the smallest $k$ such that $X_{\left(k\right)}=X_{\left(m+k\right)}$.

  3. (3)

Find the smallest $0<c\leq k$ such that
$X_{\left(m\right)}=X_{\left(m+c\right)}$. If not found, put $c=m$.

After this procedure, we find $\rho(X)=(k,c)$. The third step can be run in
parallel during the second one. See [Knu97, exercise 3.1.6] for the detail.
Although we have tried the other cycle detection algorithm developed by Brent
[Bre80] and Gosper [BGS72, item 132], they show a similar performance.

Efficient cycle-finding algorithms do not suffice to compute $\rho(B^{6}B)$.
Only with the idea above running on a laptop (2.7 GHz Intel Core i7 / 16GB of
memory), it takes about 2 hours even for $\rho(B^{5}B)$ and fails to compute
$\rho(B^{6}B)$ with an out-of-memory error.

The second idea enables us to compute $X_{\left(i+1\right)}$ efficiently from
$X_{\left(i\right)}$ for $B$-terms $X$. The key to this algorithm is to use
the canonical representation of $X_{\left(i\right)}$, that is a decreasing
polynomial, and directly compute the canonical representation of
$X_{\left(i+1\right)}$ from that of $X_{\left(i\right)}$. Additionally, the
canonical representation enables us to quickly decide equivalence which is
required many times to find the cycle. It takes time just proportional to
their lengths. If the $\lambda$-terms are used for finding the cycle, both
application and deciding equivalence require much more complicated
computation. Our implementation based on these two ideas computes
$\rho(B^{5}B)$ and $\rho(B^{6}B)$ in 2 minutes and 6 days, respectively.

For two given decreasing polynomials $P_{1}$ and $P_{2}$, we show how a
decreasing polynomial $P$ equivalent to $(P_{1}~{}P_{2})$ can be obtained. The
method is based on the following lemma about an application of one $B$-term to
another $B$-term.

######  Lemma 8.

For $B$-terms $e_{1}$ and $e_{2}$, there exists $k\geq 0$ such that
$e_{1}\circ(B~{}e_{2})=B~{}(e_{1}~{}e_{2})\circ B^{k}$.

######  Proof 3.1.

Let $P_{1}$ be a decreasing polynomial equivalent to $e_{1}$. We prove the
statement by case analysis on the maximum degree in $P_{1}$. When the maximum
degree is 0, we can take $k^{\prime}\geq 1$ such that
$P_{1}\equiv\underbrace{B\circ\dots\circ B}_{k^{\prime}}=B^{k^{\prime}}$.
Then,

$\displaystyle e_{1}\circ(B\,e_{2})$
$\displaystyle=\underbrace{B\circ\dots\circ
B}_{k^{\prime}}\circ(B~{}e_{2})=(B^{k^{\prime}+1}\,e_{2})\circ\underbrace{B\circ\dots\circ
B}_{k^{\prime}}=B\,(e_{1}\,e_{2})\circ B^{k^{\prime}}$

where equation (B3’) is used $k^{\prime}$ times in the second equation.
Therefore the statement holds by taking $k=k^{\prime}$. When the maximum
degree is greater than 0, we can take a decreasing polynomial $P^{\prime}$ for
a $B$-term and $k^{\prime}\geq 0$ such that
$P_{1}=(B\,P^{\prime})\circ\underbrace{B\circ\dots\circ
B}_{k^{\prime}}=(B\,P^{\prime})\circ B^{k^{\prime}}$ due to equation (B2’).
Then,

$\displaystyle e_{1}\circ(B\,e_{2})$
$\displaystyle=(B\,P^{\prime})\circ\underbrace{B\circ\dots\circ
B}_{k^{\prime}}\circ(B\,e_{2})$
$\displaystyle=(B\,P^{\prime})\circ(B^{k^{\prime}+1}\,e_{2})\circ\underbrace{B\circ\dots\circ
B}_{k^{\prime}}$
$\displaystyle=B~{}(P^{\prime}\circ(B^{k^{\prime}}\,e_{2}))\circ
B^{k^{\prime}}$
$\displaystyle=B~{}(B\,P^{\prime}\,(B^{k^{\prime}}\,e_{2}))\circ
B^{k^{\prime}}$ $\displaystyle=B~{}(P_{1}\,e_{2})\circ B^{k^{\prime}}$
$\displaystyle=B~{}(e_{1}\,e_{2})\circ B^{k^{\prime}}\text{.}$

Therefore, the statement holds by taking $k=k^{\prime}$.

This lemma indicates that, from two decreasing polynomials $P_{1}$ and
$P_{2}$, a decreasing polynomial $P$ equivalent to $(P_{1}\,P_{2})$ can be
obtained in the following steps where $L_{1}$ and $L_{2}$ are lists of non-
negative numbers as shown in Section 2.3 corresponding to $P_{1}$ and $P_{2}$.

######  Algorithm 9 ((Application of $B$-terms $P_{1}$ and $P_{2}$ in
canonical representation)).

  1. (1)

Build $P_{2}^{\prime}$ by raising each degree of $P_{2}$ by 1, i.e., when
$P_{2}\equiv(B^{n_{1}}\,B)\circ\dots\circ(B^{n_{l}}\,B)$,
$P_{2}^{\prime}\equiv(B^{n_{1}+1}\,B)\circ\dots\circ(B^{n_{l}+1}\,B)$. In
terms of the list representation, a list $L_{2}^{\prime}$ is built from
$L_{2}$ by incrementing each element.

  2. (2)

Find a decreasing polynomial $P_{12}$ corresponding to $P_{1}\circ
P_{2}^{\prime}$ by equation (2). In terms of the list representation, a list
$L_{12}$ is constructed by appending $L_{1}$ and $L_{2}^{\prime}$ and
repeatedly applying (2).

  3. (3)

Obtain $P$ by lowering each degree of $P_{12}$ after eliminating the trailing
0-degree units, i.e., when
$P_{12}\equiv(B^{n_{1}}\,B)\circ\dots\circ(B^{n_{l}}\,B)\circ(B^{0}\,B)\circ\dots\circ(B^{0}\,B)$
with $n_{1}\geq\dots\geq n_{l}>0$,
$P\equiv(B^{n_{1}-1}\,B)\circ\dots\circ(B^{n_{l}-1}\,B)$. In terms of the list
representation, a list $L$ is obtained from $L_{12}$ by decrementing each
element after removing trailing 0’s.

In the first step, a decreasing polynomial $P_{2}^{\prime}$ equivalent to
$B\,P_{2}$ is obtained. The second step yields a decreasing polynomial
$P_{12}$ for $P_{1}\circ P_{2}^{\prime}=P_{1}\circ(B\,P_{2})$. Since $P_{1}$
and $P_{2}$ are decreasing, it is easy to find $P_{12}$ by repetitive
application of equation (2) for each unit of $P_{2}^{\prime}$, à la insertion
operation in insertion sort. In the final step, a polynomial $P$ that
satisfies $(B\,P)\circ B^{k}=P_{12}$ with some $k$ is obtained. From Lemma 8
and the degree of decreasing polynomials, $P$ is equivalent to
$(P_{1}\,P_{2})$.

Let $P_{1}$ and $P_{2}$ be decreasing polynomials represented by lists
$L_{1}=[4,1,0]$ and $L_{2}=[2,0]$. Then a decreasing polynomial $P$ equivalent
to $(P_{1}\,P_{2})$ is obtained as a list $L$ in three steps:

  1. (1)

A list $L_{2}^{\prime}=[3,1]$ is obtained from $L_{2}$.

  2. (2)

A decreasing list $L_{12}$ is obtained by

$\displaystyle L_{12}$
$\displaystyle=[4,1,\underline{0,3},1]=[4,\underline{1,4},0,1]=[\underline{4,5},1,0,1]=[6,4,1,\underline{0,1}]=[6,4,\underline{1,2},0]=[6,4,3,1,0]$

where equation (2) is applied in each underlined pair.

  3. (3)

A list $L=[5,3,2,0]$ is obtained from $L_{12}$ as the result of the
application by decrementing each element after removing trailing 0’s.

The implementation based on the right application over decreasing polynomials
is available at https://github.com/ksk/Rho as a program named bpoly. In the
current implementation, every decreasing polynomial is represented by a list
(simulated by an array with offset and live length) whose $k$-th element
stores the number of occurrences of $(B^{k}B)$. For example,
$(B^{3}B)\circ(B^{2}B)\circ(B^{2}B)\circ(B^{0}B)\circ(B^{0}B)$ is represented
by a list `[2,0,2,1]` where the 0-th element is the leftmost `2`. Since
$(B^{k}B)^{m}$ is equivalent to $B^{k}B^{m}$, this representation can be seen
as a variant of Curry’s normal form mentioned in Section 2.3 by inserting the
identity function $B^{k}B^{0}$ for each skipped degree $k$ (e.g.,
$(B^{3}B^{1})\circ(B^{2}B^{2})\circ(B^{1}B^{0})\circ(B^{0}B^{2})$ for the
above). Using the Curry’s normal form, we can adopt a slightly-improved
algorithm by equation $B^{n}B^{m}\circ
B^{n^{\prime}}B^{m^{\prime}}=B^{n^{\prime}+m}B^{m^{\prime}}\circ B^{n}B^{m}$
if $n<n^{\prime}$ at the step (2) in Algorithm 9. Regarding cycle detection of
the implemenation, Floyd’s, Brent’s and Gosper’s algorithms are used. Note
that the program does not terminate for the combinator which does not have the
$\rho$-property. It will not help to decide if a combinator has the
$\rho$-property. One might observe how the terms grow by repetitive right
applications through running the program, though.

###  3.2. $B$-terms not having the $\rho$-property

A computer can check that a $B$-term has the $\rho$-property just by
calculation but cannot show that a $B$-term does not have the $\rho$-property.
In this subsection, we present two methods to prove that specific $B$-terms do
not have the $\rho$-property. One employs decreasing polynomial representation
as previously discussed and the other makes use of tree grammars for binary
tree representation.

####  3.2.1. Using polynomial representation

We show that $B^{2}$ does not have $\rho$-property as an experiment. Note that
$B^{2}$ has the decreasing polynomial representation $(B^{0}B)\circ(B^{0}B)$
which has the smallest length, 2, among the $B$-terms that are expected not to
have the $\rho$-property.

To disprove the $\rho$-property of $B^{2}$, we show the following lemmas about
the regularity of decreasing polynomial representation of
$B^{2}_{\left(i\right)}$ for certain $i$. In these statements, we use

$\displaystyle t_{m}$ $\displaystyle=\frac{m^{2}+m}{2}$ and
$\displaystyle\bigodot_{i=k}^{n}f_{i}$ $\displaystyle=f_{k}\circ f_{k+1}\circ
f_{k+2}\circ\dots\circ f_{n-1}\circ f_{n}\text{.}$

In particular, $\bigodot_{i=k}^{n}f_{i}$ is an identity function if $k>n$.

######  Lemma 10.

For any $k$ and $m$ with $0\leq k\leq m$ and $l>0$,

$\displaystyle\bigodot_{i=k}^{m}(B^{m-i}\,B)^{2}\circ(B^{l}\,B)^{2}$
$\displaystyle=(B^{2m-2k+l+2}\,B)^{2}\circ\bigodot_{i=k}^{m}(B^{m-i}\,B)^{2}$
(4)

holds.

######  Proof 3.2.

This statement can be obtained by applying equation (2) for $4(m-k+1)$ times.

######  Lemma 11.

For any $m\geq 1$ and $0\leq j\leq m$,

$B^{2}_{\left(t_{m}+j\right)}=\bigodot_{i=1}^{j}(B^{2m-i-j+2}\,B)^{2}\circ\bigodot_{i=j+1}^{m}(B^{m-i}\,B)^{2}$
(5)

holds.

######  Proof 3.3.

We prove the statement by induction on $m$. In the case of $m=1$, $t_{m}=1$.
When $j=0$, equation (5) is clear. When $j=1$, equation (5) is shown by

$\displaystyle B^{2}_{\left(2\right)}$
$\displaystyle=((B^{0}~{}B)\circ(B^{0}~{}B))~{}((B^{0}~{}B)\circ(B^{0}~{}B))$
$\displaystyle=(B^{2}~{}B)\circ(B^{2}~{}B)=(B^{2}~{}B)^{2}$

by the application procedure over decreasing polynomial representation.

For the step case, we show that if equation (5) holds for $m=k\geq 1$ and
$0\leq j\leq k$, then it also holds for $m=k+1$ and $0\leq j\leq k+1$. It is
proved by induction on $j$ where $k$ is fixed. When $j=0$, from the outer
induction hypothesis, we obtain

$\displaystyle B^{2}_{\left(t_{k+1}\right)}$
$\displaystyle=B^{2}_{\left(t_{k}+k+1\right)}$
$\displaystyle=B^{2}_{\left(t_{k}+k\right)}\,B^{2}$
$\displaystyle=\left(\bigodot_{i=1}^{k}(B^{2k-i-k+2}\,B)^{2}\right)~{}\left(\left(B^{0}\,B\right)\circ\left(B^{0}\,B\right)\right)$
$\displaystyle=\bigodot_{i=1}^{k}(B^{k-i+1}\,B)^{2}\circ\left(B^{0}\,B\right)\circ\left(B^{0}\,B\right)$
$\displaystyle=\bigodot_{i=1}^{k+1}(B^{(k+1)-i}\,B)^{2}$

by applying the application procedure over decreasing polynomial
representations, hence the statement holds for $j=0$. When $0<j\leq k+1$, from
the inner induction hypothesis and Lemma 10, we similarly obtain

$\displaystyle B^{2}_{\left(t_{k+1}+j\right)}$
$\displaystyle=B^{2}_{\left(t_{k+1}+j-1\right)}\,B^{2}$
$\displaystyle=\left(\bigodot_{i=1}^{j-1}(B^{2k-i-j+5}\,B)^{2}\circ\bigodot_{i=j}^{k+1}(B^{k-i+1}\,B)^{2}\right)\left(\left(B^{0}\,B\right)\circ\left(B^{0}\,B\right)\right)$
$\displaystyle=\bigodot_{i=1}^{j-1}(B^{2k-i-j+4}\,B)^{2}\circ\bigodot_{i=j}^{k}(B^{k-i}\,B)^{2}\circ\left(B^{2}\,B\right)\circ\left(B^{2}\,B\right)$
$\displaystyle=\bigodot_{i=1}^{j-1}(B^{2k-i-j+4}\,B)^{2}\circ\left(B^{2k-2j+4}\,B\right)^{2}\circ\bigodot_{i=j}^{k}(B^{k-i}\,B)^{2}$
$\displaystyle=\bigodot_{i=1}^{j}(B^{2(k+1)-i-j+2}\,B)^{2}\circ\bigodot_{i=j+1}^{k+1}(B^{(k+1)-i}\,B)^{2}\text{.}$

Therefore, the statement holds for $m=k+1$.

These lemmas immediately lead to the anti-$\rho$-property of $B^{2}$.

######  Theorem 12.

The $B$-term $B^{2}$ does not have the $\rho$-property.

######  Proof 3.4.

We prove the statement by contradiction. If $B^{2}$ has the $\rho$-property,
then the set of the normal forms of $S=\\{B^{2}_{\left(i\right)}\mid i>0\\}$
is finite. Hence we can take $m$ as the maximum length of decreasing
polynomial representation among all $B$-terms in $S$. However, decreasing
polynomial representation of $B^{2}_{\left(t_{m+1}\right)}$ has length $m+1$
according to Lemma 11. This contradicts the assumption of $m$.

####  3.2.2. Using tree grammars

Another way for disproving the $\rho$-property of $B$-terms is to consider the
$\beta\eta$-normal form of their $\lambda$-terms. As shown in Section 2, the
$\beta\eta$-normal form of a $B$-term can be regarded as a binary tree. We can
disprove the $\rho$-property of $B$-terms by observing what happens on the
binary trees during the repetitive right application. More specifically, we
first find a set which is closed under the application of a given term, and
then show the length of the spine of trees is unbounded on the repetitive
right application. This leads to the anti-$\rho$-property of the term as shown
in Theorem 14.

First, we introduce some notations. In this section, we write
$\langle\star,\star,\star,\ldots,\star\rangle$ for the binary tree
$\langle\ldots\langle\langle\star,\star\rangle,\star\rangle,\ldots,\star\rangle$
and identify $B$-terms with their corresponding binary trees. For a binary
tree $t=\langle\star,t_{1},\dots,t_{k}\rangle$, we define $l(t)=\text{(the
number of leaves in $t$)}$, $a(t)=k$, and $N_{i}(t)=t_{i}$ for $i=1,\dots,k$.
If $X^{\prime}$ is a $B$-term, $l(X^{\prime})$, $a(X^{\prime})$, and
$N_{i}(X^{\prime})$ are defined to be $l(t)$, $a(t)$, and $N_{i}(t)$ for the
binary tree $t$ corresponding to $X^{\prime}$. Suppose the $\beta\eta$-normal
form of $X^{\prime}$ is $\lambda x_{1}^{\prime}\dots
x^{\prime}_{n^{\prime}}.\,x_{1}^{\prime}~{}e_{1}~{}\dots~{}e_{k}$ and let $X$
be another $B$-term whose $\beta\eta$-normal form is $\lambda x_{1}\dots
x_{n}.\,e$. We can see $X^{\prime}~{}X=(\lambda x^{\prime}_{1}\dots
x^{\prime}_{n^{\prime}}.\,x^{\prime}_{1}~{}e_{1}~{}\cdots~{}e_{k})~{}X=\lambda
x^{\prime}_{2}\dots x^{\prime}_{n^{\prime}}.\,X~{}e_{1}~{}\cdots~{}e_{k}$ and
from Lemma 4, its $\beta\eta$-normal form is

$\begin{cases}\lambda x^{\prime}_{2}\dots x^{\prime}_{n^{\prime}}x_{k+1}\dots
x_{n}.\,e[e_{1}/x_{1},\ldots,e_{k}/x_{k}]&(k\leq n)\\\ \lambda
x^{\prime}_{2}\dots
x^{\prime}_{n^{\prime}}.\,e[e_{1}/x_{1},\dots,e_{n}/x_{n}]~{}e_{n+1}~{}\cdots~{}e_{k}&(\text{otherwise}).\end{cases}$

Here $e[e_{1}/x_{1},\dots,e_{k}/x_{k}]$ is the term which is obtained by
substituting $e_{1},\dots,e_{k}$ to the variables $x_{1},\dots,x_{k}$ in $e$.

By simple computation with this fact, we get the following lemma:

######  Lemma 13.

Let $X$ and $X^{\prime}$ be $B$-terms. Then

$\displaystyle l(X^{\prime}~{}X)$
$\displaystyle=l(X^{\prime})-1+\max\\{l(X)-a(X^{\prime}),\ 0\\}$ (6)
$\displaystyle a(X^{\prime}~{}X)$
$\displaystyle=a(X)+a(N_{1}(X^{\prime}))+\max\\{a(X^{\prime})-l(X),\ 0\\}$ (7)
$\displaystyle N_{1}(X^{\prime}~{}X)$
$\displaystyle=\begin{cases}N_{1}(X)[N_{2}(X^{\prime})/x_{2},\ldots,N_{m}(X^{\prime})/x_{m}]&(\text{if
$N_{1}(X^{\prime})$ is a leaf})\\\
N_{1}(N_{1}(X^{\prime}))&(\text{otherwise})\end{cases}$ (8)

where $m=\min\\{l(X),\ a(X^{\prime})\\}$.

From this lemma, we obtain a key theorem to prove the anti-$\rho$-property.

######  Theorem 14.

Let $X$ be a $B$-term and $T$ be a set of $B$-terms. If $\left\\{X_{(i)}\
\middle|\ i\geq 1\right\\}\subset T$ and $l(X)-a(X^{\prime})\geq 1$ for any
$X^{\prime}\in T$, then $X$ does not have the $\rho$-property.

######  Proof 3.5.

It suffices to show the following: Under the hypotheses of the theorem, for
any $i\geq 1$, there exists $j>i$ that satisfies $l(X_{(j)})>l(X_{(i)})$.
Suppose, for contradiction, that there exists $i\geq 1$ that satisfies
$l(X_{(i)})=l(X_{(j)})$ for any $j>i$. We get $a(X_{(j)})=l(X)-1$ by (6) and
then $a(N_{1}(X_{(j-1)}))=l(X)-a(X)-1$ by (7). Here, $l(X)-a(X)\geq 2$ since
if the $\beta\eta$-normal form of $X$ is $\lambda x^{\prime}_{1}\dots
x^{\prime}_{n^{\prime}}.\,x^{\prime}_{1}~{}e_{1}~{}\dots~{}e_{k}$, each
$e_{i}$ ($i=1,\dots,k-1$) has at least one variable and $e_{k}$ has at least
two variables because otherwise the $\lambda$-term is not $\eta$-normal.
Therefore $a(N_{1}(X_{(j-1)}))\geq 1$, so $N_{1}(X_{(j-1)})$ is not a leaf for
any $j>i$. From (8), we obtain
$N_{1}(X_{(j-1)})=N_{1}(N_{1}(X_{(j-2)}))=\cdots=\underbrace{N_{1}(\cdots
N_{1}(}_{j-i}X_{(i)})\cdots)$ for any $j>i$. However, this implies that
$X_{(i)}$ has infinitely many variables and it yields contradiction.

Using this theorem, we prove that the $B$-term $(B^{k}B)^{(k+2)n}$ does not
have the $\rho$-property. The $\beta\eta$-normal form of $(B^{k}B)^{(k+2)n}$
is given by

$\lambda x_{1}\dots
x_{k+(k+2)n+2}.\,x_{1}~{}x_{2}~{}\cdots~{}x_{k+1}~{}(x_{k+2}~{}x_{k+3~{}}\cdots~{}x_{k+(k+2)n+2}).$

This is deduced from Lemma 5 since the binary tree corresponding to the above
$\lambda$-term is
$t=\langle\underbrace{\star,\dots,\star}_{k+1},\langle\underbrace{\star,\dots,\star}_{(k+2)n+1}\rangle\rangle$
and $\mathcal{L}(t)=[\underbrace{k,\ldots,k}_{(k+2)n}]$. In particular, we get
$l((B^{k}B)^{(k+2)n})=k+(k+2)n+2$.

To apply Theorem 14, we introduce a set $T_{k,n}$ which satisfies the
hypotheses of Theorem 14. First we inductively define a set of terms
$T^{\prime}_{k,n}$ as follows:

  1. (1)

$\star\in T^{\prime}_{k,n}$

  2. (2)

$\langle\star,~{}s_{1},~{}\ldots,~{}s_{(k+2)n}\rangle\in T^{\prime}_{k,n}$ if
$s_{i}=\star$ for a multiple $i$ of $k+2$ and $s_{i}\in T^{\prime}_{k,n}$ for
the others.

Then we define $T_{k,n}$ by $T_{k,n}=\left\\{\langle
t_{0},~{}t_{1},~{}\ldots,~{}t_{k+1}\rangle\ \middle|\ t_{0},\
t_{1},\ldots,t_{k+1}\in T^{\prime}_{k,n}\right\\}$. Since the binary tree of
$(B^{k}B)^{(k+2)n}$ is
$\langle\underbrace{\star,\ldots,\star}_{k+1},\langle\star,\underbrace{\star,\ldots,\star}_{(k+2)n}\rangle\rangle$,
we can see $(B^{k}B)^{(k+2)n}\in T_{k,n}$. Now we shall prove that $T_{k,n}$
is closed under right application of $(B^{k}B)^{(k+2)n}$.

######  Lemma 15.

If $X\in T_{k,n}$ then $X~{}(B^{k}B)^{(k+2)n}\in T_{k,n}$.

######  Proof 3.6.

From the definition of $T_{k,n}$, if $X\in T_{k,n}$ then $X$ can be written in
the form $\langle t_{0},\ t_{1},\ \dots,\ t_{k+1}\rangle$ for some
$t_{0},\ldots,t_{k+1}\in T^{\prime}_{k,n}$. In the case where $t_{0}=\star$,
we have $X~{}(B^{k}B)^{(k+2)n}=\langle
t_{1},~{}\ldots,~{}t_{k+1},~{}\langle\star,~{}\underbrace{\star,~{}\ldots,~{}\star}_{(k+2)n}\rangle\rangle\in
T_{k,n}$. In the case where $t_{0}$ has the form of 2 in the definition of
$T^{\prime}_{k,n}$, then we have
$X=\langle\star,~{}s_{1},~{}\ldots,~{}s_{(k+2)n},~{}t_{1},~{}\ldots,~{}t_{k+1}\rangle$
with $s_{i}=\star$ for a multiple $i$ of $k+2$ and $s_{i}\in T^{\prime}_{k,n}$
for others, hence

$X~{}(B^{k}B)^{(k+2)n}=\langle s_{1},~{}\ldots,~{}s_{k+1},~{}\langle
s_{k+2},~{}\ldots,~{}s_{(k+2)n},~{}t_{1},~{}\ldots,~{}t_{k+1},~{}\star\rangle\rangle.$

We can easily see $s_{1},\ \ldots,\ s_{k+1}$, and $\langle s_{k+2},\ \ldots,\
s_{(k+2)n},\ t_{1},\ \ldots,\ t_{k+1},\ \star\rangle$ are in
$T^{\prime}_{k,n}$.

From the definition of $T_{k,n}$, we can compute that $a(X)$ equals $k+1$ or
$(k+2)n+k+1$ if $X\in T_{k,n}$. Particularly, we get the following:

######  Lemma 16.

For any $X\in T_{k,n}$, $a(X)\leq(k+2)n+k+1=l((B^{k}B)^{(k+2)n})-1$.

By Theorem 14, we get the desired result:

######  Theorem 17.

For any $k\geq 0$ and $n>0$, $(B^{k}B)^{(k+2)n}$ does not have the
$\rho$-property.

We give more examples of $B$-terms which satisfy the condition in Theorem 14
with some set $T$. Consider $X=(B^{2}B)^{2}\circ(BB)^{2}\circ
B^{2}=\langle\star,\ \langle\star,\ \langle\star,\ \langle\star,\ \star,\
\star\rangle,\ \star\rangle,\ \star\rangle\rangle$. We inductively define
$T^{\prime}$ as follows:

  1. (1)

$\star\in T^{\prime}$

  2. (2)

For any $t\in T^{\prime}$, $\langle\star,\ t,\ \star\rangle\in T^{\prime}$

  3. (3)

For any $t_{1},t_{2}\in T^{\prime}$, $\langle\star,\ t_{1},\ \star,\
\langle\star,\ t_{2},\ \star\rangle,\ \star\rangle\in T^{\prime}$

Then $T=\left\\{\langle t_{1},\ \langle\star,\ t_{2},\
\star\rangle\rangle~{}\middle|~{}t_{1},t_{2}\in T^{\prime}\right\\}$ satisfies
the conditions in Theorem 14:

######  Claim 18.

$\\{X_{(k)}\mid k\geq 1\\}\subset T$.

######  Proof 3.7.

By definition, $X\in T$. Let $X^{\prime}=\langle t_{1},\ \langle\star,\
t_{2},\ \star\rangle\rangle\in T$. Then, we have

$X^{\prime}X=\begin{cases}\langle\star,\ t_{2},\ \star,\ \langle\star,\
\langle\star,\ \langle\star,\ \star,\ \star\rangle,\ \star\rangle,\
\star\rangle\rangle&\text{if $t_{1}=\star$}\\\ \langle t_{1}^{\prime},\
\langle\star,\ \langle\star,\ t_{2},\ \star,\ \langle\star,\ \star,\
\star\rangle,\ \star\rangle,\ \star\rangle\rangle&\text{if
$t_{1}=\langle\star,\ t_{1}^{\prime},\ \star\rangle$}\\\ \langle t_{11},\
\langle\star,\ \langle\star,\ t_{12},\ \star,\ \langle\star,\ \langle\star,\
t_{2},\ \star\rangle,\ \star\rangle,\ \star\rangle,\
\star\rangle\rangle&\text{if $t_{1}=\langle\star,\ t_{11},\ \star,\
\langle\star,\ t_{12},\ \star\rangle,\ \star\rangle$},\end{cases}$

and, in either case, $X^{\prime}X\in T$.

######  Claim 19.

$l(X)-a(X^{\prime})\geq 1$ for any $X^{\prime}\in T$.

######  Proof 3.8.

Since $a(X^{\prime})$ is equal to either 1, 3, or 5, and $l(X)=8$,
$l(X)-a(X^{\prime})\geq 3$.

Thus, $(B^{2}B)^{2}\circ(BB)^{2}\circ B^{2}$ does not have the
$\rho$-property. Consider $X=(BB)^{3}\circ B^{3}=\langle\star,\ \langle\star,\
\star,\ \star,\ \star\rangle,\ \star,\ \star\rangle$. We inductively define
$T^{\prime}$ as follows:

  1. (1)

$\star\in T^{\prime}$

  2. (2)

For any $t\in T^{\prime}$, $\langle\star,\ t,\ \star,\ \star\rangle\in
T^{\prime}$

Then $T=\\{\langle t_{1},\langle\star,t_{2},\star,\star\rangle\rangle\mid
t_{1},t_{2}\in T^{\prime}\\}$ satisfies the conditions in Theorem 14:

######  Claim 20.

$\\{X_{(k)}\mid k\geq 1\\}\subset T$.

######  Proof 3.9.

By definition, $X\in T$. Let $X^{\prime}=\langle t_{1},\ \langle\star,\
t_{2},\ \star,\ \star\rangle\rangle\in T$. Then, we have

$X^{\prime}X=\begin{cases}\langle\star,\ t_{2},\ \star,\ \star,\
\langle\star,\ \langle\star,\ \star,\ \star,\ \star\rangle,\ \star,\
\star\rangle\rangle&\text{if $t_{1}=\star$}\\\ \langle t_{1}^{\prime},\
\langle\star,\ \langle\star,\ \langle\star,\ t_{2},\ \star,\ \star\rangle,\
\star,\ \star\rangle,\ \star,\ \star\rangle\rangle&\text{if
$t_{1}=\langle\star,\ t_{1}\,\ \star,\ \star\rangle$}\end{cases}$

and, in either case, $X^{\prime}X\in T$.

######  Claim 21.

$l(X)-a(X^{\prime})\geq 1$ for any $X^{\prime}\in T$.

######  Proof 3.10.

$a(X^{\prime})$ equals 1 or 4 and $l(X)=8$, so $l(X)-a(X^{\prime})\geq 4$.

Thus, $(BB)^{3}\circ B^{3}$ does not have the $\rho$-property.

Theorem 14 gives a possible technique to prove that $l(X_{(i)})$ diverges, or,
the anti-$\rho$-property of $X$, for some $B$-term $X$. Since the hypotheses
of Theorem 14 implies that $l(X_{(i)})$ is also monotonically non-decreasing,
we can consider another problem on $B$-terms: “Give a necessary and sufficient
condition for $l(X_{(i)})$ to be monotonically non-decreasing for a $B$-term
$X$.”

##  4\. Possible approaches

The present paper introduces a canonical representation to make equivalence
check of $B$-terms easier. The idea of the representation is based on that we
can lift all $\circ$’s (2-argument $B$) to the outside of $B$ (1-argument $B$)
by equation (B2’). One may consider it the other way around. Using the
equation, we can lift all $B$’s (1-argument $B$) to the outside of $\circ$
(2-argument $B$). Then one of the arguments of $\circ$ becomes $B$. By
equation (B3’), we can move all $B$’s right. Thereby we find another canonical
representation for $B$-terms given by

$\displaystyle e~{}$
$\displaystyle\mathbin{::=}~{}B~{}\mid~{}B~{}e~{}\mid~{}e\circ B.$

We can show the uniqueness of this representation by giving a bijective
transformation $f$ from it to the polynomial representation. We define $f$
inductively by

$\displaystyle f(B)$ $\displaystyle=B^{0}B$ $\displaystyle f(B~{}e)$
$\displaystyle=(B^{n_{1}+1}B)\circ\dots\circ(B^{n_{k}+1}B)\quad\text{if
$f(e)=(B^{n_{1}}B)\circ\dots\circ(B^{n_{k}}B)$}$ $\displaystyle f(e\circ B)$
$\displaystyle=f(e)\circ(B^{0}B).$

Note that $B^{0}B=B$ and the second rule of $f$ does not change the
equivalence class of $B$-terms because $B(e_{1}\circ\dots\circ
e_{k})=(B~{}e_{1})\circ\dots\circ(B~{}e_{k})$ (Equation (B2’)). We can see the
inverse of this function is given by

$\displaystyle f^{-1}(B^{0}B)$ $\displaystyle=B$ $\displaystyle
f^{-1}((B^{n_{1}}B)\circ\dots\circ(B^{n_{k}}B))$
$\displaystyle=B~{}(f^{-1}((B^{n_{1}-1}B)\circ\dots\circ(B^{n_{k}-1}B)))\quad(n_{k}>0)$
$\displaystyle f^{-1}((B^{n_{1}}B)\circ\dots\circ(B^{n_{k}}B)\circ(B^{0}B))$
$\displaystyle=(f^{-1}((B^{n_{1}}B)\circ\dots\circ(B^{n_{k}}B)))\circ B.$

Function application (written as $@$, explicitly) over this canonical
representation can be recursively defined by

$\begin{array}[]{r@{$\;@\;$}l@{$\;=\;$}l}B&e&B~{}e\\\ (e_{1}\circ
B)&e_{2}&e_{1}~{}@~{}(B~{}e_{2})\\\ (B~{}e)&B&e\circ B\\\
(B~{}e_{1})&(e_{2}\circ B)&((B~{}e_{1})~{}@~{}e_{2})\circ B\\\
(B~{}B)&(B~{}e)&(B~{}(B~{}e))\circ B\\\ (B~{}(e_{1}\circ
B))&(B~{}e_{2})&((B~{}e_{1})~{}@~{}(B~{}(B~{}e_{2})))\circ B\\\
(B~{}(B~{}e_{1}))&(B~{}e_{2})&B~{}((B~{}e_{1})~{}@~{}e_{2})\text{.}\end{array}$

Notice that the pattern matching is exhaustive. The correctness of the
equations is proved by equations (B2’) and (B3’). Termination of the recursive
definition is shown by a simple lexicographical order of the first and the
second operand of application. Note that this canonical form can be
represented by a sequence of $(B~{}\square)$ and $(\square\circ B)$ where
$\square$ stands for a hole. Also, a sequence of them exactly corresponds to a
single term in canonical form by hole application. e.g.,
$[(B~{}\square),~{}(B~{}\square),~{}(\square\circ B)]$ represents
$B~{}(B~{}(B\circ B))$ where a nullary constructor $B$ is filled in the last
element $(\square\circ B)$. This fact may be used to find the $\rho$\- or
anti-$\rho$-properties. By writing 0 and 1 for $(B~{}\square)$ and
$(\square\circ B)$, the above equation can be rewritten as follows:

$\displaystyle\varepsilon@y$ $\displaystyle=0y$ $\displaystyle 1x@y$
$\displaystyle=x@0y$ $\displaystyle 0x@\varepsilon$ $\displaystyle=1x$
$\displaystyle 0x@1y$ $\displaystyle=1(0x@y)$ $\displaystyle 0\varepsilon@0y$
$\displaystyle=100y$ $\displaystyle 01x@0y$ $\displaystyle=1(0x@00y)$
$\displaystyle 00x@0y$ $\displaystyle=0(0x@y)$

where $\varepsilon$ is used for the end marker (filling $B$ at the end). A
monomial $B$-term corresponds to a binary sequence that does not contain $1$.
If $x@y$ is always greater than $x$ in some measure when $y$ contains $1$, we
can claim the “only-if” part of Conjecture 1.

Waldmann [Wal13] suggests that the $\rho$-property of $B^{n}B$ may be checked
even without converting $B$-terms into canonical forms. He simply defines
$B$-terms by

$\displaystyle e$ $\displaystyle\mathbin{::=}B^{k}\mid e~{}e$

and regards $B^{k}$ as a constant which has a rewrite rule
$B^{k}~{}e_{1}~{}e_{2}~{}\dots~{}e_{k+2}\to
e_{1}~{}(e_{2}~{}\dots~{}e_{k+2})$. He implemented a check program in Haskell
to confirm the $\rho$-property. Even in the restriction on rewriting, he found
that $(B^{0}B)_{\left(9\right)}=(B^{0}B)_{\left(13\right)}$,
$(B^{1}B)_{\left(36\right)}=(B^{1}B)_{\left(56\right)}$,
$(B^{2}B)_{\left(274\right)}=(B^{2}B)_{\left(310\right)}$ and
$(B^{3}B)_{\left(4267\right)}=(B^{3}B)_{\left(10063\right)}$, in which it
requires a few more right applications to find the $\rho$-property than the
case of canonical representation. If the $\rho$-property of $B^{n}B$ for any
$n\geq 0$ is shown under the restricted equivalence given by the rewrite rule,
then we can conclude the “if” part of Conjecture 1.

##  5\. Concluding remark

We have investigated the $\rho$-properties of $B$-terms in particular forms so
far.

Table 1. Summary of known results on the $\rho$-property of $B$-terms having $\rho$-property |  $B^{n}B$ with $0\leq n\leq 6$
---|---
having anti-$\rho$-property |  $(B^{k}B)^{(k+2)n}$ with $k\geq 0,n>0$
|  $(B^{2}B)^{2}\circ(BB)^{2}\circ B^{2}$
|  $(BB)^{3}\circ B^{3}$

Table 1 summarizes all results we obtained. While the $B$-terms equivalent to
$B^{n}B$ with $n\leq 6$ have the $\rho$-property, the $B$-terms
$(B^{k}B)^{(k+2)n}$ with $k\geq 0$ and $n>0$, $(B^{2}B)^{2}\circ(BB)^{2}\circ
B^{2}$, and $(BB)^{3}\circ B^{3}$ do not. We have also introduced a canonical
representation of $B$-terms which is useful to prove or disprove of specific
$B$-terms.

We introduce remaining problems related to these results. The $\rho$-property
is defined for any combinatory terms (and closed $\lambda$-terms). We
investigated it mainly for $B$-terms as a simple but interesting instance to
give a partial solution of Conjecture 1 in the present paper. The conjecture
implies that the $\rho$-property of $B$-terms is decidable. One could consider
the decidability of the $\rho$-property for $BCK$ and $BCI$-terms which is
still open. Also, the decidability for the $\rho$-property of $S$-terms and
$L$-terms can be considered. Waldmann’s work on a rational representation of
normalizable $S$-terms [Wal00] may be helpful to solve it. We expect that none
of the $S$-terms have the $\rho$-property as $S$ itself does not, though.
Regarding $L$-terms, Statman’s work [Sta89] may be helpful where equivalence
of $L$-terms is shown decidable up to a congruence relation induced by
$L~{}e_{1}~{}e_{2}\to e_{1}~{}(e_{2}~{}e_{2})$. It would be interesting to
investigate the $\rho$-property of $L$-terms in this setting.

## Acknowledgment

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.

## References

  * [Bar84] Hendrik P. Barendregt.  The Lambda Calculus: Its Syntax and Semantics.  Studies in Logic and the Foundations of Mathematics. Elsevier Science, 1984.
  * [Bel04] James Belk.  Thompson’s group F.  PhD thesis, Cornell University, 2004.
  * [BGS72] Michael Beeler, Ralph W. Gosper, and Richard C. Schroeppel.  HAKMEM.  Technical report, Massachusetts Institute of Technology, Cambridge, MA, USA, 1972.
  * [Bre80] Richard P. Brent.  An improved Monte Carlo factorization algorithm.  BIT, 20(2):176–184, 1980.
  * [Cur30a] Haskell B. Curry.  Grundlagen der Kombinatorischen Logik (Teil I).  American Journal of Mathematics, 52(3):509–536, 1930.
  * [Cur30b] Haskell B. Curry.  Grundlagen der Kombinatorischen Logik (Teil II).  American Journal of Mathematics, 52(4):789–834, 1930.
  * [IN18] Mirai Ikebuchi and Keisuke Nakano.  On repetitive right application of b-terms.  In 3rd International Conference on Formal Structures for Computation and Deduction, FSCD 2018, July 9-12, 2018, Oxford, UK, pages 18:1–18:15, 2018.
  * [Knu97] Donald E. Knuth.  The Art of Computer Programming, Volume 2 (3rd Ed.): Seminumerical Algorithms.  Addison-Wesley Longman Publishing Co., Inc., Boston, MA, USA, 1997.
  * [Lja68] Evgeny S. Ljapin.  Semigroups.  Translations of Mathematical Monographs. American Mathematical Society, 1968.
  * [MT73] Ralph McKenzie and Richard J. Thompson.  An elementary construction of unsolvable word problems in group theory**this work was aided by national science foundation grants gp-7578 and gp-6232x3.  In W.W. Boone, F.B. Cannonito, and R.C. Lyndon, editors, Word Problems, volume 71 of Studies in Logic and the Foundations of Mathematics, pages 457 – 478. Elsevier, 1973.
  * [Nak08] Keisuke Nakano.  $\rho$-property of combinators.  29th TRS Meeting in Tokyo, 2008.
  * [Oka03] Chris Okasaki.  Flattening combinators: surviving without parentheses.  Journal of Functional Programming, 13(4):815–822, July 2003.
  * [Pip89] Adolfo Piperno.  Abstraction problems in combinatory logic a compositive approach.  Theor. Comput. Sci., 66(1):27–43, 1989.
  * [Sch24] Moses Schönfinkel.  Über die Bausteine der mathematischen Logik.  Mathematische Annalen, 92(3–4):305–316, 1924.
  * [Smu12] Raymond M. Smullyan.  To Mock a Mockingbird.  Knopf Doubleday Publishing Group, 2012.
  * [Sta89] Rick Statman.  The Word Problem for Smullyan’s Lark Combinator is Decidable.  Journal of Symbolic Computation, 7(2):103–112, February 1989.
  * [Sta11] Rick Statman.  To Type A Mockingbird.  Draft paper available from http://tlca.di.unito.it/PAPER/TypeMock.pdf, December 2011.
  * [Wal00] Johannes Waldmann.  The Combinator S.  Information and Computation, 159(1-2):2–21, May 2000.
  * [Wal13] Johannes Waldmann.  Personal communication, March 2013.