Dlaczego liczby naturalne zamiast liczb całkowitych?

28

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.

Artem Pelenitsyn
źródło
Myślę, że nie jest to pytanie na poziomie badawczym, choć interesujące.
Raphael,
4
To nie jest, ale jest to rodzaj dużego pytania, które akceptujemy.
Suresh Venkat,
1
Zastanawiam się, czy w jakiś sposób zestaw liczb całkowitych nieujemnych może być nawet bardziej fundamentalny niż liczby naturalne ze względu na unikalne właściwości wartości 0, która nie istnieje w tej drugiej. Sugerowałbym również, że jest to bardziej uzasadnione jako wybór podstawowego typu numerycznego dla komputerów cyfrowych, biorąc pod uwagę znaczenie 0.
Richard Cook
Nie rozumiem twojego UPD . Naturalne są bardziej fundamentalne niż liczby całkowite, a odpowiedzi dają przykłady, dlaczego tak jest.
Radu GRIGore,
Odp: UPD. Nie jestem zbyt pewien, dlaczego „ludzie z branży” byliby „rozczarowani”. (Swoją karierę sam spędziłem w branży.) Dlaczego ktoś miałby oczekiwać, że teoria powinna być oczywistym rozszerzeniem tego, co już zna? Dość często zdarza się, że pewne rzeczy wspólne w przemyśle, podobnie jak zmienne całkowite, są bardziej z powodów „historycznych” niż z głębokich teorii.
Marc Hamann,

Odpowiedzi:

24

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.

Neel Krishnaswami
źródło
20

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.

Marc Hamann
źródło
5
Kolejny powód: jeśli chcesz czegoś w rodzaju cyfr kościelnych, ujemna liczba całkowita musiałaby oznaczać odwrócenie funkcji. Tak więc w tym kontekście liczby całkowite byłyby bardziej naturalne w rachunku funkcji obliczeniowych bijectywnych.
Per Vognsen,
@Per Vognsen: nie wiem, w jaki sposób się tam kłócisz. Ale myślę, że można bezpiecznie powiedzieć, że obliczalne funkcje bijectywne są mniej podstawowe niż arbitralne funkcje obliczeniowe przez większość czasu. ;-)
Marc Hamann
Nie ma wątpliwości, że liczby zespolone, które znajdują się na szczycie hierarchii liczb Liczby naturalne -> Liczby całkowite -> Liczby wymierne -> Liczby rzeczywiste -> Liczby zespolone są bardziej fundamentalne niż inne, ponieważ mają „ładniejsze” właściwości algebraiczne. Są wszędzie w nauce, ale są wyraźnie nieobecni w „podstawach” matematyki. Zatem odpowiedź na to, co jest bardziej „podstawowymi” liczbami całkowitymi lub naturalnymi, naprawdę zależy od kogo zapytasz: algorytmisty lub algebraisty.
Tegiri Nenashi,
Ponieważ jest to strona TCS, myślę, że możemy bezpiecznie uprzywilejować widok informatyki. ;-) Pod względem obliczeniowym hierarchia ta jest progresywna: każdy nowy wpis jest dosłownie oparty na poprzednim. Ponieważ „fundamentalne” zwykle odnosi się do czegoś u podstawy, myślę, że cel natury jest odpowiedni do nadania tego tytułu.
Marc Hamann
17

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).NZ

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.NZ

Raphael
źródło
11

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.

Jacques Carette
źródło
Są języki, które mają podstawowy typ dla naturałów.
Raphael,
@Raphael: Wiem. Ale nie te, które inaczej lubię (mianowicie Haskell i OCaml). Nie jestem jeszcze gotowy, aby rozpocząć „programowanie” w Agdzie lub Coq.
Jacques Carette,
Co jest tak złego w ilorazach?
David Harris,
3
Ilości są świetne w semantyce. O wiele trudniej sobie z nimi poradzić w rzeczywistych obliczeniach i konkretnych reprezentacjach. Istnieją niezliczone artykuły na temat radzenia sobie z nimi w Coq, Isabelle, Agda, (ogólnie teoria typów) itp. Po prostu założyłem, że we wszystkich społecznościach wiedza o folklorze jest taka, że ​​iloraz jest tylko bólem w radzeniu sobie „w rzeczywistości”.
Jacques Carette
2
Wydaje mi się, że jest to najsilniejsza odpowiedź grupy: Naturals to najprostszy nietrywialny indukcyjny typ danych. po podaniu definicji i udowodnieniu prostych właściwości liczb naturalnych utorowałeś drogę dla bardziej złożonych typów danych indukcyjnych, takich jak listy lub drzewa.
cody
7

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.

Uday Reddy
źródło
6

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ć.

Dave Clarke
źródło
Miałem na myśli przede wszystkim wypisany rachunek lambda. Na tej podstawie opiera się przebieg książek, o których wspomniałem w pierwszym poście. Wydaje mi się, że obecnie niepoprawna lambda nie jest tak istotna w teorii typów i teorii PL (może się mylę, ale to właśnie widzę w tych książkach). W każdym razie dziękuję!
Artem Pelenitsyn,