Typentheorie - Type theory

In der Mathematik , Logik und Informatik ist ein Typsystem ein formales System, in dem jeder Begriff einen "Typ" hat, der seine Bedeutung und die Operationen, die mit ihm ausgeführt werden können, definiert. Typtheorie ist die wissenschaftliche Erforschung von Typsystemen.

Einige Typentheorien dienen als Alternative zur Mengenlehre als Grundlage der Mathematik . Zwei bekannte solche Theorien sind Alonzo Church 's getippt λ-Kalkül und Per Martin-Löf ' s intuitionistic Typentheorie .

Die Typentheorie wurde geschaffen , um Paradoxien in früheren Grundlagen wie der naiven Mengenlehre , der formalen Logik und den Rewrite - Systemen zu vermeiden .

Die Typentheorie ist eng mit Computertypsystemen verwandt und überschneidet sich in einigen Fällen damit , die ein Feature der Programmiersprache sind, das verwendet wird, um Fehler zu reduzieren und bestimmte Compiler-Optimierungen zu erleichtern .

Geschichte

Zwischen 1902 und 1908 schlug Bertrand Russell als Reaktion auf seine Entdeckung, dass Gottlob Freges Version der naiven Mengenlehre von Russells Paradox betroffen war, verschiedene "Typentheorien" vor . 1908 kam Russell an einem „verästelten“ Theorie der Typen zusammen mit einem „ Axiom Reduzibilitätsaxiom “ beide in prominent Whitehead und Russell ‚s Principia Mathematica zwischen 1910 veröffentlicht und 1913 Sie versuchten Russells Paradox zu lösen , indem man zuerst eine Hierarchie zu schaffen von Typen und ordnet dann jede konkrete mathematische (und möglicherweise andere) Entität einem Typ zu. Entitäten eines bestimmten Typs werden ausschließlich aus Entitäten dieser Typen erstellt, die in ihrer Hierarchie niedriger sind, wodurch verhindert wird, dass eine Entität sich selbst zugewiesen wird.

In den 1920er Jahren schlugen Leon Chwistek und Frank P. Ramsey eine unverzweigte Typentheorie vor, die heute als "Theory of Simple Types" oder Simple Type Theory bekannt ist , die die Hierarchie der Typen in der früheren verzweigten Theorie zusammenbrach und als solche nicht erforderte das Axiom der Reduzierbarkeit.

Die gängige Verwendung von "Typentheorie" ist, wenn diese Typen mit einem Begriff-Rewrite-System verwendet werden . Das berühmteste frühe Beispiel ist Alonzo Church ‚s einfach typisierten Lambda - Kalkül . Churchs Typentheorie half dem formalen System, das Kleene-Rosser-Paradoxon zu vermeiden, das den ursprünglichen untypisierten Lambda-Kalkül betraf. Church demonstrierte, dass sie als Grundlage der Mathematik dienen kann und wurde als Logik höherer Ordnung bezeichnet .

Einige andere Art Theorien umfassen Per Martin-Löf ‚s intuitionistic Typ Theorie , die die Grundlage in einigen Bereichen verwendet wurde konstruktiven Mathematik . Thierry Coquand ‚s Kalkül von Konstruktionen und seine Derivate sind die Grundlage , die von Coq , Lean und andere. Das Gebiet ist ein Bereich aktiver Forschung, wie die Homotopietypentheorie zeigt .

Grundlegendes Konzept

Die zeitgemäße Darstellung von Typensystemen im Kontext der Typentheorie wurde durch einen von Henk Barendregt eingeführten konzeptionellen Rahmen systematisiert .

Typ, Begriff, Wert

In einem System der Typentheorie steht ein Begriff einem Typ gegenüber . Zum Beispiel 4 , 2 + 2 und sind alle separate Terme vom Typ nat für natürliche Zahlen. Traditionell folgt auf den Begriff ein Doppelpunkt und sein Typ, z. B. 2 : nat – dies bedeutet, dass die Zahl 2 vom Typ nat ist . Abgesehen von dieser Opposition und Syntax kann in dieser Allgemeinheit wenig über Typen gesagt werden, aber oft werden sie als eine Art Sammlung (nicht unbedingt als Mengen) der Werte interpretiert , auf die der Begriff ausgewertet werden könnte. Es ist üblich, Terme mit e und Typen mit τ zu bezeichnen . Wie Begriffe und Typen geformt werden, hängt vom jeweiligen Typsystem ab und wird durch einige Syntax und zusätzliche Einschränkungen der Wohlgeformtheit präzisiert . ${\displaystyle 2\cdot 2}$

