Konwersja alpha
Z Wikipedii
Konwersja α to 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ętrzynych.
Przykłady prawidłowych kowersji α:
- λ x . λ y . x y -> λ z . λ y . z y
- λ x . λ y . x y -> λ x . λ z . x z
Przykłady nieprawidłowych konwersji α:
- λ x . λ y . x y -> λ x . λ x . x x
- λ x . λ y . x y -> λ y . λ y . y y
Konwersja α jest trywialna, jest jednak ważna, gdyż pozwala unikać kolizji zmiennych.
