Hello,
I'm wondering if the rules described below can be found in existing
literature. In what follows we use the "=" sign to indicate that both
sides of the equation can be beta-reduced to one and the same term.
Classic definition of the beta reduction is well-known:
(\x. M A) -> M[x := A]. (*)
Here substitution is determined by the following four rules:
i) x[x := A] = A;
ii) y[x := A] = y;
iii) (\y. M)[x := A] = \y. M[x := A];
iv) (M N)[x := A] = (M[x := A] N[x := A]).
One can observe that
(\x. x A) = A, (1)
and
(\x. y A) = y. (2)
Further, due to (*)
(\x. \y. M A) -> (\y. M)[x := A] = \y. M[x := A] <- \y. (\x. M A),
hence
(\x. \y. M A) = \y. (\x. M A). (3)
Finally, using (*) one can write
(\x. (M N) A) -> (M N)[x := A] = (M[x := A] N[x := A]) <- ((\x. M A)
(\x. N A)),
hence
(\x. (M N) A) = ((\x. M A) (\x. N A)). (4)
Usage of the rules (1)-(4) could simplify construction of a machine
for automated evaluation of lambda expressions: if each of the above
rules is applied within one clock cycle, then after every cycle the
memory will contain a valid expression.
I will be very grateful for any information about where this or a
similar approach to reduction of lambda expressions was considered in
the literature.
|