Schreibumgebung, Typzuweisung, Typbeurteilung

Die Eingabe erfolgt normalerweise in einem Kontext oder einer Umgebung, die durch das Symbol gekennzeichnet ist . Eine Umgebung ist oft eine Liste von Paaren . Dieses Paar wird manchmal als Zuweisung bezeichnet . Der Kontext vervollständigt die obige Opposition. Zusammen bilden sie eine Form Urteil bezeichnet . ${\displaystyle \Gamma}$${\displaystyle e:\tau}$${\displaystyle \Gamma\vdash e:\tau}$

Regeln umschreiben, Konvertierung, Reduktion

Typtheorien haben eine explizite Berechnung und sind in Regeln zum Umschreiben von Begriffen kodiert . Diese werden als Umrechnungsregeln oder, wenn die Regel nur in eine Richtung geht, eine Reduktion Regel . Zum Beispiel und sind syntaktisch unterschiedliche Begriffe, aber ersteres reduziert sich auf letzteres. Diese Ermäßigung wird geschrieben . Diese Regeln stellen auch entsprechende Äquivalenzen zwischen den schriftlichen Begriffen her . ${\displaystyle 2+2}$${\displaystyle 4}$${\displaystyle 2+2\twoheadrightarrow 4}$${\displaystyle 2+2\äquivalent 4}$

Der Begriff reduziert sich auf . Da sie nicht weiter reduziert werden kann, wird sie als Normalform bezeichnet . Verschiedene Systeme des typisierten Lambda-Kalküls einschließlich des einfach typisierten Lambda-Kalküls , Jean-Yves Girards System F und Thierry Coquands Konstruktionskalkül sind stark normalisierend . In solchen Systemen impliziert eine erfolgreiche Typprüfung einen Kündigungsnachweis der Laufzeit. ${\displaystyle 2+1}$${\displaystyle 3}$${\displaystyle 3}$

Typregeln

Basierend auf den Urteilen und Äquivalenzen können Typinferenzregeln verwendet werden, um zu beschreiben, wie ein Typsystem syntaktischen Konstruktionen (Termen) einen Typ zuordnet, ähnlich wie bei der natürlichen Deduktion . Um sinnvoll zu sein, sind Konvertierungs- und Typregeln normalerweise eng miteinander verbunden, wie zB durch eine Subjektreduktionseigenschaft , die einen Teil der Solidität eines Typsystems bestimmen könnte.

Entscheidungsprobleme

Ein Typ - System ist mit den natürlich assoziiert Entscheidungsproblemen der Typprüfung , typability und Typ inhabitation .

Typprüfung

Das Entscheidungsproblem der Typprüfung (abgekürzt mit ) lautet: ${\displaystyle \Gamma \vdash e:\tau ?}$

Entscheiden Sie bei einer gegebenen Typumgebung , einem Begriff und einem Typ , ob dem Begriff der Typ in der Typumgebung zugewiesen werden kann .${\displaystyle \Gamma}$${\displaystyle e}$${\displaystyle \tau}$${\displaystyle e}$${\displaystyle \tau}$${\displaystyle \Gamma}$

Entscheidbarkeit der Typprüfung bedeutet, dass die Typsicherheit eines beliebigen Programmtextes (Quellcodes) überprüft werden kann.

Typisierbarkeit

Das Entscheidungsproblem der Typisierbarkeit (abgekürzt mit ) lautet: ${\displaystyle \exists \Gamma ,\tau .\Gamma \vdash e:\tau ?}$

Entscheiden Sie zu einem Begriff , ob es eine Typumgebung und einen Typ gibt, so dass dem Begriff der Typ in der Typumgebung zugewiesen werden kann .${\displaystyle e}$${\displaystyle \Gamma}$${\displaystyle \tau}$${\displaystyle e}$${\displaystyle \tau}$${\displaystyle \Gamma}$

