Dlaczego liczby naturalne zamiast liczb całkowitych?

Interesuje mnie, dlaczego autorzy książek na temat teorii języków programowania i teorii typów tak uwielbiają liczby naturalne (np. J. Mitchell, Podstawy języków programowania i B. Pierce, Typy i języki programowania). Opis prostego rachunku różniczkowego lambda, a zwłaszcza języka programowania PCF, jest zwykle oparty na języku Nat i Bool. Dla osób używających i uczących PL przemysłowych ogólnego przeznaczenia o wiele bardziej naturalne jest traktowanie liczb całkowitych zamiast naturalnych. Czy możesz podać kilka dobrych powodów, dla których teoretyk PL preferuje nat? Poza tym jest to trochę mniej skomplikowane. Czy są jakieś fundamentalne powody, czy to tylko zaszczyt tradycji?

UPD Dla tych wszystkich komentarzy na temat „fundamentalności” naturałów: Jestem całkiem świadomy tych wszystkich fajnych rzeczy, ale wolałbym zobaczyć przykład, kiedy naprawdę istotne jest posiadanie tych właściwości w teorii typów teorii PL. Np. Szeroko wspomniana indukcja. Kiedy mamy jakąkolwiek logikę (którą po prostu wpisujemy LC), jak podstawową logikę pierwszego rzędu, naprawdę używamy indukcji - ale indukcji na drzewie pochodnym (które mamy również w lambda).

Moje pytanie w zasadzie pochodzi od ludzi z branży, którzy chcą zdobyć podstawową teorię języków programowania. Kiedyś mieli w swoich programach liczby całkowite i bez konkretnych argumentów i zastosowań do badanej teorii (teoria typów w naszym przypadku), dlaczego uczyć się języków tylko z nat, czują się dość rozczarowani.

Krótka odpowiedź: naturals są pierwszymi limitami porządkowymi. Stąd odgrywają one centralną rolę w teorii zbiorów aksjomatycznych (np. Aksjomat nieskończoności jest twierdzeniem, że istnieją) i logiką, a teoretycy PL dzielą fundamentalne zainteresowania z logikami. Chcemy mieć dostęp do zasady indukcji, aby udowodnić całkowitą poprawność, zakończenie i podobne właściwości, a naturale są (er) naturalnym wyborem dobrego porządku.

Nie chcę jednak sugerować, że binarne liczby całkowite o skończonej szerokości są mniej fajnymi obiektami. Są reprezentacjami p-adiki i pozwalają nam na zastosowanie metod szeregów potęgowych w teorii liczb i kombinatorykach. Oznacza to, że ich znaczenie staje się bardziej widoczne w algorytmii niż PL, ponieważ wtedy zaczynamy bardziej dbać o złożoność niż zakończenie.

Naturale są znacznie bardziej fundamentalną koncepcją niż liczby całkowite.

Indukcja zachodzi nad naturałami, a liczby całkowite można wyprowadzić z naturałów po prostym dodaniu jednoargumentowego odwrotnego operatora.

W rzeczywistości chciałbym zadać odwrotne pytanie: dlaczego projektanci języka programowania wczesnego (i maszyny rejestrującej) zapisali liczby całkowite jako podstawowy typ danych, skoro są one tak drugorzędne i tak łatwo pochodzą od naturali?

Podejrzewam, że dzieje się tak tylko dlatego, że było kilka fajnych kodowań binarnych, które mogłyby elegancko obsługiwać liczby całkowite. ;-)

Zastanów się, jak często chcesz ignorować ujemny zakres programistycznej liczby całkowitej i zastanów się nad impulsem, aby mieć liczbę całkowitą bez znaku, aby odzyskać utracony bit.

Pomiędzy i istnieje obliczalna bijectycja . Dlatego wystarczy uzasadnić obliczalność i tym podobne, używając tylko liczb naturalnych, cały czas wiedząc, że wyniki uogólniają się na liczby całkowite (i liczby wymierne oraz wszystkie inne rekurencyjnie wyliczalne zbiory).$\mathbb{N}$$\mathbb{Z}$

Rozumowanie tylko w przypadku naturali jest wygodne, ponieważ masz indukcję, a jest dobrze uzasadnionym zestawem z naturalnym porządkiem . Ta ostatnia jest szczególnie ważna, ponieważ może być instrumentalizowana w dowodach zakończenia. Chociaż możesz zdefiniować dobrze ugruntowane zamówienie na , jest to mniej wygodne, ponieważ nie pasuje do zwykłego porządku.$\mathbb{N}$$\leq$$\mathbb{Z}$

Jeszcze innym powodem (związanym z już podanymi, ale ta odpowiedź dodaje nowe informacje) jest to, że istnieje bardzo prosta, pozbawiona ilorazów konstrukcja naturali, która towarzyszy ładnej zasadzie indukcji [jak już powiedziano] . To, co nie zostało rozwinięte, to to, jak trudno jest wymyślić liczby całkowite bez ilorazu.

Im więcej programów robię tam, gdzie chcę mieć wysoką pewność, tym bardziej potrzebuję naturałów i stwierdzenie, że posiadanie tylko liczb całkowitych jest dla mnie prawdziwym bólem.

Czy są jakieś dobre powody, dla których teoretycy PL wolą liczby naturalne niż liczby całkowite? Jest kilka, ale w podręczniku na temat semantyki języka programowania myślę, że nie ma technicznego powodu, dla którego trzeba. Nie mogę wymyślić żadnego innego miejsca niż systemy typu zależnego, w których indukcja danych jest ważna w teorii PL. Inne podręczniki Mike'a Gordona , Davida Schmidta , Boba Tennenta i Johna Reynoldsa tego nie robią. (I te książki byłyby prawdopodobnie bardziej odpowiednie do nauczania ludzi, którym zależy na przemysłowych PL PL ogólnego przeznaczenia!)

Masz więc dowód, że nie jest to konieczne. W rzeczywistości twierdziłbym, że dobry podręcznik teorii teorii PL powinien być parametryczny w prymitywnych typach języka programowania i mylące jest sugerowanie czegoś innego.

Naturale, boole i operacje na nich można w prosty sposób zakodować w czystym rachunku lambda jako tak zwane cyfry kościelne (i chyba boole kościelne). Nie jest jasne, jak ładnie zakodować liczby całkowite, chociaż oczywiście można to zrobić.