On Mar 4, 12:52=A0am, Anton Salikhmetov <salikhme...@[EMAIL PROTECTED]
> wrote:
> Hello,
>
> I'm wondering if the rules described below can be found in existing
> literature. In what follows we use the "=3D" 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 :=3D A]. (*)
>
> Here substitution is determined by the following four rules:
>
> i) x[x :=3D A] =3D A;
> ii) y[x :=3D A] =3D y;
> iii) (\y. M)[x :=3D A] =3D \y. M[x :=3D A];
> iv) (M N)[x :=3D A] =3D (M[x :=3D A] N[x :=3D A]).
>
> One can observe that
>
> (\x. x A) =3D A, (1)
>
> and
>
> (\x. y A) =3D y. (2)
>
> Further, due to (*)
>
> (\x. \y. M A) -> (\y. M)[x :=3D A] =3D \y. M[x :=3D A] <- \y. (\x. M A),
>
> hence
>
> (\x. \y. M A) =3D \y. (\x. M A). (3)
>
> Finally, using (*) one can write
>
> (\x. (M N) A) -> (M N)[x :=3D A] =3D (M[x :=3D A] N[x :=3D A]) <- ((\x.
M =
A)
> (\x. N A)),
>
> hence
>
> (\x. (M N) A) =3D ((\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.
It appears that this set of rules is not good when the classic
"leftmost outermost" reduction strategy is used.
Let us apply the rules (1)-(4) to the following lambda expression:
\a. \b. \a a b -(rule 3)->
\b. (\a. a a) b -(rule 4)->
(\b. \a. a b) (\b. a b) -(rule 3)->
\a. (\b. a b) (\b. a b) -(rule 4)->
\a. \b. a (\b. a b) (\a. b (\b. a b)) -(rule 3)->
=2E..
It is easy to see that the expression grows indefinitely at further
application of the rules, and the normal form is never reached. This
is because the third rule creates "parasitic" redexes.
Perhaps, there exists another reduction strategy that gives the normal
form for any reducible expression and is "compatible" with these
rules. I would be very grateful for any ideas on how such a strategy
could be discovered.
|
