Redukcja beta

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

Relację $\beta$-redukcji nazywamy najmniejszą relację $\to _{\beta }\subset \Lambda \times \Lambda$ taką, że:

• $(\lambda x.M)N\to _{\beta }M[x:=N],$
• Jeśli $M\to _{\beta }M'$ to, $MN\to _{\beta }M'N,$ $NM\to _{\beta }NM'$ oraz $\lambda x.M\to _{\beta }\lambda x.M'$

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

Zobacz też

• konwersja alpha