Hello,

After long searching and studying literature about Explicit
Substitutions and Term Rewriting Systems, the first paper discussing
the Eta reduction in the context of Explicit Substitutions I found
became "Eta-Conversion for the Languages of Explicit Substitutions" by
Therese Hardin (http://www.springerlink.com/content/
p778664h6lwk4653/). Unfortunately, this paper does not offer a system
that has a well-defined algorithm for evaluation. Hence my further
search was focused at Term Rewriting Systems with Eta reduction
implementation.

Later, the paper "An explicit Eta rewrite rule" by Daniel Briaud
(http://hal.inria.fr/docs/00/07/42/58/PDF/RR-2417.pdf) was found. This
paper appends an "Eta" rewrite rules to the \lambda\upsilon version of
Explicit Substitutions theory. The resulting \lambda\upsilon\eta
theory is indeed a TRS with a finite number of rewriting rules.
However, this theory does not satisfy for implementing it in the form
of an abstract machine, since a normal form for its terms representing
computable functions does not match that of Pure Lambda Calculus, and
the latter one even cannot be achieved from the \lambda\upsilon\eta
normal form. For example, the following expression, which has already
been a normal form, is reduced with the \lambda\upsilon\eta theory's
rewrite rules to another expression, which does not contain enough
information for recovering the initial term:

\x. ((x x) x) = \((1 1) 1) -Eta- (1 1)[\bot/] -
1[\bot/] 1[\bot/] - \bot \bot = \bot \bot.

In turn, the strong reduction in the combinatory logic appeared to
require an infinite number of axioms - that had been proved in the
paper "Axioms for Strong Reduction in Combinatory Logic" by Roger
Hindley (http://links.jstor.org/sici?
sici=0022-4812(196706)32%3A2%3C224%3AAFSRIC%3E2.0.CO%3B2-
D&origin=crossref). Therefore, the combinatory logic is also useless
for creating an abstract machine for strong reduction. Indeed, it is
easier to use Pure Lambda Calculus for that reason. On the other hand,
naive implementation of Pure Lambda Calculus' Eta reduction is
extremely inefficient.

I also attempted to use the style of Micro-Lambda Calculus, which had
been considered in J. Klop's Ustica notes (http://web.mac.com/
janwillemklop/Site/Courses_and_Notes_files/ustica-lectures.pdf), for
the Eta reduction:

\x. (x x) - not a redex,
\x. (y x) - y,
\x. (\y. M x) - an expression containing a Beta redex,
\x. ((M N) x)...

Unfortunately, for the application case, it is not clear for me how to
perform Eta reduction without analyzing both M and N subexpressions.
As far as know, the question whether an equivalent of Eta for Micro-
Lambda Calculus exists remains unresolved.

I would be grateful for any help in studying possible ways to
implement Eta reduction in abstract reduction machines.

With best regards,
Anton Salikhmetov