Liczby naturalne Churcha

Liczby naturalne Churcha to 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.

Porównaj: liczby naturalne von Neumanna, liczby naturalne w artykule "aksjomaty i konstrukcje liczb"