Setoid - Setoid
In der Mathematik ist ein Setoid ( X , ~) eine Menge (oder ein Typ ) X, die mit einer Äquivalenzbeziehung ~ ausgestattet ist. Ein Setoid kann auch als E-Set , Bishop- Set oder Extension-Set bezeichnet werden .
Setoids sind vor allem in studierte Beweistheorie und in Art theoretischen Grundlagen der Mathematik . Wenn man in der Mathematik eine Äquivalenzrelation für eine Menge definiert, bildet man häufig sofort die Quotientenmenge (Umwandlung von Äquivalenz in Gleichheit ). Im Gegensatz dazu können Setoide verwendet werden, wenn ein Unterschied zwischen Identität und Äquivalenz beibehalten werden muss, häufig mit einer Interpretation der Intensitätsgleichheit (die Gleichheit auf der ursprünglichen Menge) und der Extensionsgleichheit (die Äquivalenzbeziehung oder die Gleichheit auf der Quotientensatz).
Beweistheorie
In der Beweistheorie, insbesondere in der Beweistheorie der konstruktiven Mathematik, die auf der Curry-Howard-Korrespondenz basiert , identifiziert man häufig einen mathematischen Satz mit seinen Beweisen (falls vorhanden). Ein gegebener Satz kann natürlich viele Beweise haben; Nach dem Prinzip der Beweisrelevanz ist normalerweise nur die Wahrheit des Satzes von Bedeutung, nicht welcher Beweis verwendet wurde. Die Curry-Howard-Korrespondenz kann jedoch Beweise in Algorithmen verwandeln , und Unterschiede zwischen Algorithmen sind häufig wichtig. Daher können Beweistheoretiker es vorziehen, einen Satz mit einer Reihe von Beweisen zu identifizieren, wobei Beweise als gleichwertig angesehen werden, wenn sie durch Beta-Konvertierung oder dergleichen ineinander umgewandelt werden können .
Typentheorie
In typentheoretischen Grundlagen der Mathematik können Setoide in einer Typentheorie verwendet werden, der Quotiententypen fehlen , um allgemeine mathematische Mengen zu modellieren. Zum Beispiel in Per Martin-Löf ‚s intuitionistic Typen Theorie gibt es keine Art von reellen Zahlen , nur eine Art von regelmäßigen Cauchyfolgen von rationalen Zahlen . Um eine echte Analyse in Martin-Löfs Rahmen durchzuführen , muss man daher mit einem Setoid reeller Zahlen arbeiten, der Art regulärer Cauchy-Sequenzen, die mit dem üblichen Begriff der Äquivalenz ausgestattet sind. Prädikate und Funktionen reeller Zahlen müssen für reguläre Cauchy-Sequenzen definiert und als mit der Äquivalenzbeziehung kompatibel erwiesen werden. Typischerweise (obwohl dies von der verwendeten Typentheorie abhängt) gilt das Axiom der Wahl für Funktionen zwischen Typen (Intensionsfunktionen), nicht jedoch für Funktionen zwischen Setoiden (Erweiterungsfunktionen). Der Begriff "Menge" wird verschiedentlich entweder als Synonym für "Typ" oder als Synonym für "Setoid" verwendet.
Konstruktive Mathematik
In der konstruktiven Mathematik nimmt man oft ein Setoid mit einer Apartness-Beziehung anstelle einer Äquivalenzrelation, die als konstruktives Setoid bezeichnet wird. Manchmal betrachtet man auch einen partiellen Setoid unter Verwendung einer partiellen Äquivalenzbeziehung oder einer partiellen Apartheit. (siehe zB Barthe et al. , Abschnitt 1)
Siehe auch
Anmerkungen
- ^ Alexandre Buisse, Peter Dybjer, "Die Interpretation der intuitionistischen Typentheorie in lokal kartesischen geschlossenen Kategorien - eine intuitionistische Perspektive" , Electronic Notes in Theoretical Computer Science 218 (2008) 21–32.
-
^ "Bischofssatztheorie" (PDF) : 9. Zitierjournal benötigt
|journal=( Hilfe )
Verweise
- Hofmann, Martin (1995), "Ein einfaches Modell für Quotiententypen", Typisierte Lambda-Kalküle und -Anwendungen (Edinburgh, 1995) , Lecture Notes in Comput. Sci., 902 , Berlin: Springer, S. 216–234, CiteSeerX 10.1.1.55.4629 , doi : 10.1007 / BFb0014055 , ISBN 978-3-540-59048-4, MR 1477985.
- Barthe, Gilles; Capretta, Venanzio; Pons, Olivier (2003), "Setoids in Type Theory" (PDF) , Journal of Functional Programming , 13 (2): 261–293, doi : 10.1017 / S0956796802004501 , MR 1985376.