Manuál k pochopení eta-redukce by Standa Novák (stanov@mail.muni.cz)
Vyjádřete následující funkci bez lambda abstrakce:
\x -> 0 < 35 - 3 * 2 ^ x
Nejprve si celý výraz převedeme do prefixu s respektováním priority jednotlivých operátorů.
Stejnou barvou je vyznačena funkce a její argumenty.
\x -> (<) 0 ((-) 35 ((*) 3 ((^) 2 x)))
Prefixový zápis binárních funkcí můžeme zapsat jako částečnou aplikaci binární funkce na jeden
argument.
\x -> (0<) ((35-) ((3*) ((2^) x)))
Nyní již můžeme začít s převodem výrazu do pointfree. Využijeme k tomu definici tečky
(f . g) x = f (g x) v opačném směru na argument funkce (35-), tj. červená závorka:
(3*) ((2^) x)
--f- (--g- x)
\x -> (0<) ((35-) (((3*).(2^)) x))
Pokračujeme stejně, jako v předchozím kroku:
(35-) (((3*).(2^)) x)
--f-- (-----g----- x)
\x -> (0<) (((35-).((3*).(2^))) x)
Stejný postup.
(0<) (((35-).((3*).(2^))) x)
--f- (---------g--------- x)
\x -> ((0<).((35-).((3*).(2^)))) x
V tomto bodě je již x úplně napravo, tím pádem můžeme odstranit lambdu.
(0<).((35-).((3*).(2^)))
Jelikož funkce (.) sdružuje zprava, můžeme odstranit závorky určující pořadí vyhodnocení.
(0<).(35-).(3*).(2^)