Typentheorie

aus Wikipedia, der freien Enzyklopädie
Wechseln zu: Navigation, Suche
Racine carrée bleue.svg
Dieser Artikel wurde auf der Qualitätssicherungsseite des Portals Mathematik eingetragen. Dies geschieht, um die Qualität der Artikel aus dem Themengebiet Mathematik auf ein akzeptables Niveau zu bringen.

Bitte hilf mit, die Mängel dieses Artikels zu beseitigen, und beteilige dich bitte an der Diskussion! (Artikel eintragen)

In mathematischer Logik und theoretischer Informatik sind Typentheorien formale Systeme, in denen jeder Term einen Typ hat und Operationen auf bestimmte Typen beschränkt sind. Einige Typentheorien werden als Alternative zur axiomatischen Mengenlehre als Grundlage für die moderne Mathematik benutzt.

Typentheorien haben Überschneidungen mit Typsystemen, die ein Merkmal von Programmiersprachen zur Fehlervermeidung darstellen.

Zwei populäre Typentheorien, die als mathematische Grundlagen genutzt werden, sind Alonzo Churchs typisierter Lambda Kalkül und Per Martin-Löfs intuitionistische Typentheorie.

Weitere Einzelheiten[Bearbeiten]

Nach der Typentheorie gibt es einfache Mengen, welche lediglich Urelemente, aber keine Mengen als Elemente enthalten können; Mengen des zweiten Typs können nur einfache Mengen enthalten, Mengen des dritten Typs nur Mengen des zweiten Typs usw. Mengen haben also einen um eins höheren Typ als ihre Elemente. Diese System beruht somit auf einer Stratifikation des Mengenbegriffs und vermeidet dadurch die Russellsche Antinomie, da die Darstellung der Menge aller sich nicht selbst enthaltenden Mengen schon aus syntaktischen Gründen nicht möglich ist, denn die dazu nötigen Aussagen x\in x und x\notin x sind syntaktisch nicht korrekt.

In einer kumulativen Typentheorie können in einer Menge beliebige Mengen niedrigerer Stufe oder Urelemente enthalten sein, wodurch ebenfalls die Russellsche Antinomie vermieden wird.

Die erste einfache Version der Typentheorie formulierte Russell im Jahr 1903 im Anhang seiner Principles of Mathematics, die zweite komplexere Version im Jahr 1908 in Mathematical Logic as based on the Theory of Types. Letztere wurde die Grundlage der berühmten Principia Mathematica, die er nach beinahe zehnjähriger Vorbereitungszeit zusammen mit Alfred North Whitehead ab 1910 veröffentlichte. Die einfache Typentheorie wird seit Ramsey auch Simplified Theory of Types (oder kurz STT) genannt; sie ist hinreichend zur Vermeidung der logischen Widersprüche wie der Russellschen Antinomie, aber nicht für die Lösung der semantischen Widersprüche wie der Grelling-Nelson-Antinomie; dies vermag erst seine wesentlich aufwendigere Ausgabe von 1908, die Ramified Theory of Types (RTT), die „verzweigte“ Typentheorie.

Diese Version der Typentheorie setzte sich wegen ihrer Kompliziertheit und eingeschränkten Leistungsfähigkeit nicht auf Dauer durch. Als bequemer und leistungsfähiger erwies sich die von Ernst Zermelo 1907 entwickelte axiomatische Mengenlehre, die Abraham Fraenkel 1922 erweiterte und die heute als Zermelo-Fraenkel-Mengenlehre, kurz ZF, bekannt und als Basis der Mathematik weitgehend anerkannt ist. Zudem hat man in ZF eine zum Fundierungsaxiom äquivalente Von-Neumann-Hierarchie, die eine Art Stratifikation darstellt, aber keine weiteren Restriktionen mit sich bringt. Die Stufen oder Ränge der Mengen entsprechen zudem einer kumulativen Typentheorie.

Eine vereinfachte Variante der Typentheorie entwarf Quine 1937 in seinen New Foundations.

Typentheorien spielen eine wichtige Rolle in der Theorie der Programmiersprache und in darauf basierenden Programmiersprachen und computergestützten Beweissystemen wie Coq und Agda (dependent types).

Homotopietypentheorie[Bearbeiten]

Homotopietypentheorie (HoTT) bezeichnet Entwicklungen der intensionalen Typentheorie, basierend auf der Interpretation von Typen als Objekte der Homotopietheorie. Homotopietypentheorie kann als Alternative zur Mengenlehre als Grundlage für jegliche Mathematik benutzt werden. Aktuelle Forschung umfasst deshalb u. a. die Formulierung herkömmlicher Mathematik auf Grundlage von Typentheorie und die Umsetzung in Beweisassistenten.

Im akademischen Jahr 2012/2013 entstand in einem gemeinsamen Forschungsprojekt am Institute for Advanced Study ein Buch über die Grundlagen dieser Disziplin.[1]

Literatur[Bearbeiten]

Weblinks[Bearbeiten]

Einzelnachweise[Bearbeiten]

  1. homotopytypetheory.org, die zentrale Website der beteiligten Wissenschaftler.