Czy optymalni ewaluatorzy faktycznie są optymalni?

Następujący termin (przy użyciu indeksów bruijn):

BADTERM = λ((0 λλλλ((((3 λλ(((0 3) 4) (1 λλ0))) λλ(((0 4) 3) (1 0))) λ1) λλ1)) λλλ(2 (2 (2 (2 (2 (2 (2 (2 0)))))))))

Po zastosowaniu do numeru kościoła Nszybko ocenia się w normalnej formie u kilku istniejących ewaluatorów, w tym naiwnych . Jeśli jednak zakodujesz ten termin w sieciach interakcyjnych i ocenisz go za pomocą abstrakcyjnego algorytmu Lampinga, zajmie to wykładniczą liczbę redukcji beta w stosunku do N. W przypadku Optlam, w szczególności:

N   interactions(betas)     (BADTERM N)
1   129(72)                 λλλ(1 (2 (2 (2 (2 (2 (2 (2 0))))))))
2   437(205)                λλλ(2 (1 (2 (2 (2 (2 (2 (2 0))))))))
3   976(510)                λλλ(1 (1 (2 (2 (2 (2 (2 (2 0))))))))
4   1836(1080)              λλλ(2 (2 (1 (2 (2 (2 (2 (2 0))))))))
5   3448(2241)              λλλ(1 (2 (1 (2 (2 (2 (2 (2 0))))))))
6   6355(4537)              λλλ(2 (1 (1 (2 (2 (2 (2 (2 0))))))))
7   11888(9181)             λλλ(1 (1 (1 (2 (2 (2 (2 (2 0))))))))
8   22590(18388)            λλλ(2 (2 (2 (1 (2 (2 (2 (2 0))))))))
9   43833(36830)            λλλ(1 (2 (2 (1 (2 (2 (2 (2 0))))))))
10  85799(73666)            λλλ(2 (1 (2 (1 (2 (2 (2 (2 0))))))))
11  169287(147420)          λλλ(1 (1 (2 (1 (2 (2 (2 (2 0))))))))
12  335692(294885)          λλλ(2 (2 (1 (1 (2 (2 (2 (2 0))))))))
13  668091(589821)          λλλ(1 (2 (1 (1 (2 (2 (2 (2 0))))))))
14  1332241(1179619)        λλλ(2 (1 (1 (1 (2 (2 (2 (2 0))))))))
15  2659977(2359329)        λλλ(1 (1 (1 (1 (2 (2 (2 (2 0))))))))

W przypadku podobnych ewaluatorów, takich jak BOHM, wymaga to znacznie mniej etapów beta, ale więcej interakcji. Jeśli optymalni ewaluatorzy są optymalni, w jaki sposób mogą oceniać terminy asymptotycznie wolniej niż obecni ewaluatorzy?

Ten link zawiera wyjaśnienie pochodzenia tego terminu, a także implementację tej samej funkcji, która zachowuje się odwrotnie, prawie dziwnie: powinna działać w czasie wykładniczym - w większości wykładników działa w wykładniczym czasie - jednak optymalnym ewaluatorzy znormalizują to w czasie liniowym!

Skuteczność optlamu

Nie badałem szczegółów BADTERM ani implementacji ewaluatora optlam, ale wydaje mi się dość dziwne, że optlam wykonuje szereg interakcji ß drastycznie różniących się od innych optymalnych ewaluatorów, takich jak BOHM. Taka liczba musi być z definicji zasadniczo taka sama dla danego terminu. Czy jesteś pewien poprawności rdzenia optlam?

Wydajność optymalnych oceniających

Przypomnijmy, że pojęcie optymalności tych ewaluatorów jest lepiej znane jako optymalizacja Lévy'ego i nie jest to naiwne, ponieważ strategia redukcji wykonująca minimalną liczbę kroków ß nie jest obliczalna. Zminimalizowana jest zatem liczba równoległych kroków redukcji ß wykonywanych na całej rodzinie redeksów, czyli mniej więcej zbiór uzyskany przez symetryczne i przechodnie zamknięcie relacji, która wiąże dwa redeksy, gdy jeden jest kopiowany z drugiego. Zasadniczo nie powinno dziwić zauważenie rozbieżności między liczbą kroków ß a resztą kroków duplikacji, ponieważ wiemy, że większość obciążenia normalizacyjnego można przenieść z tego pierwszego na drugi, jak pokazują Asperti, Coppola i Martini [1].

Nie powinno nas również dziwić, że całkowita liczba interakcji potrzebnych do normalizacji terminu z optymalnym ewaluatorem jest niższa niż ze zwykłym, ponieważ wcześniejsze obserwacje empiryczne wykazały już znaczną poprawę wydajności. Mimo to tak ogromny skok złożoności, od wykładniczego do liniowego, jest być może pierwszym tego rodzaju odkryciem. (Sprawdzę to.)

Z drugiej strony, teoretyczne wyniki dotyczące wydajności optymalnej redukcji (co jest waszym wielkim pytaniem), są wciąż nieliczne i jeszcze nie są ogólne, ponieważ ograniczają się do proofów typu EAL (co jest w zasadzie tym samym ograniczeniem optymalnym ewaluator, jeśli dobrze rozumiem), ale wszystkie są umiarkowanie pozytywne, ponieważ w najgorszym przypadku złożoność redukcji podziału jest ograniczona przez zwykłą stałą wartością [2,3].

Bibliografia

1. A. Asperti, P. Coppola i S. Martini, (Optymalne) Duplikacja nie jest elementarną rekurencją , Informacja i obliczenia, obj. 193, 2004.
2. P. Baillot, P. Coppola i U. Dal Lago, Logika światła i optymalna redukcja: Kompletność i złożoność , Informacje i obliczenia, vol. 209, nr 2, s. 118–142, 2011.
3. S. Guerrini, T. Leventis i M. Solieri, Głęboko w optymalność - złożoność i poprawność współdzielenia implementacji ograniczonej logiki , DICE 2012, Tallin, Estonia, 2012.