Równoważne sformułowanie teorii złożoności w rachunku Lambda?

W teorii złożoności definicja złożoności czasu i przestrzeni odnosi się do uniwersalnej maszyny Turinga: odpowiednio. liczba kroków przed zatrzymaniem i liczba dotkniętych komórek na taśmie.

Biorąc pod uwagę tezę Kościoła-Turinga, powinno być możliwe zdefiniowanie złożoności również pod względem rachunku lambda.

Moje intuicyjne założenie jest takie, że złożoność czasu może być wyrażona jako liczba redukcji β (możemy zdefiniować konwersję α za pomocą indeksów De Brujina, a η i tak jest zaledwie zmniejszeniem), podczas gdy złożoność przestrzeni można zdefiniować jako liczbę symbole (λ, indeksy DB, symbole „zastosuj”) w największej redukcji.

Czy to jest poprawne? Jeśli tak, to gdzie mogę uzyskać referencję? Jeśli nie, to jak się mylę?

Jak zauważyłeś, rachunek λ ma pozornie proste pojęcie złożoności czasowej: wystarczy policzyć liczbę kroków redukcji β. Niestety, rzeczy nie są proste. Powinniśmy zapytać:

 Is counting β-reduction steps a good complexity measure?

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

Przez długi czas nie było jasne, czy można to osiągnąć za pomocą rachunku λ. Główne problemy są następujące.

• Istnieją terminy, które wytwarzają formy normalne w wielomianowej liczbie kroków o wielkości wykładniczej. Zobacz (1). Nawet zapisywanie normalnych formularzy zajmuje czas wykładniczy.

• Ważną rolę odgrywa również wybrana strategia redukcji. Na przykład istnieje rodzina terminów, która zmniejsza wielomianową liczbę równoległych kroków β (w sensie optymalnej redukcji λ (2), ale których złożoność nie jest elementarna (3, 4).

W artykule (1) wyjaśniono ten problem, pokazując rozsądne kodowanie, które zachowuje klasę złożoności PTIME, zakładając redukcję Call-By-Name najbardziej na lewo. Kluczowym spostrzeżeniem wydaje się być to, że wykładnicze wysadzenie może nastąpić tylko z nieciekawych powodów, które można pokonać poprzez odpowiednie dzielenie się warunków podrzędnych.

Zauważ, że dokumenty takie jak (1) pokazują, że zgrubne klasy złożoności, takie jak PTIME, pokrywają się, bez względu na to, czy liczone są kroki β, czy kroki maszyny Turinga. Nie oznacza to, że niższe klasy złożoności, takie jak O (log n), również się pokrywają. Oczywiście, takie klasy złożoności również nie są stabilne w zależności od modelu maszyny Turinga (np. 1-taśma vs wiele-taśma).

Praca D. Mazzy (5) dowodzi twierdzenia Cooka-Levina (𝖭𝖯-kompletność SAT) za pomocą języka funkcjonalnego (wariant rachunku λ) zamiast maszyn Turinga. Kluczowy wgląd jest następujący:

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

Nie wiem, czy zrozumiano sytuację dotyczącą złożoności przestrzeni.

---

1. B. Accattoli, U. Dal Lago, Beta Redukcja jest rzeczywiście niezmienna .

2. J.-J. Opłaty, redukcje korygują i optymalizują w obliczeniach lambda.

3. JL Lawall, HG Mairson, Optymalność i nieefektywność: co nie jest modelem kosztów rachunku lambda ?

4. A. Asperti, H. Mairson, Równoległa redukcja beta nie jest elementarną rekurencyjną .

5. D. Mazza, Church Meets Cook i Levin .

$\beta$$\lambda$

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

$\beta$