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: Encyklopedia PWN • 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ę ${\displaystyle \beta }$-redukcji nazywamy najmniejszą relację ${\displaystyle \to _{\beta }\subset \Lambda \times \Lambda }$ taką, że:

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

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

• konwersja α