Liczby naturalne Churcha
Z Wikipedii
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:
- 0 to λ f . λ x . x
- 1 to λ f . λ x . f x
- 2 to λ f . λ x . f (f x)
- 3 to λ f . λ x . f (f (f x))
Operacje na liczbach naturalnych Churcha są opisane w artykule arytmetyka w rachunku lambda.
Porównaj: liczby naturalne von Neumanna
