Was waren die Forschungsergebnisse des Univalent Foundations Program-Jahres (Homotopy Type Theory)?

7

Das Institute for Advanced Study hat ein einjähriges Sonderprogramm für das Univalent Foundations-Programm durchgeführt .

Am Ende haben sie ein Buch und ein Code-Repository erstellt .

Am Ende sehen wir einen Blogeintrag in Scientific American, der behauptet:

... könnte eine neue, in sich geschlossene Grundlage für die gesamte Mathematik bilden.

Dies ist eine kühne Behauptung. Im Gegensatz dazu kann ich bescheidenere Behauptungen wie einen einfachen Beweis in Agda sehen, dass die Summe zweier Gewinnchancen immer gerade ist .

Meine Frage ist: Welche neuartigen Forschungsergebnisse haben diese Leute Ende des Jahres tatsächlich produziert? Der Artikel zeigt nur, dass sie Code in Agda geschrieben haben. Ist es nur so, dass wir mit einigen Anwendungen eine neue Sicht auf die Martin-Löf-Typentheorie haben?

Annahmen

  • Ich verstehe die umfassenderen Ideen der Martin-Löf-Typentheorie in Bezug auf den Isomorphismus zwischen Typen und Beweisen.
homotopy-type-theory Falkenauge
quelle
2
Ich sehe keinen Zusammenhang zwischen dem Univalent Foundations-Programm und dem Simple Agda-Beweis.
Dave Clarke
Meine Frage war, worauf sich "ihre Agda / Coq-Beweise" summierten. Ich präsentierte ein einfaches Beispiel eines anderen gut geschriebenen Agda-Beweises, der nicht behauptete, die Grundlage der Mathematik zu sein.
Hawkeye
1
Riesenäpfel gegen kleine Orangen.
Dave Clarke

Antworten:

7

Das Buch selbst ist repräsentativ für das Forschungsprodukt des Programms. Der Code, den sie tatsächlich geschrieben haben, ist meines Wissens hauptsächlich in Coq, und sicherlich wurde die Entwicklung, die das Buch begleitet, in Coq geschrieben.

Die Homotopietypentheorie selbst bildet im Wesentlichen Martin-Löf zusammen mit dem Univalenzaxiom , das im Wesentlichen besagt, dass äquivalente Typen gleich sind. Der Begriff der Äquivalenz stammt aus einer Sicht, die eine Verbindung zwischen einer synthetischen Homotopietheorie und der Martin-Löf-Typentheorie herstellt, daher der Name. Dieses Axiom weicht einer mächtigen Typentheorie, von der das Buch zeigt, dass sie in der Lage ist, über viele wichtige existierende Grundlagen der Mathematik nachzudenken.

Tatsächlich enthält Teil 2 des Buches Entwicklungen einer traditionelleren, topologisch motivierten Version der Homotopietheorie, der Mengenlehre, der Kategorietheorie und einer schönen konstruktiven Darstellung der reellen Zahlen. Ich habe den Coq-Code noch nicht so ausführlich untersucht, aber ich verstehe, dass alle diese Präsentationen von einer entsprechenden Coq-Quelle begleitet werden. Da wir all diese wichtigen Grundlagen vollständig innerhalb der Homotopietypentheorie formulieren können, ist die Hypothese, dass dies eine wichtige Grundlage für die künftige Mathematik sein könnte, sinnvoll. Die Idee ist, dass Mathematiker diese wegweisenden Entwicklungen auf mehr Ergebnisse in Bereichen wie Algebra, Topologie und Analyse ausweiten können.

Da sich die Homotopietypentheorie auf die Fähigkeit bezieht, in Coq über die Curry-Howard-Korrespondenz Mathematik zu üben, können Sie sich die Homotopietypentheorie als eine leistungsfähigere Instanz von Curry-Howard vorstellen. Der aufregendste Beitrag dieser Arbeit ist wirklich, dass sie Mathematikern die Sprache gibt, um über Mathematik in Bezug auf die Typentheorie zu sprechen, und die Idee ist, dass dies einerseits ermöglichen sollte, dass mehr Mathematik von mechanisierten Beweisen in Beweisen wie Coq, as begleitet wird sowie Computer-Proofs, die ihren einfachen englischen Entsprechungen besser entsprechen. Jeder, der Coq verwendet hat, wird Ihnen sagen, dass die von Ihnen erstellten Proofs häufig nicht wie vergleichbare Proofs im Klartext aussehen.

Ethan A. Kuefner
quelle
Sie sagen also im Wesentlichen, dass sie einige Zeit damit verbracht haben, die Bausteine ​​zu bearbeiten - aber sie haben noch nichts von Bedeutung ergeben.
Hawkeye
2
Es kommt wirklich darauf an, was Sie unter "Konsequenz" verstehen. Einige wirklich nicht triviale Theoreme (wie ) wurden in diesem Rahmen formal bewiesen, mit dem Vorteil, dass sowohl der Ausdruck als auch der Beweis mit dieser neuen Formulierung relativ einfach sind. Der Blog hat viele Diskussionen über solche Ergebnisse. homotopytypetheory.org/blogπ1(S.1)=Z.
cody
Was meinst du mit "synthetischer Homotopietheorie"?
Jonaprieto
2
@jonaprieto Synthetische Homotopietheorie bedeutet, dass wir Theoreme über die Homotopietypen von Räumen ableiten, indem wir nur modellinvariante Eigenschaften dieser Typen und keine spezifischen Modelle wie CW-Komplexe, topologische Räume oder einfache Mengen verwenden. Dies ist analog zu z. B. der synthetischen euklidischen Geometrie, die Theoreme durch direkte Manipulation mit Kurven unter Verwendung geometrischer Konstruktionen beweist, im Gegensatz zum analytischen Ansatz, bei dem eine der nicht eindeutigen Codierungen dieser Kurven als Lösungen für Gleichungen ausgewählt und Gleichungen manipuliert werden.
Anton Fetisov
In ähnlicher Weise können wir in der synthetischen Homotopietheorie über die Kontraktionsfähigkeit bestimmter Räume, über Pfadfibrationen und Homotopien sprechen, aber wir können zB nicht über die Menge der Punkte eines Raums sprechen, sondern homotopieäquivalente Räume unterscheiden, wie z R.n für verschiedene noder verwenden Sie nichtinvariante Homotopieeigenschaften wie die Definition eines Kreises als Teilmenge in R.2(da das Flugzeug und alle seine Teilmengen zusammenziehbar sind).
Anton Fetisov