Gibt es eine typisierte Lambda-Rechnung, die konsistent und vollständig ist?

Gibt es eine typisierte Lambda-Rechnung, in der die entsprechende Logik unter der Curry-Howard-Korrespondenz konsistent ist und in der es typisierbare Lambda-Ausdrücke für jede berechenbare Funktion gibt?

Dies ist zugegebenermaßen eine ungenaue Frage, da eine genaue Definition der "typisierten Lambda-Rechnung" fehlt. Ich frage mich im Grunde, ob es entweder (a) bekannte Beispiele dafür oder (b) bekannte Unmöglichkeitsbeweise für etwas in diesem Bereich gibt.

Edit: @cody gibt eine genaue Version dieser Frage in seiner Antwort unten an: Gibt es ein logisches reines Typensystem (LPTS), das konsistent und vollständig ist (in einem unten definierten Sinne)?

In Ordnung, ich werde es kurz ansprechen: Im Allgemeinen gilt für ein gegebenes Typensystem Folgendes:$T$

Wenn alle gut Typ Begriffe im Kalkül - Normalisieren sind, dann T ist konsistent , wenn sie als Logik betrachtet.$T$$T$

Der Beweis erfolgt im Allgemeinen unter der Annahme, dass Sie einen Term vom Typ F a l s e haben , indem Sie die Subjektreduktion verwenden, um eine normale Form zu erhalten, und dann durch Induktion über die Struktur eines solchen Terms fortfahren, um einen Widerspruch zu erhalten.$\mathrm{absurd}$$\mathrm{False}$

Es ist natürlich zu fragen, ob das Gegenteil zutrifft, dh

Für jede Art System , wenn T ist logisch konsistent , dann jeder gut getippt Begriff in T ist Normalisieren.$T$$T$$T$

Das Problem dabei ist, dass es keinen wirklich allgemeinsten Begriff von "Typensystem" gibt und noch weniger Übereinstimmung über die Bedeutung der logischen Konsistenz für solche Systeme besteht. Wir können dies jedoch empirisch überprüfen

Für die meisten bekannten Typsysteme, die eine logische Interpretation haben, gilt in der Tat das Gegenteil.

Wie ist dies mit der Vollständigkeit von Turing verbunden? Nun, zum einen zeigt Andrejs Argument , dass eine der folgenden Aussagen zutreffen muss , wenn die Typprüfung entscheidend ist :

1. Die Menge aller gut getippten Programme stimmt nicht vollständig.
2. Es gibt ein nicht abschließendes, gut typisiertes Programm.

Dies deutet darauf hin, dass:

Typsysteme, die eine logische Interpretation haben und konsistent und rekursiv aufzählbar sind, sind es nicht Turing abgeschlossen.

Um einen tatsächlichen Satz anstelle eines Vorschlags zu geben, müssen Typensysteme und logische Interpretationen mathematisch präzise formuliert werden.

Nun kommen zwei Bemerkungen in den Sinn:

1. Es gibt ein unentscheidbares Typsystem, das Schnittpunkttypsystem, das eine logische Interpretation hat und jedes normalisierende Term darstellen kann. Wie Sie bemerken, ist dies nicht ganz das Gleiche wie "Turing Complete", da der Typ einer Gesamtfunktion möglicherweise aktualisiert (genauer definiert) werden muss, bevor er auf das gewünschte Argument angewendet wird. Der Kalkül ist ein "Curry-Stil" -Kalkül und ist gleich STLC + Γ ⊢ $\lambda$ und ΓΓM:τ∩

   $$\frac{\Gamma\vdash M:\tau\quad \Gamma\vdash M:\sigma}{\Gamma\vdash M:\tau\cap\sigma}$$ Es ist klar, dass die "Interpretation"∩= $$\frac{\Gamma\vdash M:\tau\cap\sigma}{\Gamma\vdash M:\tau}\quad \frac{\Gamma\vdash M:\tau\cap\sigma}{\Gamma\vdash M:\sigma}$$ $\cap=\wedge$ zu einer konsistenten logischen Interpretation führt.

2. Es gibt eine Klasse von Typsystemen, die Pure Type Systems , in denen eine solche Frage präzisiert werden könnte. In diesem Rahmen ist die logische Interpretation jedoch weniger klar. Man könnte versucht sein zu sagen: "Ein PTS ist konsistent, wenn es einen unbewohnten Typ hat". Dies funktioniert jedoch nicht, da Typen möglicherweise in verschiedenen "Universen" leben, in denen einige konsistent sind und andere nicht. Coquand und Herbelin definieren einen Begriff von logischen reinen Typensystemen , in denen die Frage sinnvoll ist und zeigen

   Jedes inkonsistente, nicht abhängige LPTS hat einen Schleifen-Kombinator (und auch Turing Complete).

   Welches beantwortet die Frage in eine Richtung (inkonsistent TC) in diesem Fall. Soweit ich weiß, ist die Frage nach dem allgemeinen LPTS noch offen und ziemlich schwierig.$\Rightarrow$

Bearbeiten: Die Umkehrung des Coquand-Herbelin-Ergebnisses ist nicht so einfach, wie ich dachte! Folgendes habe ich mir bisher ausgedacht.