Eine Variante der Typisierung ist die Typability wrt. eine Typumgebung (abgekürzt mit ), für die eine Typumgebung Teil der Eingabe ist. Enthält der angegebene Begriff keine externen Referenzen (wie freie Begriffsvariablen), dann stimmt die Typisierung mit der Typisierung bzgl. die leere Typumgebung. ${\displaystyle \exists \tau .\Gamma \vdash e:\tau ?}$

Die Typisierung ist eng mit der Typinferenz verbunden . Während die Typisierung (als Entscheidungsproblem) die Existenz eines Typs für einen gegebenen Begriff anspricht, erfordert die Typinferenz (als Berechnungsproblem) die Berechnung eines tatsächlichen Typs.

Typ Wohnen

Das Entscheidungsproblem der Typinhabitation (abgekürzt mit ) lautet: ${\displaystyle \exists e.\Gamma \vdash e:\tau ?}$

Entscheiden Sie bei einer gegebenen Typumgebung und einem Typ , ob es einen Begriff gibt, dem der Typ in der Typumgebung zugewiesen werden kann .${\displaystyle \Gamma}$${\displaystyle \tau}$${\displaystyle e}$${\displaystyle \tau}$${\displaystyle \Gamma}$

Das Paradox von Girard zeigt, dass die Typisierung stark mit der Konsistenz eines Typsystems mit der Curry-Howard-Korrespondenz zusammenhängt. Um solide zu sein, muss ein solches System unbewohnte Typen haben.

Der Gegensatz von Begriffen und Typen kann auch als Implementierung und Spezifikation angesehen werden . Durch Programmsynthese (das rechnerische Gegenstück zu) kann Typ-Inhabitation (siehe unten) verwendet werden, um (alle oder Teile davon) Programme aus einer in Form von Typinformationen gegebenen Spezifikation zu konstruieren.

Interpretationen der Typentheorie

Die Typentheorie ist eng mit vielen Feldern aktiver Forschung verbunden. Insbesondere die Curry-Howard-Korrespondenz bietet einen tiefen Isomorphismus zwischen intuitionistischer Logik, typisiertem Lambda-Kalkül und kartesischen geschlossenen Kategorien.

Intuitionistische Logik

Neben der Auffassung von Typen als Ansammlung von Werten eines Begriffs bietet die Typentheorie eine zweite Interpretation des Gegensatzes von Begriff und Typen. Typen können als Aussagen und Terme als Beweise angesehen werden . In dieser Lesart einer Typisierung wird ein Funktionstyp als Implikation , dh als Satz, der aus folgt, betrachtet . ${\displaystyle\alpha\rightarrow\beta}$${\displaystyle \beta}$${\displaystyle\alpha}$

Kategorientheorie

Die interne Sprache der kartesischen geschlossenen Kategorie ist der einfach typisierte Lambda-Kalkül . Diese Ansicht kann auf andere typisierte Lambda-Kalküle erweitert werden. Bestimmte kartesische geschlossene Kategorien, die Topoi, wurden als allgemeiner Rahmen für die Mathematik anstelle der traditionellen Mengenlehre vorgeschlagen.

Unterschied zur Mengenlehre

Es gibt viele verschiedene Mengentheorien und viele verschiedene Systeme der Typentheorie, daher handelt es sich im Folgenden um Verallgemeinerungen.

