Typentheorie

aus Wikipedia, der freien Enzyklopädie
Wechseln zu: Navigation, Suche

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.

Geschichte[Bearbeiten | Quelltext bearbeiten]

Zwischen 1902 und 1908 schlug Bertrand Russell verschiedene Typentheorien vor, mit denen die Russellsche Antinomie der naiven Mengenlehre Gottlob Freges vermieden werden sollte. Seine "verzweigte" Typentheorie und das Reduzibilitätsaxiom spielten eine wichtige Rolle in den zwischen 1910 und 1913 veröffentlichten Principia Mathematica. Whitehead und Russell versuchten dort, Russells Paradoxon durch eine Hierarchie von Typen zu vermeiden, wobei jeder mathematischen Entität ein Typ zuzuordnen ist. Objekte eines bestimmten Typs können nur aus Objekten niederen Typs aufgebaut sein, so dass Schleifen vermieden werden. In den 1920er Jahren schlugen Leon Chwistek und Frank P. Ramsey eine einfachere Theorie vor, die heute als "einfache Typentheorie" bekannt ist.

Üblicherweise besteht eine Typentheorie aus Typen und einem Termersetzungssystem. Ein bekanntes Beispiel ist der Lambda-Kalkül. Auf ihm basiert die Logik höherer Stufe.

In einigen Bereichen der konstruktiven Mathematik und auch für den Beweisassistenten Agda wird die intuitionistische Typentheorie verwendet. Dagegen beruht der Beweisassistent Coq auf dem Konstruktionskalkül CoC. Ein aktives Forschungsgebiet ist die Homotopietypentheorie.

Grundlegende Konzepte[Bearbeiten | Quelltext bearbeiten]

In einer Typentheorie hat jeder Term einen Typ und Operationen werden nur für Terme eines bestimmten Typs definiert. Ein Typurteil besagt, dass der Term vom Typ ist. Zum Beispiel ist der Typ der natürlichen Zahlen und sind Terme von diesem Typ. ist das Urteil, dass vom Typ ist.

Eine Funktion wird in der Typentheorie durch einen Pfeil bezeichnet. Die Nachfolger-Funktion hat das Urteil . Der Aufruf einer Funktion wird gelegentlich auch ohne Klammer geschrieben, also anstelle von

Eine Typentheorie kann auch Termumformungsregeln enthalten. Zum Beispiel sind und syntaktisch unterschiedliche Terme, der erste läßt sich aber auf den zweiten reduzieren. Man schreibt .

Typentheorien[Bearbeiten | Quelltext bearbeiten]

Lambda-Kalkül (nach Church)[Bearbeiten | Quelltext bearbeiten]

Hauptartikel: Lambda-Kalkül

Alonzo Church benutzte den Lambda-Kalkül, um 1936 sowohl eine negative Antwort auf das Entscheidungsproblem zu geben als auch eine Fundierung eines logischen Systems zu finden, wie es den Principia Mathematica von Bertrand Russell und Alfred North Whitehead zugrunde lag. Mittels des untypisierten Lambda-Kalküls kann man klar definieren, was eine berechenbare Funktion ist. Die Frage, ob zwei Lambda-Ausdrücke (s. u.) äquivalent sind, kann im Allgemeinen nicht algorithmisch entschieden werden. In seiner typisierten Form kann der Kalkül benutzt werden, um Logik höherer Stufe darzustellen. Der Lambda-Kalkül hat die Entwicklung funktionaler Programmiersprachen, die Forschung um Typsysteme von Programmiersprachen im Allgemeinen sowie moderne Teildisziplinen in der Logik wie die Typtheorie wesentlich beeinflusst.

Intuitionistische Typentheorie (nach Martin-Löf)[Bearbeiten | Quelltext bearbeiten]

Die intuitionistische Typentheorie nach Per Martin-Löf ist eine auf den Prinzipien des Konstruktivismus aufbauende Typentheorie und alternative Grundlegung der Mathematik.

Sie beruht auf einer Analogie zwischen Propositionen und Typen: eine Proposition wird mit dem Typ ihres Beweises identifiziert.

Calculus of Constructions (nach Coquand)[Bearbeiten | Quelltext bearbeiten]

Die Typentheorie Calculus of Constructions (CoC) nach Thierry Coquand ist ein Lambda-Kalkül höherer Ordnung, der die Grundlage sowohl für einen konstruktiven Aufbau der Mathematik als auch für das computerisierte Beweissystem Coq ist.

Homotopietypentheorie[Bearbeiten | Quelltext bearbeiten]

Die Homotopietypentheorie (HoTT) bezeichnet Entwicklungen der intensionalen Typentheorie von Martin-Löf, basierend auf der Interpretation von Typen als Objekte der Homotopietheorie (Vladimir Voevodsky). 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 | Quelltext bearbeiten]

Weblinks[Bearbeiten | Quelltext bearbeiten]

Einzelnachweise[Bearbeiten | Quelltext bearbeiten]

  1. Homotoppy Type Theorie: Univalent Foundations (pdf)