An impure solution to the problem of matching fans

Some time ago, I found an impure solution to the problem of matching fans in Lamping's abstract algorithm. It is described in [1] and implemented in [2], the essential part of source code being available in [3].

My understanding is that the algorithm effectively eliminates the need in bookkeeping nodes (so-called "oracle") for optimal reduction in case of arbitrary untyped λ-terms. Although I have no formal proof for its correctness yet, the amount of testing [4, 5] that have already been done leaves little room for counterexamples.

Questions remaining open are: how to (dis)prove correctness of the algorithm as well as how to simplify and improve the algorithm? Any help would be highly appreciated.

[5] (the "Benchmarks" section)

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Amount of testing

(Disclaimer: I am not familiar with optimal reduction and the 'matching fans" problem.)

If I understand correctly, the "amount of testing" you reference is that you wrote a couple (non-trivial) programs and tested that your reducer returns the expected output.

I don't consider that this is enough testing to give confidence of a non-trivial property, as the programs that humans write are typically of a very specific shape. (For example, I am no expert, but your tests may all fall in the fragment where it is known that an oracle is not needed?)

Here is what I would find more convincing:
- a formal proof that the algorithms acts as desired
- or, at least, an exhaustive check that all lambda-terms smaller than a certain bound (say 15) behave as desired

Then there is also the matter of what you are claiming and testing. Are you only testing that the reduction returns the right result, or are you testing that the reduction sequence is "optimal" as claimed? It sounds plausible that an invalid simplification of the algorithm would still compute correct normal-forms, only not in an optimal way -- if I understand correctly, your current tests would not catch this error?

(Have you implemented the standard algorithm to compare the reduction sequences of both? Are you claiming that they are identical, or merely of the same length?)

Still looking for counterexamples

Some other test cases are available in the software package itself [5], including comparison with Lambdascope, matching the number of beta-reductions wherever Lambdascope is able to reach normal form within reasonable amount of interactions (up to ten million interactions).

A formal proof of the algorithm's (in)correctness is one of the things I am asking for help with. Due to different nature of the solution, I am unable to directly apply techniques from [6]. So far, I have not been able to construct a counterexample which would differ in its normal form or number of beta-reductions from the optimal one. Any help in finding one would be highly appreciated.

[5] (the "Benchmarks" section)
[6] Andrea Asperti, Stefano Guerrini. The Optimal Implementation of Functional Programming Languages. Cambridge Tracts in Theoretical Computer Science, v.45, Cambridge University Press, 1998, isbn = 9780521621120

Exhaustive search

Have you tried exhaustively searching for counter-examples of size below 15?


No, I have not. If you know how to arrange such a search, please feel free to use CLI:

$ npm i -g @alexo/lambda
└── @alexo/lambda@0.3.6
$ lambda -p 'S K I' # experimental algorithm
11(7), 2 ms
v1: v1
$ lambda -p -a optimal 'S K I' # Lambdascope
59(7), 4 ms
v1: v1