• Die Mengenlehre baut auf der Logik auf. Es erfordert ein separates System wie die Prädikatenlogik darunter. In der Typentheorie können Konzepte wie "und" und "oder" als Typen in der Typentheorie selbst kodiert werden.
• In der Mengenlehre ist ein Element nicht auf eine Menge beschränkt. In der Typentheorie gehören Begriffe (im Allgemeinen) nur zu einem Typ. (Wo eine Teilmenge verwendet würde, verwendet die Typtheorie tendenziell eine Prädikatsfunktion , die wahr zurückgibt, wenn der Term in der Teilmenge enthalten ist, und falsch zurückgibt, wenn der Wert nicht vorhanden ist. Die Vereinigung zweier Typen kann als ein neuer Typ definiert werden, der als Summe bezeichnet wird type , der neue Begriffe enthält.)
• Die Mengenlehre kodiert Zahlen normalerweise als Mengen. (0 ist die leere Menge, 1 ist eine Menge, die die leere Menge enthält usw. Siehe Mengentheoretische Definition natürlicher Zahlen .) Die Typentheorie kann Zahlen als Funktionen mit Church-Codierung oder natürlicher als induktive Typen kodieren . Induktive Typen erzeugen neue Konstanten für die Nachfolgefunktion und die Null, die Peanos Axiomen sehr ähnlich sind .
• Die Typentheorie hat durch die BHK-Interpretation eine einfache Verbindung zur konstruktiven Mathematik . Es kann durch den Curry-Howard-Isomorphismus mit der Logik verbunden werden . Und einige Typentheorien sind eng mit der Kategorietheorie verbunden .

Optionale Funktionen

Abhängige Typen

Ein abhängiger Typ ist ein Typ, der von einem Begriff oder einem anderen Typ abhängt. Daher kann der von einer Funktion zurückgegebene Typ vom Argument der Funktion abhängen.

Zum Beispiel kann eine Liste von s der Länge 4 einen anderen Typ haben als eine Liste von s der Länge 5. In einer Typtheorie mit abhängigen Typen ist es möglich, eine Funktion zu definieren, die einen Parameter "n" nimmt und eine Liste zurückgibt mit "n" Nullen. Der Aufruf der Funktion mit 4 würde einen Term mit einem anderen Typ erzeugen, als wenn die Funktion mit 5 aufgerufen würde. ${\displaystyle \mathrm {nat}}$${\displaystyle \mathrm {nat}}$

Ein anderes Beispiel ist der Typ, der aus den Beweisen besteht, dass der Argumentterm eine bestimmte Eigenschaft hat, wie der Typterm, zB eine gegebene natürliche Zahl, ist eine Primzahl. Siehe Curry-Howard-Korrespondenz . ${\displaystyle \mathrm {nat}}$

Abhängige Typen spielen eine zentrale Rolle in der intuitionistischen Typentheorie und im Design funktionaler Programmiersprachen wie Idris , ATS , Agda und Epigram .

Gleichheitstypen

Viele Systeme der Typtheorie haben einen Typ, der die Gleichheit von Typen und Begriffen repräsentiert. Dieser Typ unterscheidet sich von der Konvertibilität und wird oft als Satzgleichheit bezeichnet .

In der intuitionistischen Typentheorie wird der Gleichheitstyp (auch Identitätstyp genannt) als Identität bezeichnet. Es gibt einen Typ, wenn ein Typ ist und und beide Begriffe des Typs sind . Ein Begriff vom Typ wird als Bedeutung interpretiert, die gleich ist . ${\displaystyle I}$${\displaystyle I\ A\ a\ b}$${\displaystyle A}$${\displaystyle a}$${\displaystyle b}$${\displaystyle A}$${\displaystyle I\ A\ a\ b}$${\displaystyle a}$${\displaystyle b}$

In der Praxis ist es möglich, einen Typ zu erstellen, aber es wird keinen Begriff dieses Typs geben. In der intuitionistischen Typentheorie beginnen neue Gleichheitsbegriffe mit der Reflexivität. Wenn ein Begriff vom Typ ist , dann existiert ein Begriff vom Typ . Kompliziertere Gleichheiten können geschaffen werden, indem man einen reflexiven Term erzeugt und dann auf einer Seite reduziert. Wenn also ein Begriff vom Typ ist , dann gibt es einen Begriff vom Typ und durch Reduktion einen Begriff vom Typ erzeugen . Somit bedeutet in diesem System der Gleichheitstyp, dass zwei Werte des gleichen Typs durch Reduktionen konvertierbar sind. ${\displaystyle I\ \mathrm {nat} \ 3\ 4}$${\displaystyle 3}$${\displaystyle \mathrm {nat}}$${\displaystyle I\ \mathrm {nat} \ 3\ 3}$${\displaystyle 2+1}$${\displaystyle \mathrm {nat}}$${\displaystyle I\ \mathrm {nat} \ (2+1)\ (2+1)}$${\displaystyle I\ \mathrm {nat} \ (2+1)\ 3}$

