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.
These rules were discussed in the paper "A two-level approach to logic
plus functional programming integration" by M. Bellia et al.
|
