Ackerman-Hierarchie für primitive Rekursion höherer Ordnung in System T.

Gödel definiert in seinem System T die primitive Rekursion über höhere Typen. Ich fand Notizen von Girard, in denen er die Implementierung von System T zusätzlich zu einfach eingegebenem Lambda-Kalkül erklärt. Auf Seite 50 erwähnt er, dass wir mit dem System mehr Ausdruckskraft gewinnen, sobald wir mehr Typen im Recursor verwenden.

Ich verstehe nicht, wie genau das passiert. Ist es möglich, eine Art Ackermann-Hierarchie mit der primitiven Rekursion höherer Ordnung zu entwickeln, dh eine Hierarchie von immer schneller wachsenden Funktionen, bei der jede Funktion in System T ausgedrückt werden kann, die Diagonale jedoch nicht? Ich denke schon, aber die Konstruktion scheint mir nicht offensichtlich zu sein und ich wäre interessiert zu sehen, wie man sie konstruieren oder Hinweise auf Literatur erhalten würde.

Ich bin nach etwas Konkretem. Mir ist das allgemeine diagonale Argument bekannt, das die Existenz einer Funktion nicht in T beweist, aber ich würde gerne sehen, wie man wirklich "in der Typhierarchie aufsteigen" würde.

computability lambda-calculus recursion type-theory Gilles 'SO - hör auf böse zu sein'
quelle

Das ist eine schöne Frage. Ich wette, die Hierarchie folgt dem Rang des Typs, bei dem die Rekursion stattfindet. Es lohnt sich fast zu schreiben. Ich werde hierher zurückkommen, wenn ich die Zeit dazu habe.

Andrej Bauer

@AndrejBauer Ich habe darüber nachgedacht und ich würde vermuten, dass man neue Iteratoren mit höheren Ebenen in der Typhierarchie erstellen und eine schnell wachsende Hierarchie unter implementieren könnte

f_{ϵ_{0}}

$f_{\epsilon_0}$ . Möglicherweise entsprechen die Typebenen (mit einem gewissen Versatz) der Turmhöhe der Exponenten

ω^{ω^{. . .}}

$\omega^{\omega^{...}}$ auf der Hierarchie, aber ich konnte keinen Beweis ziehen (..doch).

Wie stellen Sie sich übrigens die nächste Rekursionsstufe nach der primitiven Rekursion vor? Wenn es sich um einen höheren Typ handelt, würden Sie dann eine allgemeine Rekursion (so dass wir keine Kündigung erhalten) oder eine Art Rekursion, bei der die Dinge immer noch enden (in welchem Fall, was wäre das)?

Andrej Bauer

@AndrejBauer Ich glaube, dies könnte angegangen werden, um Iteratoren zu definieren. (Ich verwende zahlentheoretische Funktionen anstelle von Lambda-Kalkül.) Zum Beispiel

I (f, 0) = f (1)

$I(f,0)=f(1)$ ,

I (f, n + 1) = f (I (f, n))

$I(f,n+1)=f(I(f,n))$ und definieren

g (0) = S

$g(0)=S$ ,

g (n) = I (g (n - 1))

$g(n)=I(g(n-1))$ (S ist Nachfolger) wo

g : N \times N^{N} \to N^{N}

$g:\mathbb{N}\times \mathbb{N}^\mathbb{N}\to\mathbb{N}^\mathbb{N}$ ,

f : N \to N

$f:\mathbb{N}\to\mathbb{N}$ . Jetzt

h (n) = g (n) (n)

$h(n)=g(n)(n)$ sollte vergleichbar sein mit

f_{ω}

$f_\omega$ . Anreise nach

f_{ω^{n}}

$f_{\omega^n}$ zum

n \in N

$n\in\mathbb{N}$ scheint machbar, aber

f_{ω^{ω}}

$f_{\omega^\omega}$ scheint herausfordernd. Nach dem Erreichen von

f_{ω^{ω}}

$f_{\omega^\omega}$ Ich würde erwarten, dass sich die Dinge klären.

Ihre Beispiele

I

$I$ und

g

$g$ befinden sich noch im System T-Fragment.

Andrej Bauer

Antworten:

(Dies ist eine sehr teilweise Antwort, die nur den ersten Punkt und nicht die Hauptfrage zur Hierarchie anspricht.)

Ich habe keinen Beweis, auf den ich Sie hinweisen könnte, aber die Idee ist, dass ein einziger Rekorder erster Ordnung über Naturtöne wie

\begin{array}{l} r e c : (n a t \to n a t) \to n a t \to n a t \to n a t \\ r e c f z n = f (f (\dots f (z))) (n times f) \end{array}

$\begin{array}{l} rec: (nat \to nat) \to nat \to nat \to nat \\ rec\ f\; z\; n = f(f(\ldots f(z))) \qquad \mbox{($n$ times $f$)} \end{array}$

wäre viel weniger mächtig als das vollständige (primitive) Rekursionsschema

r e c_{U} : (U \to U) \to U \to n a t \to U

$rec_U: (U \to U) \to U \to nat \to U$