Es ist wichtig, einen Gleichheitstyp zu haben, da er innerhalb des Systems manipuliert werden kann. Es gibt normalerweise kein Urteil, um zu sagen, dass zwei Begriffe nicht gleich sind; stattdessen bilden wir wie in der Brouwer-Heyting-Kolmogorov-Interpretation auf ab , wobei der unterste Typ keine Werte hat. Es gibt einen Begriff vom Typ , aber keinen vom Typ . ${\displaystyle \neg (a=b)}$${\displaystyle (a=b)\to \bot}$${\displaystyle \bot}$${\displaystyle (I\ \mathrm {nat} \ 3\ 4)\to \bot}$${\displaystyle (I\ \mathrm {nat} \ 3\ 3)\to \bot}$

Die Homotopietypentheorie unterscheidet sich von der intuitionistischen Typentheorie hauptsächlich durch die Behandlung des Gleichheitstyps.

Induktive Typen

Ein System der Typentheorie erfordert einige grundlegende Begriffe und Typen, mit denen es operieren kann. Einige Systeme bauen sie aus Funktionen mit Church-Codierung auf . Andere Systeme haben induktive Typen : eine Menge von Basistypen und eine Menge von Typkonstruktoren , die Typen mit wohlerzogenen Eigenschaften erzeugen. Zum Beispiel bestimmte rekursive Funktionen auf induktiven Typen genannt werden garantiert zu beenden.

Koinduktive Typen sind unendliche Datentypen, die erzeugt werden, indem eine Funktion angegeben wird, die das/die nächste(n) Element(e) generiert. Siehe Koinduktion und Kernkursion .

Induktion-Induktion ist ein Merkmal zum Deklarieren eines induktiven Typs und einer Typenfamilie, die vom induktiven Typ abhängt.

Die Induktionsrekursion ermöglicht eine breitere Palette von Typen mit gutem Verhalten, wodurch der Typ und die rekursiven Funktionen gleichzeitig definiert werden können.

Universumstypen

Typen wurden erstellt, um Paradoxien wie Russells Paradox zu verhindern . Die Motive, die zu diesen Paradoxien führen – die Möglichkeit, über alle Arten Dinge sagen zu können – existieren jedoch immer noch. Viele Typentheorien haben also einen "Universumstyp", der alle anderen Typen enthält (und nicht sich selbst).

In Systemen, in denen Sie möglicherweise etwas zu Universumstypen sagen möchten, gibt es eine Hierarchie von Universumstypen, von denen jeder den darunter liegenden in der Hierarchie enthält. Die Hierarchie ist als unendlich definiert, aber Anweisungen dürfen sich nur auf eine endliche Anzahl von Universumsebenen beziehen.

Typuniversen sind in der Typentheorie besonders knifflig. Der ursprüngliche Vorschlag der intuitionistischen Typentheorie litt unter dem Paradox von Girard .

Computerkomponente

Viele Systeme der Typentheorie, wie der einfach typisierte Lambda-Kalkül , die intuitive Typentheorie und die Konstruktionsrechnung , sind ebenfalls Programmiersprachen. Das heißt, sie haben eine "rechnerische Komponente". Die Berechnung ist die Reduktion von Begriffen der Sprache unter Verwendung von Umschreibungsregeln .

Ein System der Typtheorie, das eine gut verhaltene Rechenkomponente hat, hat durch die BHK-Interpretation auch eine einfache Verbindung zur konstruktiven Mathematik .

Nicht-konstruktive Mathematik in diesen Systemen ist durch Hinzufügen von Operatoren zu Fortsetzungen wie Aufruf mit aktueller Fortsetzung möglich . Diese Operatoren neigen jedoch dazu, wünschenswerte Eigenschaften wie Kanonizität und Parametrizität zu brechen .

Typtheorien

Haupt

