A combinator, higher-order function given by a closed λ-term, is said to have the ρ-property if the combinator X satisfies Xm and Xn are βη-equivalent for distinct m and n, where Xn is defined by X1 = X and Xn = Xn-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, B10 = B6, 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
(Bm1 B) o
(Bm2 B) o ... o
(Bmk B),
with m1 ≥ m2 ≥...≥ mk ≥ 0
where Bn stands fold n-fold composition of B,
e.g., (B3 B) stands B(B(B B)).
To check the ρ-property of B2 B,
run
$ bpoly 2
which results in (B2 B)294 = (B2 B)258 with the history of computation over decreasing polynomials. To check the ρ-property of (B2 B) o (B2 B) o (B1 B) o (B1 B) o (B0 B) o (B0 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 Bm B where m is given as an argument.
To check the ρ-property of B2 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 Bn B with some n.
in which if-part and only-if-part are both still open.
For every n ≤ 6, it is known that Bn B has the ρ-property.
- (B0 B)10 = (B0 B)6
- (B1 B)52 = (B1 B)32
- (B2 B)294 = (B2 B)258
- (B3 B)10036 = (B3 B)4240
- (B4 B)622659 = (B4 B)191206
- (B5 B)1000685878 = (B5 B)766241307
- (B6 B)2980054085040 = (B6 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.
- (Bk B)(k+2)n with k≥0 and n>0
- (B2 B)2 o (B1 B)2 o (B0 B)2
- (B1 B)3 o (B0 B)3
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.