One-step reduction strategy for micro-lambda and extensionality in TRS
Anton Salikhmetov
Some time ago I exchanged a few emails with Prof. Barendregt on
certain aspects of lambda calculus and the extensionality property.
Prof. Barendregt suggested that I could write to J. Klop for
clarification
of some questions on explicit substitution and term rewriting systems.
Unfortunately, professor Klop did not respond.
My question is about the unsolved problem stated on page 81 of
J. Klop's Ustica lectures: is there a recursive normalizing one-step
reduction strategy for micro lambda calculus?
The Ustica notes can be downloaded using the following link:
http://web.mac.com/janwillemklop/Site/Courses_and_Notes_files/ustica-lectures.pdf
I came up with a (most probably very naive) strategy which is rather
similar to the algorithm defined by Gyorgy Revesz. The strategy can be
described as follows. If the function body in the leftmost outermost
redex is of the form "\a. \b. ... \z. M" where M is a redex, then
contract M. Otherwise, contract the leftmost outermost redex.
I tested this strategy using a set of different lambda terms,
including quite complex ones which were successfully evaluated. Some
even more complex expressions failed to be evaluated, but I guess that
the reason was the limits imposed by my hardware and the operating
system.
This makes me feel that the strategy might provide a positive answer
to the open question: indeed, a good set of "test cases" showed that
the approach was working.
Just in case, an archive containing Python implementation of the
strategy described above can be downloaded using the following link:
http://pygx.sourceforge.net/micro.tar
Would you mind helping me to determine whether my approach is in fact
a normalizing one-step strategy and whether the construction is
correct?
With best regards,
Anton Salikhmetov