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 N
evalú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!
Such a number must be, by definition, basically the same on a given term
así 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.