Äquivalente Formulierung der Komplexitätstheorie in der Lambda-Rechnung?

In der Komplexitätstheorie beziehen sich die Definition von Zeit- und Raumkomplexität beide auf eine universelle Turingmaschine: resp. die Anzahl der Schritte vor dem Anhalten und die Anzahl der Zellen auf dem Band, die berührt wurden.

Angesichts der Church-Turing-These sollte es möglich sein, Komplexität auch in Bezug auf die Lambda-Rechnung zu definieren.

Meine intuitive Vorstellung ist, dass Zeitkomplexität als die Anzahl der β-Reduktionen ausgedrückt werden kann (wir können die α-Umwandlung unter Verwendung von De Brujin-Indizes weg definieren, und η ist sowieso kaum eine Reduktion), während Raumkomplexität als die Anzahl von definiert werden kann Symbole (λs, DB-Indizes, "Apply" -Symbole) in der größten Reduktion.

Ist das richtig? Wenn ja, wo kann ich eine Referenz bekommen? Wenn nicht, wie irre ich mich?

Wie Sie hervorheben, hat der λ-Kalkül eine scheinbar einfache Vorstellung von Zeitkomplexität: Zählen Sie einfach die Anzahl der β-Reduktionsschritte. Leider sind die Dinge nicht einfach. Wir sollten fragen:

 Is counting β-reduction steps a good complexity measure?

$M$$|M|$$M$$poly(|M|)$$tr(M)$$poly(|tr(M)|)$

Es war lange Zeit unklar, ob dies im λ-Kalkül erreicht werden kann. Die Hauptprobleme sind die folgenden.

• Es gibt Begriffe, die Normalformen in einer Polynomzahl von Schritten erzeugen, die exponentiell groß sind. Siehe (1). Selbst das Aufschreiben der normalen Formen nimmt exponentielle Zeit in Anspruch.

• Auch die gewählte Reduktionsstrategie spielt eine wichtige Rolle. Zum Beispiel gibt es eine Familie von Begriffen, die sich in einer Polynomzahl paralleler β-Schritte reduziert (im Sinne einer optimalen λ-Reduktion (2), deren Komplexität jedoch nicht elementar ist (3, 4).

Das Papier (1) verdeutlicht das Problem, indem es eine vernünftige Codierung zeigt, die die Komplexitätsklasse PTIME unter der Annahme von Call-By-Name-Reduzierungen ganz links beibehält . Die wichtigste Erkenntnis scheint zu sein, dass das exponentielle Aufblasen nur aus uninteressanten Gründen erfolgen kann, die durch das ordnungsgemäße Teilen von Unterbegriffen besiegt werden können.

Beachten Sie, dass Papiere wie (1) zeigen, dass grobe Komplexitätsklassen wie PTIME zusammenfallen, unabhängig davon, ob Sie β-Schritte oder Turing-Maschinenschritte zählen. Dies bedeutet nicht, dass auch Klassen mit geringerer Komplexität wie O (log n) zusammenfallen. Natürlich sind solche Komplexitätsklassen auch unter Variation des Turing-Maschinenmodells nicht stabil (z. B. 1-Band gegen Multi-Band).

D. Mazzas Arbeit (5) beweist den Cook-Levin-Satz (𝖭𝖯-Vollständigkeit von SAT) unter Verwendung einer funktionalen Sprache (eine Variante des λ-Kalküls) anstelle von Turing-Maschinen. Die wichtigste Erkenntnis ist folgende:

$$\frac{\text{Boolean circuits}}{\text{Turing machines}}=\frac{\text{affine $\lambda$-terms}}{\text{$\lambda$-terms}}$$

Ich weiß nicht, ob die Situation bezüglich der Raumkomplexität verstanden wird.

---

1. B. Accattoli, U. Dal Lago, Beta-Reduktion ist in der Tat unveränderlich .

2. J.-J. Levy, Reductions korrigiert und optimiert die Lambda-Berechnung.

3. JL Lawall, HG Mairson, Optimalität und Ineffizienz: Was ist kein Kostenmodell der Lambda-Rechnung ?

4. A. Asperti, H. Mairson, Parallele Beta-Reduktion ist nicht elementar rekursiv .

5. D. Mazza, Kirche trifft Koch und Levin .

$\beta$$\lambda$

$\mathsf L$$\mathsf P$$M\to^\ast N$$M$

$\beta$