Konwersja α

Konwersja α – operacja w rachunku lambda polegająca na zamianie zmiennej określanej przez lambdę oraz wszystkich jej wystąpień w wyrażeniu pod lambdą, na inną, nie kolidującą z żadną z lambd zewnętrznych lub wewnętrznych.

Przykłady prawidłowych konwersji α:

• $\lambda x.\lambda y.xy\rightarrow \lambda z.\lambda y.zy$
• $\lambda x.\lambda y.xy\rightarrow \lambda x.\lambda z.xz$

Przykłady nieprawidłowych konwersji α:

• $\lambda x.\lambda y.xy\rightarrow \lambda x.\lambda x.xx$
• $\lambda x.\lambda y.xy\rightarrow \lambda y.\lambda y.yy$

Konwersja α jest trywialna, jest jednak ważna, gdyż pozwala unikać kolizji zmiennych.

Zobacz też

• redukcja β