A combinator, higher-order function given by a closed λ-term, is said to have the ρ-property if the combinator X satisfies X_m and X_n are βη-equivalent for distinct m and n, where X_n is defined by X₁ = X and X_n = X_n-1 X for n > 1.

Three programs rho, bpoly and bmono are available here.

Each program can be built by make with the name of the target program, e.g., make rho. You may build all programs just by make as far as requirements are satisfied.

• For rho, OCaml (≥ 4.08) and CamlP5 are required
• For bpoly, OCaml (≥ 4.08), CamlP5 and Zarith are required.
• For bmono, a standard C compiler is required.

The program rho checks the ρ-property of arbitrary combinators. For example, the ρ-property of B, B₁₀ = B₆, is checked by

$ rho B

where $ denotes the command prompt. To check B(B B), run

$ rho 'B(B B)'

simply. Available combinators can be seen by

$ rho -l

where \x[...] represents λ-abstraction. This syntax of λ-abstraction can be used for combinators given by users. Use the -q option for the quiet mode. Although the program only checks first 65535 terms by default, add the -u option for keeping on trying to find the cycle. Using the -f option, Floyd's (also called tortoise-and-hare) semi-algorithm is used for finding cycles with constant memory usage. Run

$ rho -h

for details of command line options.

The program bpoly checks the ρ-property of a B-term. The implementation is based on the normal form of B-terms in the 'decreasing polynomial' representation [1] of the form (B^m₁ B) o (B^m₂ B) o ... o (B^m_k B), with m₁ ≥ m₂ ≥...≥ m_k ≥ 0 where Bⁿ stands fold n-fold composition of B, e.g., (B³ B) stands B(B(B B)). To check the ρ-property of B² B, run

$ bpoly 2

which results in (B² B)₂₉₄ = (B² B)₂₅₈ with the history of computation over decreasing polynomials. To check the ρ-property of (B² B) o (B² B) o (B¹ B) o (B¹ B) o (B⁰ B) o (B⁰ B), run

$ bpoly 2 2 1 1 0 0

which does not terminate up to the given limit of repetition (65535 by default) because it does not have the ρ-property as shown our paper [1]. Command line options similar to those of rho are available. It is better to add the -f or -b option for larger n so as to use Floyd's or Brent's cycle-finding algorithm. Run

$ bpoly -h

for details of command line options.

The program bmono checks the ρ-property of a monomial B-term of the form B^m B where m is given as an argument. To check the ρ-property of B² B, run

$ bmono 2

in a similar way to bpoly. The program bmono is written in C and specialized for checking monomial B-terms, so it may run faster than bpoly. The program bpoly should be used for observing the divergence of repetitive right application of non-monomial B-terms because only monomial B-terms have the ρ-property as conjectured below.

Keisuke Nakano conjectured in 2008 [2] that

a B-term has the ρ-property if and only if it is equivalent to Bⁿ B with some n.

in which if-part and only-if-part are both still open.

For every n ≤ 6, it is known that Bⁿ B has the ρ-property.

• (B⁰ B)₁₀ = (B⁰ B)₆
• (B¹ B)₅₂ = (B¹ B)₃₂
• (B² B)₂₉₄ = (B² B)₂₅₈
• (B³ B)₁₀₀₃₆ = (B³ B)₄₂₄₀
• (B⁴ B)₆₂₂₆₅₉ = (B⁴ B)₁₉₁₂₀₆
• (B⁵ B)_1000685878 = (B⁵ B)_766241307
• (B⁶ B)_{2980054085040} = (B⁶ B)_{2641033883877}

All of the above can be confirmed by running the bpoly program. It took 8 days to check the ρ-property of the case n=6.

It is shown that the following B-terms do not have the ρ-property.

• (B^k B)^(k+2)n with k≥0 and n>0
• (B² B)² o (B¹ B)² o (B⁰ B)²
• (B¹ B)³ o (B⁰ B)³

The proofs are found in [1] and [3].

[1] Mirai Ikebuchi and Keisuke Nakano. On Repetitive Right Application of B-terms, In the proceedings of the 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018), pp.18:1-18:15, Oxford, UK, July 2018.

[2] Keisuke Nakano. ρ-Property of Combinators, 29th TRS Meeting, Tokyo, 2008.

[3] Mirai Ikebuchi and Keisuke Nakano. On Properties of B-terms, Logical Methods in Computer Science (LMCS), Volume 16, Issue 2, June 2020.