¿Los evaluadores óptimos son realmente óptimos?

10

El siguiente término (usando índices 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)))))))))

Cuando se aplica a un número de iglesia se Nevalúa rápidamente a su forma normal en varios evaluadores existentes, incluidos los ingenuos . Sin embargo, si codifica ese término en redes de interacción y lo evalúa usando el algoritmo abstracto de Lamping, se necesita un número exponencial de reducciones beta en relación con N. En Optlam, específicamente:

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

En evaluadores similares como BOHM, se requieren muchos menos pasos beta, pero más interacciones. Si los evaluadores óptimos son óptimos, ¿cómo pueden evaluar términos asintóticamente más lentos que los evaluadores existentes?

Este enlace tiene una explicación sobre el origen del término, así como una implementación de la misma función que se comporta de manera opuesta, casi de manera extraña: debe ejecutarse en tiempo exponencial; en la mayoría de los evaluadores funciona en tiempo exponencial; sin embargo, es óptimo ¡Los evaluadores lo normalizan en tiempo lineal!

MaiaVictor
fuente

Respuestas:

5

Eficiencia de optlam

No he estudiado los detalles de BADTERM ni de la implementación del evaluador optlam, pero me parece bastante extraño que optlam realice una serie de interacciones ß drásticamente diferentes a otro evaluador óptimo como BOHM. Tal número debe ser, por definición, básicamente el mismo en un término dado. ¿Estás seguro de la corrección del núcleo de optlam?

Eficiencia de evaluadores óptimos

Recuerde que la noción de optimización de estos evaluadores se conoce más propiamente como Lévy-optimality, y no es la ingenua, ya que una estrategia de reducción que realiza el número mínimo de ß-pasos no es computable. Lo que se minimiza, entonces, es el número de pasos de reducción ß paralelos realizados en una familia completa de redex, que es aproximadamente el conjunto obtenido por el cierre simétrico y transitivo de la relación que une dos redexes cuando uno se copia del otro. En general, no debería sorprender ver discrepancias entre el número de pasos ß y el resto de pasos de duplicación, ya que sabemos que la mayor parte de la carga de normalización podría transferirse del primero al segundo, como lo muestran Asperti, Coppola y Martini [1].

Tampoco debería sorprendernos ver que el número total de interacciones necesarias para normalizar un término con un evaluador óptimo es menor que con uno ordinario, ya que la observación empírica previa ya mostró notables mejoras en el rendimiento. Sin embargo, a pesar de esto, un salto de complejidad tan enorme, del tiempo exponencial al lineal, es quizás el primero de este tipo que se descubre. (Comprobaré esto)

Por otro lado, los resultados teóricos sobre la eficiencia de la reducción óptima (que es su gran pregunta), todavía son pocos y aún no generales, ya que se limitan a las redes de prueba de tipo EAL (que es básicamente la misma restricción de optmal evaluador, si lo entiendo correctamente), pero todos son ligeramente positivos, ya que en el peor de los casos la complejidad de compartir la reducción está limitada por la ordinaria por un factor constante [2,3].

Referencias

  1. A. Asperti, P. Coppola y S. Martini, (óptima) La duplicación no es recursiva elemental , Información y Computación, vol. 193, 2004.
  2. P. Baillot, P. Coppola y U. Dal Lago, Lógica de la luz y reducción óptima: Completitud y complejidad , Información y Computación, vol. 209, no. 2, págs. 118–142, 2011.
  3. S. Guerrini, T. Leventis y M. Solieri, Deep into optimality: complejidad y corrección de compartir la implementación de lógicas limitadas , DICE 2012, Tallin, Estonia, 2012.
Marco Solieri
fuente
Such a number must be, by definition, basically the same on a given termasí que pensé. Eso me sorprendió ya que Optlam da la misma cantidad de versiones beta que BOHM en muchos casos que probé. Sin embargo, en algunos casos da menos, debido a su estrategia de llamada por necesidad. Alguien me dijo que la reducción sin el oráculo no es realmente óptima y ahora ya no lo sé. En general, estoy profundamente confundido. Pero no, definitivamente no hay pruebas de que Optlam funcione correctamente. Estoy pensando en el resto de tu comentario, gracias.
MaiaVictor
Además, he encontrado muchos términos diferentes que se comportan igual que Badterm. Estoy estudiando más el tema para poder encontrar términos más simples que lo repliquen.
MaiaVictor
Una especie de estrategia paralela llamada por necesidad es estándar para los evaluadores óptimos, incluido BOHM, ya que es necesaria para la optimización de Lévy. El oráculo no es estrictamente necesario para reducir de manera óptima los términos λ: los términos estratificados, como los de tipo EAL, no lo necesitan.
Marco Solieri
Oh, mi mal, entonces. De todos modos, solo para asegurarme de que lo entiendo, cuando se tiene en cuenta la duplicación (no solo las versiones beta), ¿puede haber términos que sean asintóticamente más lentos para reducir en los evaluadores óptimos, incluso en el caso de tipo EAL? En ese caso, me pregunto por qué es significativo contar solo los pasos beta y si realmente hay algún beneficio en el uso de redes de interacción para la reducción del cálculo λ ...
MaiaVictor
1
¡Ajá! ¿Entonces hay términos que no se pueden escribir EAL que se pueden reducir sin el oráculo? Supuse que si Optlam lo reducía, era de tipo EAL (ya que no tengo un inferenciador de tipo EAL). Si ese no es el caso, entonces todo tiene sentido ahora. Dado que el subconjunto de términos que se pueden escribir con EAL tiene el poder suficiente para expresar cualquier algoritmo de poli-tiempo como la ordenación, creo que sería prudente intentar diseñar específicamente los términos que se pueden escribir con EAL. Sin embargo, me pregunto cómo podría hacerse en la práctica. Muchas gracias.
MaiaVictor