• Einfach eingegebener Lambda-Kalkül, der eine Logik höherer Ordnung ist ;
• intuitionistische Typentheorie ;
• System F ;
• LF wird oft verwendet, um andere Typentheorien zu definieren;
• Konstruktionsrechnung und ihre Ableitungen.

Unerheblich

• Automat ;
• ST-Typ-Theorie ;
• UTT (Luos vereinheitlichte Theorie der abhängigen Typen)
• einige Formen der kombinatorischen Logik ;
• andere im Lambda-Würfel definiert ;
• andere unter dem Namen typisierte Lambda-Kalküle ;
• andere unter dem Namen reines Typsystem .

Aktiv

• Die Homotopietyptheorie wird erforscht.

Praktische Wirkung

Programmiersprachen

Es gibt umfangreiche Überschneidungen und Interaktionen zwischen den Gebieten der Typentheorie und der Typensysteme. Typsysteme sind eine Funktion der Programmiersprache, die entwickelt wurde, um Fehler zu identifizieren. Jede statische Programmanalyse , wie beispielsweise die Typprüfalgorithmen in der semantischen Analysephase des Compilers , hat eine Verbindung zur Typtheorie.

Ein Paradebeispiel ist Agda , eine Programmiersprache, die UTT (Luos Unified Theory of Dependent Types) für ihr Typsystem verwendet. Die Programmiersprache ML wurde zur Manipulation von Typtheorien entwickelt (siehe LCF ) und ihr eigenes Typsystem wurde stark davon beeinflusst.

Mathematische Grundlagen

Der erste Computerbeweisassistent namens Automath verwendete die Typentheorie, um Mathematik auf einem Computer zu kodieren. Martin-Löf hat speziell die intuitionistische Typentheorie entwickelt , um die gesamte Mathematik zu kodieren , um als neue Grundlage für die Mathematik zu dienen. Es wird laufend an mathematischen Grundlagen mit Hilfe der Homotopie-Typentheorie geforscht .

Mathematiker, die in der Kategorientheorie arbeiten, hatten bereits Schwierigkeiten, mit der allgemein akzeptierten Grundlage der Zermelo-Fraenkel-Mengentheorie zu arbeiten . Dies führte zu Vorschlägen wie Lawveres Elementary Theory of the Category of Sets (ETCS). Die Homotopie-Typentheorie setzt sich in dieser Linie mit der Typentheorie fort. Forscher untersuchen Verbindungen zwischen abhängigen Typen (insbesondere dem Identitätstyp) und algebraischer Topologie (insbesondere Homotopie ).

Nachweisassistenten

Ein Großteil der aktuellen Forschung zur Typtheorie wird von Beweisprüfern , interaktiven Beweisassistenten und automatisierten Theorembeweisern angetrieben . Die meisten dieser Systeme verwenden eine Typtheorie als mathematische Grundlage für die Kodierung von Beweisen, was angesichts der engen Verbindung zwischen Typtheorie und Programmiersprachen nicht verwunderlich ist:

• LF wird von Twelf verwendet , um oft andere Typentheorien zu definieren;
• viele Typentheorien, die unter die Logik höherer Ordnung fallen, werden von der HOL-Familie von Beweisern und PVS verwendet ;
• Computational Type Theory wird von NuPRL verwendet ;
• Konstruktionsrechnung und ihre Ableitungen werden von Coq , Matita und Lean verwendet ;
• UTT (Luos vereinheitlichte Theorie der abhängigen Typen) wird von Agda verwendet, die sowohl eine Programmiersprache als auch ein Beweisassistent ist

Viele Typentheorien werden von LEGO und Isabelle unterstützt . Isabelle unterstützt neben Typentheorien auch Stiftungen, wie z. B. ZFC . Mizar ist ein Beispiel für ein Beweissystem, das nur die Mengenlehre unterstützt.

Linguistik

Typentheorie ist auch weit verbreitet in formalen Theorien der Semantik der natürlichen Sprachen , vor allem Montague Grammatik und seine Nachkommen. Insbesondere kategoriale Grammatiken und Vorgruppengrammatiken verwenden häufig Typkonstruktoren , um die Typen ( Substantiv , Verb usw.) von Wörtern zu definieren.

