Standardowe konstruktywne definicje liczb całkowitych, racjonalnych i rzeczywistych?

Liczby naturalne są definiowane indukcyjnie jako (na przykładzie składni Coq)

Inductive nat: Set :=
| O: nat
| S: nat -> nat.

Czy istnieje standardowy sposób konstruktywnego definiowania liczb całkowitych (a może innych zbiorów, takich jak racjonalne i rzeczywiste)?

Istnieje wiele sposobów definiowania struktury matematycznej, w zależności od właściwości, które uznajesz za definicję. Pomiędzy równoważnymi charakterystykami, które przyjmujesz za definicję, a którą bierzesz za alternatywną, nie jest ważne.

W konstruktywnej matematyce lepiej jest wybrać definicję, która ułatwia konstruktywne rozumowanie. W przypadku liczb naturalnych podstawową formą rozumowania jest indukcja, co sprawia, że ​​tradycyjna definicja zera lub następcy jest bardzo odpowiednia. Inne zestawy liczb nie mają takich preferencji.

Rozważając iloraz, w niekonstruktywnych ustawieniach często mówi się „wybierz członka klasy równoważności”. W konstruktywnym otoczeniu konieczne jest opisanie sposobu wyboru członka. Ułatwia to posługiwanie się definicjami konstruującymi jeden obiekt dla każdego elementu typu, zamiast konstruowania klas równoważności.

Na przykład, aby zdefiniować $\mathbb{Z}$matematyk może być zadowolony z wyrównania różnic liczb naturalnych:

Inductive Z1 :=
  | Nonnegative : nat -> Z1   (* ⟦Nonnegative x⟧ = ⟦x⟧ *)
  | Negative : nat -> Z1.     (* ⟦Negative x⟧ = -⟦x⟧-1 *)

Jednak ta definicja jest dziwnie asymetryczna, co może sprawić, że lepiej będzie przyjąć dwie różne reprezentacje dla zera:

Inductive Z2 :=
  | Nonnegative : nat -> Z2   (* ⟦Nonnegative x⟧ = ⟦x⟧ *)
  | Nonpositive : nat -> Z2.  (* ⟦Nonpostitive x⟧ = -⟦x⟧ *)

Lub możemy zbudować względne liczby całkowite bez użycia elementów naturalnych jako elementu budulcowego:

Inductive Pos3 :=
  | I : Pos3                  (* ⟦I⟧ = 1 *)
  | S3 : Pos3 -> Pos3         (* ⟦S3 x⟧ = ⟦x⟧+1 *)
Inductive Z3 :=
  | N3 : Pos3 -> Z3           (* ⟦N3 x⟧ = -⟦x⟧ *)
  | O3 : Z3                   (* ⟦O3⟧ = 0 *)
  | P3 : Pos3 -> Z3           (* ⟦P3 x⟧ = ⟦x⟧ *)

Standardowa biblioteka Coq używa jeszcze innej definicji: konstruuje dodatnie liczby całkowite z ich notacji to podstawa 2, ponieważ cyfra 1, po której następuje ciąg cyfr 0 lub 1. Następnie konstruuje Zjak Z3z Pos3góry. Ta definicja ma również unikalną reprezentację dla każdej liczby całkowitej. Wybór zapisu binarnego nie służy łatwiejszemu uzasadnieniu, ale produkuje bardziej wydajny kod, gdy programy są pobierane z proofów.

Łatwość rozumowania jest motywacją do wyboru definicji, ale nigdy nie jest czynnikiem nie do pokonania. Jeśli jakaś konstrukcja ułatwia konkretny dowód, można użyć tej definicji w tym konkretnym dowodzie i udowodnić, że konstrukcja jest równoważna z inną konstrukcją, która została pierwotnie wybrana jako definicja.

W przypadku liczb wymiernych trudno jest uciec od ilorazów, chyba że zaczniemy od przedstawienia liczb całkowitych jako iloczynu czynników (co powoduje pewne podstawowe operacje, takie jak dodawanie i całkowite uporządkowanie na $\mathbb{N}$trudne do zdefiniowania). Standardowa biblioteka Coq definiuje Qjako$\mathbb{N} \times \mathbb{N}^*$(licznik i mianownik) i definiuje operator =?=do testowania równoważności dwóch elementów Q. Ta definicja jest dość powszechna, ponieważ jest tak prosta, jak to tylko możliwe.

