Pojęcia wydajnego obliczenia

Algorytm maszyny Turinga w czasie wielomianowym jest uważany za wydajny, jeśli jego czas działania, w najgorszym przypadku, jest ograniczony przez funkcję wielomianu w wielkości wejściowej. Mam świadomość silnej tezy Kościoła-Turinga:

Każdy rozsądny model obliczeń może być skutecznie symulowany na maszynach Turinga

Nie znam jednak solidnej teorii do analizy złożoności obliczeniowej algorytmów rachunku.$\lambda$

Czy mamy pojęcie wydajności obliczeniowej dla każdego znanego modelu obliczeń? Czy są jakieś modele, które są przydatne tylko w przypadku pytań dotyczących obliczalności, ale są bezużyteczne w przypadku pytań o złożoności obliczeniowej?

O ile mi wiadomo, głównymi modelami obliczalności są rachunek λ, maszyny Turinga i funkcje rekurencyjne . Nie jestem świadomy sytuacji dotyczącej złożoności funkcji rekurencyjnych, mogą one, ale nie muszą być bezużyteczne dla złożoności.

Można uznać za szczęśliwy przypadek, że maszyny Turinga, które nie są tak bardzo niewydajnymi maszynami, są również bardzo dobrym modelem złożoności. To, co sprawiło, że wszystko stało się naturalne, polega na tym, że zachodzi wiele transformacji wielomianowych baz TM. (Maszyna uniwersalna, symulacja maszyny w kształcie litery z maszyną z 1 taśmą, od dowolnego alfabetu do binarnego, symulująca pamięć PRAM$n$ , ...) oraz że wielomiany są klasą funkcji stabilnych przez operacje arytmetyczne i skład - co czyni ich dobrym kandydatem do teorii złożoności.

Czysty rachunek λ był sam w sobie bezużyteczny ze względu na złożoność. W grę wszedł jednak prosty system typów, który w bardzo łatwy sposób umożliwiał gwarancje zakończenia niektórych terminów λ. Następnie niektóre inne systemy (systemy T , F , ..) pozwalały na dużą ekspresję przy zachowaniu terminacji.

Wydajność lub złożoność będąca udoskonaleniem terminacji i typy ściśle związane z logiką, później pojawiła się lekka logika liniowa, która charakteryzuje kilka klas złożoności. ( Elementary , P i niektóre odmiany dla PSPACE i innych). Badania w tej dziedzinie są bardzo aktywne i nie są ograniczone do tych klas złożoności, a nawet nie są ograniczone do rachunku λ.

tl; dr: rachunek λ był przydatny do obliczeń, terminacji i teorii złożoności.

Jednak, aby wyrazić uznanie tam, gdzie należy się uznanie, maszyny Turinga są dobrym i jednogłośnym sposobem zdefiniowania, co jest złożonością, ale dotyczy to tylko luźnych granic, takich jak „wielomian”, a nie ciasnych granic, dla których modele podobne do PRAM są bardziej odpowiednie.

$\beta$

O włączeniu rachunku λ do standardowego modelu złożoności, oto streszczenie niektórych (bardzo) świeżych badań na ten temat. Daje odpowiedź na to pytanie dla pewnej ograniczonej formy redukcji β. Zasadniczo złożoność w modelu standardowego kosztu jest podobna do zliczania kroków redukcji β, gdy ogranicza się do redukcji głowicy (która obejmuje strategie „nazwa po imieniu” i strategia „wartość po wartości”).

O niezmienności modelu jednostkowego kosztu redukcji głowy autorstwa Beniamino Accattoli i Ugo Dal Lago. (WST2012, link do postępowania )

Rachunek λ jest szeroko akceptowanym modelem obliczeniowym programów funkcjonalnych wyższego rzędu, ale nie ma dla niego żadnego bezpośredniego i powszechnie akceptowanego modelu kosztów. W związku z tym obliczeniową trudność zredukowania warunków λ do ich normalnej postaci zazwyczaj bada się, argumentując na konkretnych algorytmach implementacyjnych. Tutaj pokazujemy, że gdy redukcja głowy jest podstawową dynamiką, model kosztu jednostkowego jest rzeczywiście niezmienny. Poprawia to znane wyniki, które dotyczą jedynie słabej redukcji (według wartości lub według nazwy). Niezmienność dowodzi się za pomocą rachunku liniowego jednoznacznych podstawień, który pozwala na ładny rozkład dowolnego kroku redukcji głowy w rachunku λ na bardziej elementarne etapy podstawienia, dzięki czemu łatwiej jest zrozumieć kombinatorykę redukcji głowy.