Liczby naturalne Churcha

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ę i argument która -krotnie aplikuje do

Tak więc w zapisie matematycznym:

  • 0 to
  • 1 to
  • 2 to
  • 3 to
  • N+1 to

a w zapisie lambda: liczba naturalna to

gdzie:

to
to

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

Zobacz teżEdytuj