Konstruktive Standarddefinitionen von ganzen Zahlen, Rationalen und Realen?

Natürliche Zahlen werden induktiv definiert als (am Beispiel der Coq-Syntax)

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

Gibt es eine Standardmethode, um Ganzzahlen (und möglicherweise andere Mengen wie Rationals und Reals) konstruktiv zu definieren?

Es gibt mehrere Möglichkeiten, eine mathematische Struktur zu definieren, je nachdem, welche Eigenschaften Sie als Definition betrachten. Zwischen äquivalenten Charakterisierungen ist es nicht wichtig, welche Sie als Definition und welche als alternative Charakterisierung betrachten.

In der konstruktiven Mathematik ist es vorzuziehen, eine Definition zu wählen, die das konstruktive Denken erleichtert. Für natürliche Zahlen ist die Grundform des Denkens die Induktion, was die traditionelle Null-oder-Nachfolger-Definition sehr gut geeignet macht. Andere Zahlenreihen haben keine solche Präferenz.

Wenn Sie in nicht konstruktiven Umgebungen über Quotienten nachdenken, wird häufig gesagt, dass Sie ein Mitglied der Äquivalenzklasse auswählen. In einer konstruktiven Umgebung muss beschrieben werden, wie ein Mitglied ausgewählt wird. Dies erleichtert die Verwendung von Definitionen, die für jedes Element des Typs ein Objekt erstellen, anstatt Äquivalenzklassen zu erstellen.

Um beispielsweise zu definieren , könnte ein Mathematiker glücklich sein, Unterschiede natürlicher Zahlen gleichzusetzen: Z : = N 2 / { ( ( x , y ) , ( x ' , y ' ) ) ∣ x + y ' = x ' + y $\mathbb{Z}$

$$\mathbb{Z} := \mathbb{N}^2 / \{((x,y),(x',y')) \mid x + y' = x' + y\}$$ Während dies ein ordentliches Gefühl hat (kein „dies oder das“), ist es für konstruktives Denken einfacher, wenn die Gleichheit von Objekten mit der Gleichheit von Darstellungen übereinstimmt, sodass wir die relativen ganzen Zahlen entweder als natürliche Zahl oder als Negativ von a definieren können natürliche Zahl minus eins:

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

Diese Definition ist jedoch seltsamerweise asymmetrisch, weshalb es vorzuziehen ist, zwei verschiedene Darstellungen für Null zuzulassen:

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

Oder wir können die relativen Ganzzahlen erstellen, ohne die Naturwerte als Baustein zu verwenden:

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⟧ *)

Die Coq Standard - Bibliothek verwendet noch eine andere Definition: es konstruiert positive ganze Zahlen von ihrer Notation Basis 2, wie die Ziffer 1 durch eine Folge von Ziffern , gefolgt 0 oder 1. Es erstellt dann Zwie Z3von Pos3oben. Diese Definition hat auch eine eindeutige Darstellung für jede Ganzzahl. Die Wahl der binären Notation dient nicht der einfacheren Argumentation, sondern der Erzeugung eines effizienteren Codes, wenn Programme aus Proofs extrahiert werden.

Einfaches Denken ist eine Motivation bei der Auswahl einer Definition, aber niemals ein unüberwindbarer Faktor. Wenn eine Konstruktion einen bestimmten Beweis erleichtert, kann man diese Definition in diesem bestimmten Beweis verwenden und beweisen, dass die Konstruktion der anderen Konstruktion entspricht, die ursprünglich als Definition gewählt wurde.

$\mathbb{N}$Q$\mathbb{N} \times \mathbb{N}^*$=?=Q

Reelle Zahlen sind ein ganz anderer Fischkessel, weil sie nicht konstruierbar sind. Es ist unmöglich, die reellen Zahlen als induktiven Typ zu definieren (alle induktiven Typen sind denumerierbar). Stattdessen muss jede Definition der reellen Zahlen axiomatisch, dh nicht konstruktiv sein. Es ist möglich, denumerierbare Teilmengen der reellen Zahlen zu konstruieren; Die Vorgehensweise hängt davon ab, welche Teilmenge Sie erstellen möchten.

Gilles Antwort ist gut, mit Ausnahme des Absatzes über die reellen Zahlen, der völlig falsch ist, mit Ausnahme der Tatsache, dass die reellen Zahlen tatsächlich ein anderer Fischkessel sind. Da diese Art von Fehlinformation ziemlich weit verbreitet zu sein scheint, möchte ich hier eine detaillierte Gegenargumentation festhalten.

Es ist nicht wahr, dass alle induktiven Typen denumerierbar sind. Zum Beispiel der induktive Typ

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

ist nicht denumerierbar, für jede gegebene Sequenz, die c : nat -> cowwir bilden können, horn cdie nicht in der Sequenz durch Begründetheit des Viehs liegt. Wenn Sie eine korrekte Aussage der Form "Alle induktiven Typen sind zählbar" wünschen, müssen Sie die zulässigen Konstruktionen stark einschränken.

Die reellen Zahlen können nicht einfach als induktiver Typ konstruiert werden, außer dass sie in der Theorie des Homotopietyps als höherer induktiv-induktiver Typ konstruiert werden können , siehe Kapitel 11 des HoTT-Buches . Es könnte argumentiert werden, dass dies Betrug ist.

Entgegen der Behauptung von Gilles gibt es eine Reihe konstruktiver Definitionen und Konstruktionen der Realitäten. Sie können grob in zwei Klassen unterteilt werden:

1. Cauchy-artige Konstruktionen, bei denen die Realzahlen als metrische Vervollständigung der rationalen Zahlen angesehen werden. Diese Art der Konstruktion erfordert oft Quotienten, obwohl man möglicherweise mit einer koiunduktiven Definition davonkommen kann, abhängig davon, wie man mit Gleichheit umgeht. Eine naive Konstruktion erfordert normalerweise auch eine zählbare Auswahl, aber Fred Richman gab ein Abschlussverfahren an, das konstruktiv ohne Auswahl funktioniert, siehe seine reellen Zahlen und andere Vervollständigungen .

2. $\lambda$$\Sigma$

Auf der Implementierungsseite haben wir verschiedene konstruktive Formalisierungen von Reals (aber nicht die in der Coq-Standardbibliothek, die einfach schrecklich ist), zum Beispiel Robbert Krebbers und Bas Spitters ' Computer zertifizierte effiziente exakte Reals in Coq .

Für eine tatsächliche Implementierung exakter reeller Zahlen verweise ich Sie auf Norbert Müllers iRRAM .

$\mathbb{N} \to \mathbb{N}$