Redukcja beta

Ten artykuł od 2012-10 wymaga zweryfikowania podanych informacji.

Należy podać wiarygodne źródła w formie przypisów bibliograficznych.
Część lub nawet wszystkie informacje w artykule mogą być nieprawdziwe. Jako pozbawione źródeł mogą zostać zakwestionowane i usunięte.
Sprawdź w źródłach: Google Books • Google Scholar • BazHum • BazTech • RCIN • Internet Archive (texts / inlibrary)
Po wyeliminowaniu niedoskonałości należy usunąć szablon {{Dopracować}} z tego artykułu.

Redukcja β to najważniejsze przekształcenie w rachunku lambda, odpowiadające aplikacji funkcji.

Relację $β$ -redukcji nazywamy najmniejszą relację $\to_{β} \subset Λ \times Λ$ taką, że:

$(λ x . M) N \to_{β} M [x := N],$
Jeśli $M \to_{β} M^{'}$ to, $M N \to_{β} M^{'} N,$ $N M \to_{β} N M^{'}$ oraz $λ x . M \to_{β} λ x . M^{'}$

Najmniejszą zwrotną i przechodnią relację zawierającą $\to_{β}$ oznacza się $↠_{β},$ zaś najmniejszą zwrotną, przechodnią i symetryczną – $=_{β} .$

Zobacz też

konwersja α