Liczby rzeczywiste to zupełnie inny czajnik ryb, ponieważ nie można ich zbudować. Nie można zdefiniować liczb rzeczywistych jako typu indukcyjnego (wszystkie typy indukcyjne są policzalne). Zamiast tego każda definicja liczb rzeczywistych musi być aksjomatyczna, tzn. Niekonstruktywna. Możliwe jest konstruowanie znacznych podzbiorów liczb rzeczywistych; sposób na zrobienie tego zależy od tego, jaki podzbiór chcesz zbudować.

Odpowiedź Gillesa jest dobra, z wyjątkiem akapitu dotyczącego liczb rzeczywistych, który jest całkowicie fałszywy, z wyjątkiem faktu, że liczby rzeczywiste są rzeczywiście innym kotłem ryb. Ponieważ tego rodzaju dezinformacje wydają się być dość rozpowszechnione, chciałbym tutaj zapisać szczegółową odpieralność.

Nie jest prawdą, że wszystkie typy indukcyjne są policzalne. Na przykład typ indukcyjny

Inductive cow := 
   | nose : cow
   | horn : (nat -> cow) -> cow.

nie jest policzalny, dla danej sekwencji, c : nat -> cowktórą możemy utworzyć, horn cktóra nie jest w sekwencji przez uzasadnione bydło. Jeśli chcesz poprawnego stwierdzenia w formie „wszystkie typy indukcyjne są policzalne”, musisz poważnie ograniczyć dozwolone konstrukcje.

Liczb rzeczywistych nie można łatwo skonstruować jako typ indukcyjny, z wyjątkiem tego, że w teorii typów homotopijnych można je konstruować jako wyższy typ indukcyjno-indukcyjny , patrz rozdział 11 książki HoTT . Można argumentować, że to oszustwo.

Istnieje wiele konstruktywnych definicji i konstrukcji reali, wbrew twierdzeniom Gillesa. Można je ogólnie podzielić na dwie klasy:

1. Konstrukcje typu Cauchy'ego, w których rzeczywistości są postrzegane jako metryczne uzupełnienie liczb wymiernych. Tego rodzaju konstrukcja często wymaga ilorazów, chociaż można uciec od definicji koiuktywnej, zależnej od tego, jak traktuje się równość. Naiwna konstrukcja zazwyczaj wymaga również policzalnego wyboru, ale Fred Richman dał procedurę ukończenia, która działa konstruktywnie bez wyboru, zobacz jego liczby rzeczywiste i inne uzupełnienia .

2. Konstrukcja typu Dedekind, w której realia są postrzegane jako (dwustronne) cięcia racjonalności. Tego rodzaju konstrukcja zwykle wymaga powersetów lub podobnego urządzenia, chociaż można to zrobić tylko za pomocą podstawowych$\lambda$-kalkul i aksjatyzacja przestrzeni Sierpińskiego $\Sigma$, zobacz realia Dedekind w Abstract Stone Duality .

Po stronie implementacji mamy różne konstruktywne formalizacje reali (ale nie ta w standardowej bibliotece Coq, która jest po prostu okropna), na przykład certyfikowane przez Robberta Krebbersa i Bas Spitters's Computer wydajne dokładne reale w Coq .

W celu rzeczywistej realizacji dokładnych liczb rzeczywistych wskazuję na iRRAM Norberta Müllera .

Wreszcie, uwaga Gillesa o niezliczonych podzbiorach reali jest poza wyznacznikiem. Zupełnie możliwe jest konstruowanie lub definiowanie niepoliczalnych zbiorów, niezależnie od tego, w jakim konstruktywnym otoczeniu żyjesz. Na przykład przestrzeń Baire$\mathbb{N} \to \mathbb{N}$wszystkich sekwencji liczb jest zawsze niepoliczalna, nawet jeśli uważasz, że każda funkcja jest obliczalna przez Turinga - zobacz wyjaśnienie na moim blogu .