Konwersja α

Z testwiki
Przejdź do nawigacji Przejdź do wyszukiwania

Szablon:Dopracować 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 α:

  • λx.λy.xyλz.λy.zy
  • λx.λy.xyλx.λz.xz

Przykłady nieprawidłowych konwersji α:

  • λx.λy.xyλx.λx.xx
  • λx.λy.xyλy.λy.yy

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

Zobacz też