Liczby naturalne Churcha

Szablon:Dopracować Liczby naturalne Churcha – konstrukcja w rachunku lambda, umożliwiająca wykonywanie normalnej arytmetyki.

Rachunek lambda bez typów nie zawiera sam z siebie liczb, więc należy je skonstruować.

Liczba naturalna Churcha to funkcja wyższego rzędu pobierająca dwa argumenty – funkcję $f$ i argument $x,$ która $n$-krotnie aplikuje $f$ do $x.$

Tak więc w zapisie matematycznym:

• 0 to $x,$
• 1 to $f(x),$
• 2 to $f(f(x)),$
• 3 to $f(f(f(x))),$
• N+1 to $f(N),$

a w zapisie lambda: liczba naturalna $n$ to $\lambda f.\lambda x.f^{n}x,$

gdzie:

$f^{0}x$ to $x,$

$f^{n+1}x$ to $f(f^{n}x).$

Operacje na liczbach naturalnych Churcha są opisane w artykule arytmetyka w rachunku lambda.

Zobacz też

• Inne sposoby konstrukcji liczb