Łatwo jest pomylić, co to znaczy „reprezentować” lub „implementować” liczbę rzeczywistą. W rzeczywistości jesteśmy świadkami dyskusji w komentarzach, w których reprezentacja jest sporna. Więc pozwól mi zająć się tym pierwszym.
Skąd wiemy, że wdrożenie jest prawidłowe?
Teorią, która wyjaśnia, jak reprezentować rzeczy w komputerze, jest wykonalność . Podstawową ideą jest to, że biorąc pod uwagę zbiór , wybieramy typ danych τ i każdemu x ∈ X zbiór wartości typu τ, które go realizują . Piszemy v ⊢ x ∈ X, gdy v jest wartością, która realizuje x . Na przykład (użyję Haskell bez powodu) rozsądną implementacją może być typ danych, gdzie gdy ma wartość liczbowąXτx∈Xτv⊢x∈Xvx v ⊢ k ∈ N v ¯ k T r u e ⊢ 42 ∈ N F a l s e ⊢ n ∈ N dla n ≠ 42 . Dlaczego to jest nieprawidłowe? Potrzebujemykryterium.NInteger
v⊢k∈Nvk¯¯¯ (a zatem w szczególności -42
nie reprezentuje liczby naturalnej, podobnie jak program rozbieżny). Ale jakiś joker mógłby przejść obok i zasugerować, że używamy Bool
do reprezentowania liczb naturalnych za pomocą iTrue⊢42∈NFalse⊢n∈Nn≠42
W przypadku „liczb jokera” łatwo zauważyć, że dodawanie nie może zostać zaimplementowane. Przypuśćmy, że powiem ci, że mam dwie liczby, obie reprezentowane przez . Czy możesz podać realizatora za ich sumę? Zależy to od tego, czy suma wynosi 42, ale nie można powiedzieć. Ponieważ dodawanie jest „istotną częścią liczb naturalnych”, jest to niedopuszczalne. Innymi słowy, implementacja nie polega na zestawach, ale na strukturach , tzn. Musimy reprezentować zestawy w taki sposób, aby możliwe było również zaimplementowanie odpowiedniej struktury. Pozwól mi podkreślić:False
Wdrażamy struktury, a nie nagie zestawy. Dlatego musimy być w stanie zaimplementować całą strukturę, wraz z operacjami i wszystkimi aksjomatami, aby implementacja była poprawna.
Jeśli nie przestrzegasz tej zasady, musisz zasugerować alternatywne matematyczne kryterium poprawności. Nie znam żadnego.
Przykład: reprezentacja liczb naturalnych
W przypadku liczb naturalnych odpowiednią strukturę opisują aksjomaty Peano, a kluczowym aksjomatem, który należy zaimplementować, jest indukcja (ale także , następca, + i × ). Możemy obliczyć, wykorzystując wykonalność, to, co robi implementacja indukcyjna. Okazuje się, że jest to mapa (gdzie jest jeszcze nieznany typ danych reprezentujący liczby naturalne)0+×nat
induction : 'a -> (nat -> 'a -> 'a) -> 'nat -> 'a
satysfakcjonujący induction x f zero = x
i induction x f (succ n) = f n (induction x f n)
. Wszystko to wynika z wykonalności. Mamy kryterium: implementacja liczb naturalnych jest poprawna, gdy pozwala na implementację aksjomatów Peano. Podobny wynik można by uzyskać, jeśli stosuje się charakterystykę liczb jako początkowy Algebra do funktora .X↦1+X
Prawidłowa implementacja liczb rzeczywistych
Zwróćmy uwagę na liczby rzeczywiste i pytanie. Pierwszym pytaniem, jakie należy zadać, jest: „jaka jest odpowiednia struktura liczb rzeczywistych?” Odpowiedź brzmi: Archimedesowe Cauchy wypełnia uporządkowane pole . Takie jest ustalone znaczenie „liczb rzeczywistych”. Nie możesz go zmienić, zostało to naprawione przez innych dla ciebie (w naszym przypadku alternatywne realia Dedekinda okazują się izomorficzne z realiami Cauchy'ego, które rozważamy tutaj.) Nie możesz go zabrać, nie wolno Ci mówić „Nie dbam o wdrożenie dodawania” lub „Nie dbam o zamówienie”. Jeśli to zrobisz, nie możesz nazywać go „liczbami rzeczywistymi”, ale coś w rodzaju „liczb rzeczywistych, w których zapominamy o porządku liniowym”.
Nie będę wchodził w wszystkie szczegóły, ale wyjaśnię, w jaki sposób różne części struktury dają różne operacje na rzeczywistych elementach:
- Archimedesa aksjomat jest o obliczenie racjonalnych przybliżenia liczb rzeczywistych
- struktura pola daje zwykłe operacje arytmetyczne
- kolejność liniowa daje nam półdecydowalną procedurę testowania x<y
- kompletność Cauchy daje nam funkcję
lim : (nat -> real) -> real
, która pobiera (reprezentacji) szybki ciągiem Cauchy'ego i zwraca swój limit. (Sekwencja jest szybka, jeśli | x n - x m | ≤ 2 min ( n , m ) dla wszystkich m , n .)(xn)n|xn−xm|≤2min(n,m)m,n
Czego nie otrzymujemy, to funkcja testowa równości. Nie ma nic w aksjomatów dla liczb rzeczywistych, które prosi być rozstrzygalne. (Przeciwnie, aksjomaty Peano sugerują, że liczby naturalne są rozstrzygalne, a można to udowodnić, stosując ćwiczenie wyłącznie jako zabawę).=eq : nat -> nat -> Bool
induction
Faktem jest, że zwykła dziesiętna reprezentacja rzeczywistości, której używa ludzkość, jest zła, ponieważ nie możemy nawet wprowadzić dodawania. Punkt zmiennoprzecinkowy z nieskończoną mantysą również zawodzi (ćwiczenie: dlaczego?). Co działa, jednak jest podpisany cyfrową reprezentację, czyli ten, w którym pozwoli negatywne cyfr, jak również pozytywne. Lub możemy użyć sekwencji racjonalnych, które spełniają szybki test Cauchy'ego, jak stwierdzono powyżej.
Reprezentacja Tsuyoshi również coś implementuje, ale nie R
Rozważmy następującą reprezentację liczb rzeczywistych: rzeczywisty jest reprezentowany przez parę ( q , b ), gdzie ( q n ) n jest szybką sekwencją Cauchyego zbiegającą się z x, a b jest wartością logiczną wskazującą, czy x jest liczbą całkowitą. Aby było to przedstawienie rzeczywistych wartości, musielibyśmy zaimplementować dodawanie, ale jak się okazuje, nie możemy obliczyć flag boolowskich. To nie jest przedstawienie rzeczywistości. Ale nadal coś reprezentuje, a mianowicie podzbiór rzeczywistości Z ∪ ( R ∖ Z )x( q, b )( qn)nxbxZ ∪( R ∖ Z ). Rzeczywiście, zgodnie z interpretacją realizowalności związek jest realizowany z flagą wskazującą, które część unii jesteśmy w. Przy okazji, jest nie równa się R , chyba że wierzą w wyłączonego środka, który nie może zostać wdrożony i dlatego jest dość nieistotny dla tej dyskusji. Jesteśmy zmuszeni przez komputery do robienia rzeczy intuicyjnie.Z ∪( R ∖ Z )R
Nie możemy sprawdzić, czy wartość rzeczywista jest liczbą całkowitą
Na koniec pozwól mi odpowiedzieć na zadane pytanie. Wiemy teraz, że akceptowalną reprezentacją reali są szybkie sekwencje racjonalne Cauchy'ego. (Ważne twierdzenie głosi, że dowolne dwa przedstawienia rzeczywistości, które są dopuszczalne, są w rzeczywistości obliczalne izomorficzne.)
Twierdzenie: Testowanie, czy real jest liczbą całkowitą, nie jest rozstrzygalne.
Dowód. Załóżmy, że moglibyśmy sprawdzić, czy rzeczywista jest liczbą całkowitą (oczywiście rzeczywista jest realizowana przez szybką sekwencję Cauchy'ego). Ideą, która pozwoli ci udowodnić znacznie bardziej ogólne twierdzenie, jeśli chcesz, jest skonstruowanie szybkiej sekwencji Cauchy'ego liczb całkowitych, która zbiega się w liczbę całkowitą. Jest to łatwe, wystarczy wziąć x n = 2 - n . Następnie rozwiąż problem zatrzymania w następujący sposób. Biorąc pod maszyną Turinga T , określa się nową sekwencję ( R n ) n o
r n = { X n jeżeli T( xn)nxn= 2- nT.( yn)n
Oznacza to, że nowy wygląd sekwencji lubią sekwencji(xn)ntak długo, jakTtras, ale potem robi się „Stuck” naxmifTzatrzymuje się w krokum. Co bardzo ważne, nowa sekwencja jest również szybką sekwencją Cauchy'ego (i możemy to udowodnić, nie wiedząc, czyT sięzatrzyma). Dlatego możemy obliczyć jego limitz=limnyn
yn= { xnxmjeśli T nie zatrzymał się w ciągu n krokówjeśli T zatrzymywana na etapie m i m ≤ N
( xn)nT.xmT.mT.z= limnyn, ponieważ nasza reprezentacja reali jest poprawna. Sprawdź, czy
jest liczbą całkowitą. Jeśli tak, to musi być
0, a dzieje się tak tylko wtedy, gdy
T działa wiecznie. W przeciwnym razie
z nie jest liczbą całkowitą, więc
T musiał się zatrzymać. CO BYŁO DO OKAZANIA.
z0T.zT.
Ćwiczenie: dostosuj powyższy dowód, aby pokazać, że nie możemy testować liczb wymiernych. Następnie dostosuj go, aby pokazać, że nie możemy testować niczego nietrywialnego (jest to nieco trudniejsze).
Czasami ludzie są zdezorientowani całym tym biznesem testowania. Uważają, że udowodniliśmy, że nigdy nie możemy sprawdzić, czy rzeczywista liczba całkowita. Ale z pewnością 42 to prawda i możemy stwierdzić, czy jest liczbą całkowitą. W rzeczywistości każdy szczególności rzeczywistym możemy wymyślić, , 88 ln 89 , e gatunku √grzech1188 ln89 itd., Możemy doskonale stwierdzić, czy są to liczby całkowite. Dokładniemożemypowiedzieć, ponieważmamydodatkowe informacje: te liczby nie są nam przekazywane jako sekwencje, ale raczej jako wyrażenia symboliczne, z których możemy obliczyć bit Tsuyoshi. Tak szybko, jak tylko mamy informacji o rzeczywistym jest sekwencją racjonalnych przybliżeń zbieżnych z nim (i mamnieznaczy symboliczny wyraz opisujący sekwencję, ale czarną skrzynkę, która wyprowadzan-tej termin na wejściun) wtedy będzie tak samo bezradny jak maszyny.miπ163√nn
Morał tej historii
Nie ma sensu rozmawiać o implementacji zestawu, chyba że wiemy, jakie operacje chcemy na nim wykonać.