Ein logisches reines Typensystem ist ein PTS mit (mindestens) den Sortierungen und T y p e , (mindestens) dem Axiom P r o p : T y p e und (mindestens) der Regel ( P r o p , P r o p , P r o p ) , mit der weiteren Voraussetzung, dass es keine Art von P r o p gibt .$\mathrm{Prop}$$\mathrm{Type}$$\mathrm{Prop}:\mathrm{Type}$$(\mathrm{Prop},\mathrm{Prop},\mathrm{Prop})$$\mathrm{Prop}$

Jetzt gehe ich von einer bestimmten Aussage zur Vollständigkeit der Prüfung aus: Repariere ein LPTS $L$ and let $\Gamma$ be the context

$L$ is Turing Complete iff for every total computable function $f:\mathbb{N}\rightarrow\mathbb{N}$ there is a term $t_f$ such that

Now Andrej's diagonalization argument shows that there are non-terminating $t$ of type $\mathrm{nat}$.

Now it seems like we are half-way there! Given a non terminating term $\Gamma \vdash \mathrm{loop}:\mathrm{nat}$, we want to replace occurrences of $\mathrm{nat}$ by some generic type $A$ and get rid of $0$ and $S$ in $\Gamma$, and we will have our inconsistency ($A$ is inhabited in the context $A:\mathrm{Prop}$)!

Unfortunately this is where I get stuck, since it is easy to replace $S$ by the identity, but the $0$ is much harder to get rid of. Ideally we would like to use some Kleene recursion theorem, but I haven't figured this out yet.

Hier ist eine Antwort auf eine Variante von @codys Präzisierung meiner Frage. Es gibt eine konsistente LPTS, die in etwa @ cody's Sinne vollständig ist, wenn wir die Einführung zusätzlicher Axiome und zulassen$\beta$-Reduktionsregeln. Das System ist also streng genommen kein LPTS; es ist nur so etwas wie eins.

Betrachten Sie die Konstruktionsrechnung (oder Ihr Lieblingsmitglied der $\lambda$-cube). This is an LPTS, but we're going to add extra stuff which makes it not an LPTS. Choose constant symbols $\text{nat}, 0, S$, and add the axioms:

Index the Turing machine programs by natural numbers, and for each natural number $e$, choose a constant symbol $f_e$, add the axiom $f_e : \text{nat} \to \text{nat}$, and for all $e,x \in \mathbb{N}$, add the $\beta$-reduction rule

where as usual $\Phi_e(x)$ is the output of the $e$th Turing machine program on $x$. If $\Phi_e(x)$ diverges then this rule doesn't do anything. Note that by adding these axioms and rules the system's theorems remain recursively enumerable, though its set of $\beta$-reduction rules is no longer decidable, but merely recursively enumerable. I believe we could easily keep the set of $\beta$-reduction rules decidable by spelling out explicitly the details of a model of computation in the syntax and rules of the system.

Now, this theory is clearly Turing complete in roughly @cody's sense, just by brute force; but the claim is that it's also consistent. Let's construct a model of it.

Let $U_1 \in U_2 \in U_3$ be three sets, such that:

• $\emptyset, \mathbb{N}, 0, S \in U_1$ (where $S$ is the successor function).
• Each set is transitive; if $a \in b \in U_i$, then $a \in U_i$.
• Each set is closed under the formation of function spaces; i.e., if $A, B \in U_i$, then $B^A \in U_i$.
• Each set is closed under the formation of dependent products; i.e., if $A \in U_i$ and $f : A \to U_i$, then $\prod_{a \in A} f(a) \in U_i$.

The existence of such sets follows, for example, from ZFC plus the axiom that every cardinal is bounded by an inaccessible cardinal; we can take each set $U_i$ to be a Grothendieck universe.

We define an "interpretation" to be a mapping $v$ from the set of variable names to elements of $U_2$. Given an interpretation $v$, we can define an interpretation $I_v$ of terms of the system in the evident way:

• $I_v(x) = v(x)$, for $x$ a variable name.
• $I_v(\ast) = U_1, I_v(\Box) = U_2$.
• $I_v(\text{nat}) = \mathbb{N}, I_v(0) = 0, I_v(S) = S$.
• $I_v(f_e) = \Phi_e$, i.e., the function $\mathbb{N} \to \mathbb{N}$ defined by the $e$th Turing program.
• $I_v(AB) = I_v(A)(I_v(B))$, if $I_v(A)$ is a function with $I_v(B)$ in its domain, or $I_v(AB) = 0$ otherwise (just an arbitrary choice).
• $I_v(\lambda x : A. B)$ is the function which maps an element $a \in I_v(A)$ to $I_{v[x:=a]}(B)$.
• $I_v(\Pi x : A. B) = \prod_{a \in I_v(A)} I_{v[x:=a]}(B)$.

We have that for all terms $A$, $I_v(A) \in U_3$. Now we say that an interpretation $v$ satisfies $A : B$, written $v \models A : B$, if $I_v(A) \in I_v(B)$. We say that $\Gamma \models A : B$ if for all interpretations $v$, if $v \models x : C$ for all $(x : C) \in \Gamma$, then $v \models A : B$.

It is straightforward to check that if $\Gamma \vdash A : B$, then $\Gamma \models A : B$, so this is a model of the system. But, for any variables $x,y$, it is not the case that $y : \ast \models x : y$, because we can interpret $y$ by $\emptyset$, so the system is consistent.

Now, this is an answer to my original question, in the sense that this is something that it's reasonable to call a typed lambda calulus, which is consistent and Turing complete. However, it's not an answer to @cody's question, because this is not an LPTS, because of the addition of extra axioms and $\beta$-reduction rules. I imagine that the answer to @cody's question is much harder.