Die gebräuchlichste Konstruktion nimmt die Grundtypen und für Individuen bzw. Wahrheitswerte und definiert die Menge der Typen rekursiv wie folgt: ${\displaystyle e}$${\displaystyle t}$

• wenn und Typen sind, dann auch ;${\displaystyle a}$${\displaystyle b}$${\displaystyle\langle a,b\rangle}$
• nichts außer den Grundtypen, und was sich aus ihnen mit Hilfe der vorherigen Klausel konstruieren lässt, sind Typen.

Ein komplexer Typ ist der Typ von Funktionen von Entitäten des Typs zu Entitäten des Typs . So hat man Typen wie die als Elemente der Menge von Funktionen von Entitäten zu Wahrheitswerten interpretiert werden, dh Indikatorfunktionen von Mengen von Entitäten. Ein Typausdruck ist eine Funktion von Mengen von Entitäten zu Wahrheitswerten, dh eine (Indikatorfunktion einer) Menge von Mengen. Dieser letztere Typ wird standardmäßig als der Typ der Quantoren natürlicher Sprache angesehen , wie alle oder niemand ( Montague 1973, Barwise und Cooper 1981). ${\displaystyle\langle a,b\rangle}$${\displaystyle a}$${\displaystyle b}$${\displaystyle \langle e,t\rangle}$${\displaystyle \langle \langle e,t\rangle,t\rangle}$

Sozialwissenschaften

Gregory Bateson führte eine Theorie der logischen Typen in die Sozialwissenschaften ein; seine Vorstellungen von Double Bind und Logical Levels basieren auf Russells Typentheorie.

Bezug zur Kategorientheorie

Obwohl die anfängliche Motivation für die Kategorientheorie weit vom Fundamentalismus entfernt war, stellte sich heraus, dass die beiden Bereiche tiefe Verbindungen haben. Wie John Lane Bell schreibt: "Tatsächlich können Kategorien selbst als Typentheorien einer bestimmten Art angesehen werden; diese Tatsache allein weist darauf hin, dass die Typentheorie viel enger mit der Kategorientheorie verwandt ist als mit der Mengentheorie." Kurz gesagt kann eine Kategorie als Typentheorie betrachtet werden, indem man ihre Objekte als Typen (oder Sortierungen) betrachtet, dh "Grob gesprochen kann man sich eine Kategorie als eine ihrer Syntax entzogene Typentheorie vorstellen." Auf diese Weise ergeben sich eine Reihe von signifikanten Ergebnissen:

• kartesische geschlossene Kategorien entsprechen dem typisierten λ-Kalkül ( Lambek , 1970);
• C-Monoide (Kategorien mit Produkten und Exponentialfunktionen und einem nicht-terminalen Objekt) entsprechen dem untypisierten λ-Kalkül ( um 1980 unabhängig von Lambek und Dana Scott beobachtet );
• lokal kartesische geschlossene Kategorien entsprechen Martin-Löf-Typ-Theorien (Seely, 1984).

Das Wechselspiel, die so genannte kategoriale Logik , ist seither Gegenstand aktiver Forschung; siehe zum Beispiel die Monographie von Jacobs (1999).

Siehe auch

• Datentyp für konkrete Datentypen in der Programmierung
• Domänentheorie
• Typ (Modelltheorie)
• Geben System für eine praktischere Diskussion Typsysteme für Programmiersprachen
• Univalente Grundlagen

Anmerkungen

Verweise

Weiterlesen

Externe Links

• Robert L. Constable (Hrsg.). "Computertyptheorie" . Scholarpedia .
• The TYPES Forum — seit 1987 ein moderiertes E-Mail-Forum mit Schwerpunkt auf der Typentheorie in der Informatik.
• Das Nuprl-Buch : " Einführung in die Typentheorie. "
• Typen Projektmitschriften der Summer Schools 2005–2008
  • Die Sommerschule 2005 hat Einführungsvorlesungen
• Typtheorie in nLab , das Artikel zu vielen verwandten Themen enthält.
• Oregon Programming Languages ​​Summer School , viele Vorlesungen und einige Notizen.
  • Sommer 2015 Typen, Logik, Semantik und Verifikation