Używasz rachunku lambda do uzyskania złożoności czasu?

Czy są jakieś korzyści z obliczania złożoności czasowej algorytmu za pomocą rachunku lambda? Czy istnieje inny system zaprojektowany do tego celu?

Wszelkie referencje będą mile widziane.

Ohad ma rację co do problemów, które napotyka rachunek lambda jako podstawa do mówienia o klasach złożoności. Dużo pracy włożono w scharakteryzowanie złożoności redukowalności w rachunku lambda, szczególnie wokół pracy nad oznakowanymi i optymalnymi redukcjami z pracy doktorskiej Lèvy'ego. Ogólnie rzecz biorąc, dobre modele kosztów dla rachunku lambda nie powinny przypisywać stałej wagi wszystkim redukcjom beta: intuicyjnie, zastępowanie dużego podtermiku w wielu miejscach o różnym zasięgu powinno kosztować więcej niż zawieranie małej redeksu K, a jeśli ktoś chce określonej kwoty niezmienności kosztów w ramach różnych strategii przepisywania, staje się to niezbędne.

Dwa linki:

1. Lawall i Mairson, 1996, Optymalność i nieefektywność: co nie jest modelem kosztów rachunku lambda? (.ps.gz) - Seminalna ankieta dotycząca problemów związanych z wyborem modelu kosztów i dlaczego wiele wiarygodnych pomysłów nie działa.
2. Dal Lago i Martini, 2008, Słaby rachunek lambda jako rozsądna maszyna - Oferuje model kosztu dla rachunku lambda call-by-value, wraz z dobrym omówieniem literatury.

Istnieją wyniki ilościowe dotyczące rachunku , w postaci pomiaru długości redukcji w (typowanym) rachunku lambda. Jest to oczywiście dalekie od mówienia o złożoności algorytmów (szczególnie, że uzyskane granice szybko rosną). Patrz na przykład: Arnold Beckmann, Dokładne granice dla długości redukcji w maszynowym -calculus, Journal of Symbolic Logic 2001, 66 (3): 1277-1285.$\lambda$$\lambda$

Jeśli chodzi o coś bliższego Twojemu pytaniu, istnieje bieżący projekt, który rozwija i bada system typów (funkcjonalny język programowania), który poprzez analizę statyczną może określić (wielomianowe) granice programów (a także inne zasoby wykorzystywane przez programy). W pewnym sensie może to sugerować, że wykorzystanie programowania funkcjonalnego do analizy złożoności w czasie wykonywania może być korzystne. Strona główna projektu jest tutaj .

Prawdopodobnie przedstawicielem tego projektu jest: Jan Hoffmann, Martin Hofmann. Amortyzowana analiza zasobów z potencjałem wielomianowym - statyczne wnioskowanie granic wielomianu dla programów funkcjonalnych. W materiałach z 19. Europejskiego Sympozjum Programowania (ESOP'10). połączyć

Ostatnie rozwinięcie tego tematu: U. dal Lago i B. Accatoli udowodnili, że długość skrajnie lewej skrajnej redukcji (LOr) terminu jest niezmiennym (czasowym) modelem kosztu dla -kalkusa.$\lambda$$\lambda$

Pokazują, że maszyny Turinga (z cost = time) i -terms (z cost = length of LOr) mogą symulować się nawzajem z wielomianowym narzutem w czasie. Na przykład definicja klasy P nie zależy od tego, który z dwóch modeli obliczeniowych użyjesz do jej zdefiniowania.$\lambda$

http://arxiv.org/abs/1405.3311

Istnieje bardzo interesująca linia pracy oparta na logice liniowej, zwana teorią złożoności niejawnej, która charakteryzuje różne klasy złożoności poprzez narzucanie różnych rodzajów dyscyplin na rachunek lambda. IIRC, praca ta rozpoczęła się, gdy Bellantoni i Cook oraz Leivant wymyślili, jak wykorzystać system typów do powiązania pierwotnej rekurencji w celu przechwycenia różnych klas złożoności.

Ogólnie rzecz biorąc, przyciąganie do pracy z kalkulacjami lambda polega na tym, że czasem można znaleźć bardziej ekstensywne (tj. Bardziej matematyczne) cechy różnych intensywnych cech, które dają modelom takim jak maszyny Turinga ich moc. Na przykład jedna różnica między maszynami Turinga a rachunkiem czystego lambda polega na tym, że ponieważ Turing odbiera kody programów, klient może ręcznie wprowadzić limity czasu, aby zaimplementować połączenie typu „jaskółczy ogon” - a zatem może obliczać równolegle lub. Jednak limity czasu można również modelować metrycznie, a Escardo domyślił się (nie znam jego statusu), że modele przestrzeni metrycznej rachunku lambda są w pełni abstrakcyjne dla limitów czasu PCF +. Przestrzenie metryczne są bardzo dobrze zbadanymi obiektami matematycznymi i bardzo miło jest móc korzystać z tego zbioru teorii.

Jednak trudność w stosowaniu rachunku lambda polega na tym, że zmusza cię do stawienia czoła zjawiskom wyższego rzędu już od bramki startowej. Może to być bardzo subtelne, ponieważ teza Kościoła Turinga zawodzi na wyższym typie - naturalne modele obliczeń różnią się na wyższym typie, ponieważ różnią się tym, co wolno robić z przedstawieniami obliczeń. (Równoległy - lub jest prostym przykładem tego zjawiska, ponieważ wykazuje różnicę między LC a TM). Co więcej, nie ma nawet ścisłego włączenia między różnymi modelami, ponieważ sprzeczność przestrzeni funkcji oznacza, że ​​bardziej ekspresyjna moc w jednym rzędzie implikuje mniej ekspresyjną moc o jeden rząd wyżej.

O ile mi wiadomo, rachunek lambda jest nieodpowiedni do tego celu, ponieważ pojęcie złożoności czas / przestrzeń jest trudne do sformułowania w rachunku lambda.

Co to jest 1 jednostka złożoności czasu? Zmniejszenie wersji beta? Co z jednostkami złożoności przestrzeni? Długość sznurka?

Rachunek Lambda jest bardziej odpowiedni do abstrakcyjnej manipulacji algorytmami, ponieważ jest znacznie łatwiejszy do skomponowania niż maszyny Turinga.

Można również wyszukać rachunek jawnych podstawień, które dzielą podstawienie meta-poziomu rachunku lambda na szereg wyraźnych kroków redukcji. Dotyczy to stwierdzenia Charlesa, że ​​wszystkie zmiany nie powinny być uważane za takie same, jeśli wziąć pod uwagę złożoność czasu.

Patrz Nils Anders Danielsson, Lekka analiza złożoności czasu półformalnego dla czysto funkcjonalnych struktur danych, która jest zaimplementowana jako biblioteka w Agdzie. Cytowania podane w artykule również wyglądają bardzo obiecująco.

Jedną z kluczowych rzeczy dla mnie jest to, że właściwe / użyteczne / rozsądne / półautomatyczne jest uzyskanie złożoności czasowej algorytmów w prostym typie rachunku lambda, szczególnie jeśli te algorytmy są w nim łatwo wyrażalne (tj. Czysto funkcjonalne), a szczególnie, jeśli te algorytmy zasadniczo wykorzystują np. semantykę call-by-name. Wraz z tym jest prawdopodobnie oczywisty punkt, że nie oblicza się złożoności tylko „w rachunku lambda”, ale w rachunku lambda w ramach danej strategii oceny.