Liczby naturalne Churcha

Z Wikipedii, wolnej encyklopedii
Skocz do: nawigacji, wyszukiwania

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"