Sind optimale Bewerter tatsächlich optimal?

Der folgende Begriff (unter Verwendung von Bruijn-Indizes):

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

Wenn es auf eine Kirchennummer angewendet wird, wird es Nin mehreren vorhandenen Bewertern, einschließlich naiver, schnell in normaler Form bewertet . Wenn Sie diesen Begriff jedoch in Interaktionsnetze codieren und ihn mit dem abstrakten Algorithmus von Lamping auswerten, ist eine exponentielle Anzahl von Beta-Reduktionen in Bezug auf erforderlich N. Auf Optlam, speziell:

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))))))))

Bei ähnlichen Evaluatoren wie BOHM sind viel weniger Beta-Schritte erforderlich, aber mehr Interaktionen. Wenn optimale Bewerter optimal sind, wie können sie Begriffe asymptotisch langsamer bewerten als vorhandene Bewerter?

Dieser Link enthält eine Erklärung zur Herkunft des Begriffs sowie eine Implementierung derselben Funktion, die sich fast bizarr verhält: Sie sollte in exponentieller Zeit ausgeführt werden - in den meisten Evaluatoren in exponentieller Zeit - und dennoch optimal Evaluatoren normalisieren es in linearer Zeit!

Effizienz von Optlam

Ich habe weder die Details von BADTERM noch die Implementierung des Optlam-Evaluators untersucht, aber ich finde es ziemlich seltsam, dass Optlam eine Reihe von ß-Wechselwirkungen durchführt, die sich drastisch von denen eines anderen optimalen Evaluators wie BOHM unterscheiden. Eine solche Zahl muss per Definition für einen bestimmten Begriff grundsätzlich gleich sein. Sind Sie sicher, dass der Kern von optlam korrekt ist?

Effizienz optimaler Bewerter

Es sei daran erinnert, dass der Begriff der Optimalität dieser Bewerter besser als Lévy-Optimalität bekannt ist und nicht der naive, da eine Strategie zur Reduzierung der Mindestanzahl von ß-Schritten nicht berechenbar ist. Was dann minimiert wird, ist die Anzahl paralleler ß-Reduktionsschritte, die an einer ganzen Familie von Redex durchgeführt werden, dh ungefähr die Menge, die durch das symmetrische und transitive Schließen der Beziehung erhalten wird, die zwei Redexe bindet, wenn eine von der anderen kopiert wird. Es sollte im Allgemeinen nicht überraschen, Diskrepanzen zwischen der Anzahl der ß-Schritte und dem Rest der Duplizierungsschritte zu sehen, da wir wissen, dass der größte Teil der Normalisierungslast von der ersteren auf die letztere übertragen werden könnte, wie von Asperti, Coppola und Martini [1].

Es sollte uns auch nicht überraschen zu sehen, dass die Gesamtzahl der Interaktionen, die zur Normalisierung eines Terms mit einem optimalen Bewerter erforderlich sind, geringer ist als bei einem normalen, da frühere empirische Beobachtungen bereits bemerkenswerte Leistungsverbesserungen zeigten. Trotzdem ist ein derart großer Komplexitätssprung von der exponentiellen zur linearen Zeit vielleicht der allererste seiner Art, der entdeckt wird. (Ich werde das überprüfen.)

Andererseits sind die theoretischen Ergebnisse zur Effizienz der optimalen Reduktion (was Ihre große Frage ist) immer noch wenige und noch nicht allgemein, da sie auf EAL-typisierte Proof-Netze beschränkt sind (was im Grunde die gleiche Einschränkung des Optmals darstellt) Evaluator, wenn ich das richtig verstehe), aber alle sind leicht positiv, da im schlimmsten Fall die Komplexität der Sharing-Reduktion durch einen konstanten Faktor durch den gewöhnlichen begrenzt wird [2,3].

Verweise

1. A. Asperti, P. Coppola und S. Martini, (Optimal) Duplizierung ist nicht elementar rekursiv , Information and Computation, vol. 193, 2004.
2. P. Baillot, P. Coppola und U. Dal Lago, Lichtlogik und optimale Reduktion: Vollständigkeit und Komplexität , Information und Berechnung, vol. 209, nein. 2, S. 118–142, 2011.
3. S. Guerrini, T. Leventis und M. Solieri, Tief in die Optimalität - Komplexität und Korrektheit der gemeinsamen Nutzung der Implementierung begrenzter Logik , DICE 2012, Tallin, Estland, 2012.