da letzteres in etwa einem polymorphen Begriff in System F ähnelt, der bei vielen Typen verwendet werden kann $U$ .

In der Tat das Grundlegende $rec$ gibt uns nur Zugang zum primitiven Rekursionsschema erster Ordnung, wie wir es in einem Buch zur Berechenbarkeits- / Rekursionstheorie finden können. Nur damit wissen wir, dass Funktionen wie die von Ackermann nicht definierbar sind. (Nun, das ist nicht so offensichtlich, da wir hier auch Lambdas höherer Ordnung haben, es ist nur die Rekursion, die eingeschränkt ist. Aber der Punkt sollte trotzdem bestehen, denke ich.)

Mit dem $rec_U$ Schema können wir stattdessen wählen $U = nat \to nat$ , was es uns ermöglicht, Ackermanns Funktion zu definieren, wie Girard in dem vom OP erwähnten Buch zeigt. Daher ist das Schema streng leistungsfähiger.

Chi
quelle

Dies ist eine interessante Frage, deren Antwort absolut nicht trivial ist.

Ich werde zuerst die kurze Antwort geben: Es gibt eine Hierarchie von Systemen, nennen Sie sie $T_k$ , wo die einzigen erlaubten Rekursoren sind $\mathrm{rec}_U$ mit der Reihenfolge von $U\leq k$ , wobei die Reihenfolge eines Typs wie folgt definiert ist:

o r d (n a t) = 0

$\mathrm{ord}(\mathrm{nat})=0$

o r d (U \to V) = max (o r d (V), o r d (U) + 1)

$\mathrm{ord}(U\rightarrow V)= \max(\mathrm{ord}(V),\mathrm{ord}(U)+1)$

Dann lautet der Satz:

Satz : für jeden $k$ gibt es einen Begriff $t_k:\mathrm{nat}\rightarrow\mathrm{nat}$ , so dass

$T_{k}\vdash t_k:\mathrm{nat}\rightarrow\mathrm{nat}$

$T_{k-1}\not\vdash t_k:\mathrm{nat}\rightarrow\mathrm{nat}$

$t_k$ wächst schneller (in Abhängigkeit von $\mathbb{N}\rightarrow\mathbb{N}$ ) als jede in definierbare Funktion $T_l$ mit $l<k$ .

Beachten Sie, dass $T=\bigcup_k T_k$ .

Als ersten Schritt ist es wahrscheinlich nützlich zu bemerken, dass die Ackermann-Funktion so definiert werden kann (wie in Chis Antwort angedeutet ):

a c k (n, m) = {r e c}_{n a t \to n a t} (λ f . {r e c}_{n a t} f 0 m) (λ p . S p) n

$\mathrm{ack}(n,m) = \mathrm{rec}_{\mathrm{nat}\rightarrow\mathrm{nat}}(\lambda f.\mathrm{rec}_{\mathrm{nat}}\ f\ 0\ m)\ (\lambda p.S\ p)\ n$ Modulo ein Fehler von meiner Seite.

Dies legt in der Tat nahe, dass $\mathrm{rec}_{\mathrm{nat}\rightarrow\mathrm{nat}}$ hatte zusätzliche "Kraft".

Aber wie gehen wir den ganzen Weg den Turm hinauf, um willkürlich zu sein? $T_k$ ?

Der Trick besteht darin, eine dreifache Entsprechung zwischen:

1) Ordnungszahlen unten $\varepsilon_0$

2) Fragmente von $\mathrm{HA}_k$ der Heyting-Arithmetik, bei der die Induktion auf Aussagen mit weniger als beschränkt ist $k$ Quantifiziererwechsel.

3) Funktionen definierbar in $T_k$

Für jede Ordnungszahl $\lambda_k=\omega^{\omega^{{\dots}^\omega}}$ wo der Turm von Höhe ist $k$ Es ist möglich, einen Beweis in der Heyting-Arithmetik zu betrachten, dass eine solche Ordnungszahl begründet ist, und daraus einen Begriff zu extrahieren $t_k$ im System typisierbar $T_k$ was der Funktion entspricht $g_{\lambda_k}$ in der Grzegorczyk-Hierarchie .

Ein solcher Begriff kann nicht gut eingegeben werden $T_{k-1}$ aufgrund der oben beschriebenen Korrespondenz und der Tatsache, dass $\mathrm{HA}_{k-1}$ beweist nicht die Begründetheit von $\lambda_k$ .

Lügen und Referenzen :

Die Korrespondenz zwischen $T_k$ , $\mathrm{HA_k}$ und $\lambda_k$ ist nicht ganz so sauber wie ich vorgeschlagen habe, sollte es eigentlich geben $k$ , $k'$ und $k''$ , jeweils durch eine konkrete Konstante verbunden.

Eine explizite Konstruktion für die $t_k$ entlang des oben beschriebenen Weges wird von Ulrich Berger in der Programmextraktion aus Gentzens Beweis der transfiniten Induktion bis zu angegeben $\varepsilon_0$

Ich fürchte, ich habe keine bessere Referenz für die dreifache Korrespondenz als Proofs and Types , obwohl ich mich sehr freuen würde, von einer zu hören.

Cody
quelle