In vielen Lehrbüchern ist es einfach, die Beweise für die Reduzierung des Subjekts und die starke Normalisierung für System F zu lesen. Manchmal gibt es auch Definitionen von System F mit Paaren, wobei (t, r) ein Begriff ist, nicht nur eine Codierung. Die Frage ist, was wäre die Referenz für dieses...
Ich versuche, lineare Logik zu verstehen, um lineare Typsysteme besser zu verstehen. Wenn ich jedoch die Regeln lese, bekomme ich keine Intuition dahinter, wie ich es in der Modallogik getan habe - □A◻A\Box A bedeutet, dass AAA erforderlich ist, wie in Kripke-Frames. AAA ist für jede erreichbare...
Ich besitze ein Buch, das, inspiriert von Russells Principia Mathematica (PM) und dem logischen Positivismus, versucht, einen bestimmten Bereich zu formalisieren, indem es Axiome bestimmt und daraus Theoreme ableitet. Kurz gesagt, es wird versucht, für seine Domäne das zu tun, was PM für die...
Soweit ich weiß, basieren Datentypen in der Informatik aufgrund von Russells Paradoxon nicht auf der Mengenlehre, aber wie in realen Programmiersprachen können wir so komplexe Datentypen wie "Menge, die sich nicht selbst enthält" nicht ausdrücken, oder? Angenommen, in der Praxis ist der Typ eine...
Die Martin-Löf-Typentheorie verwendet W-Typen, um induktive Strukturen wie ganze Zahlen, Listen usw. zu definieren. Die Berechnung induktiver Konstruktionen verwendet sie jedoch nicht auf die gleiche Weise. Induktive Typen scheinen eher Axiomschemata zu sein. Sind diese beiden Ansätze gleichwertig...
Dies kann eine sehr einfache Frage sein. Aber was ist der Unterschied zwischen Typen und Sorten? Mein derzeitiges Verständnis ist, dass Sie eine Typentheorie mit Typregeln haben, die den Begriff einer gut typisierten Aussage vermitteln, aber Sortierungen grundlegender sind, Symbole in verschiedene...
Auf meiner Suche nach Forschungsarbeiten über Typensysteme für imperative Sprachen finde ich nur Lösungen für eine Sprache mit veränderlichen Referenzen, aber ohne echte imperative Kontrollstrukturen wie zusammengesetzte Operatoren, Schleifen oder Bedingungen. Es ist also nicht klar, wie eine...
Die konstruktive Typentheorie mit ihrer Grundinterpretation unter der Curry-Howard-Korrespondenz besteht nur aus insgesamt berechenbaren Funktionen. In der Literatur wurde über die Verwendung der "Computertypentheorie" zur Darstellung der Nichtbeendigung in funktionalen Programmen gesprochen, doch...
Eines der wenigen Dinge, die ich an Okasakis Buch über rein funktionale Datenstrukturen nicht mag, ist, dass sein Code mit einem erschöpfenden Mustervergleich übersät ist. Als Beispiel gebe ich seine Implementierung von Echtzeitwarteschlangen an (überarbeitet, um unnötige Suspensionen zu...
Ich bin in einer Situation, in der ich zeigen muss, dass Typchecking für einen abhängig typisierten Kalkül, an dem ich arbeite, entscheidend ist. Bisher konnte ich beweisen, dass sich das System stark normalisiert und somit die definitive Gleichheit entscheidbar ist. In vielen Referenzen, die ich...
Ich habe eine Sprache, in der Typen standardmäßig deaktiviert sind, wobei die Typinferenz auf Hindley-Milner basiert. Ich möchte einen höherrangigen Polymorphismus hinzufügen, hauptsächlich für die Arbeit mit existenziellen Typen. Ich glaube, ich verstehe, wie man diese Typen überprüft , bin mir...
Die meisten Beweisassistenten haben eine Formalisierung des Konzepts der "endlichen Menge". Diese Formalisierungen unterscheiden sich jedoch stark (obwohl man hofft, dass sie alle im Wesentlichen gleichwertig sind!). Was ich derzeit nicht verstehe, ist der Designraum und die Vor- und Nachteile...
Ich habe die folgende typisierte Theorie |- 1_X : X -> X f : A -> B, g : B -> C |- compose(g,f) : A -> C F, f : A -> B |- apply(F,f) : F(A) -> F(B) mit Gleichungen für alle Begriffe: f : A -> B, g : B -> C, h : C -> D |- compose(h,compose(f,g)) = compose(compose(h,f),g) f...
Wir wissen, dass die Beta-Gleichheit von einfach getippten Lambda-Begriffen entscheidend ist. gegebenem M, N: σ → τ entscheidbar, ob für alle X: σ MX
Für einen Korrektheitsnachweis suche ich nach einem brauchbaren Begriff der Programmäquivalenz für Barendregts reine Typsysteme (PTS); Fehlt das, für genügend spezifische Typsysteme. Mein Ziel ist es einfach, den Begriff zu verwenden und ihn nicht um seiner selbst willen zu untersuchen.≅≅\cong...
Möglicherweise liegt die Hauptursache für Leistungsprobleme in Haskell darin, dass ein Programm versehentlich einen Teil unbegrenzter Tiefe aufbaut. Dies führt sowohl zu einem Speicherverlust als auch zu einem möglichen Stapelüberlauf bei der Auswertung. Das klassische Beispiel ist die Definition...
Es ist eine ziemlich bekannte Tatsache, dass das Ableiten eines Widerspruchs aus einer Ungleichheit (zum Beispiel ) in der Martin-Loef-Typentheorie ein Universum erfordert.( 0 = 1 ) → ⊥(0=1)→⊥(0=1) \to \bot Der Beweis ist auch ziemlich einfach - in Abwesenheit von Universen können wir die...
In den erweiterten Themen in Typen und Programmiersprachen wird im Kapitel über substrukturelle Typsysteme erwähnt, dass ein "sorgfältig ausgearbeiteter" affiner Lambda-Kalkül mit einem Rekursionskombinator für Listen nur Begriffe eingeben kann, die eine polynomielle Laufzeit haben (dies ist nicht...
Angenommen, ich arbeite in der Homotopietypentheorie und meine einzigen Studienobjekte sind konventionelle Kategorien. Äquivalenzen werden hier durch die Funktoren und , die Äquivalenzen der Kategorien liefern . Es gibt natürliche Isomorphismen und so dass dieser Funktor und "inverse" Funktor...
Ich frage mich, ob mir jemand die Intuition geben kann, warum die strikte Positivität induktiver Datentypen eine starke Normalisierung garantiert. Um es klar zu sagen, ich sehe, wie negative Vorkommen zu Divergenz führen, dh indem ich definiere: data X where Intro : (X->X) -> X wir können...