Entonces, con SupGen acercándose, publicaré algunos contenidos tecnológicos que fracasarán porque no son contenidos de IA con muerte cerebral, pero quiero hacerlo de todos modos. A continuación se exponen algunas reflexiones sobre la totalidad y la terminación. En Agda (¿y Lean?), la terminación se asegura mediante "recursión estructural", lo que significa que los argumentos pueden decrecer en "orden lexicográfico". ¿Entiendes lo que esto significa? Sí, yo tampoco. Pero en realidad es bastante simple. Supón que tienes una cláusula como: foo : Nat → Nat foo (S a) (S b) (S c) (S d) = foo (S a) (S b) c (S (S (S d))) foo x = x ¿Está terminando? ¿No? ¿Cómo saberlo? En Agda, sucede así: Paso #0: - argumento 0 en LHS: (S a) - argumento 0 en RHS: (S a) - esto es *idéntico*, así que comprueba el siguiente argumento (nota: LHS/RHS significa lado izquierdo/derecho de la ecuación) Paso #1: - argumento 1 sobre LHS: (S b) - argumento 1 en RHS: (S b) - esto es *idéntico*, así que comprueba el siguiente argumento Paso #2: - argumento 2 sobre LHS: (S c) - argumento 2 en RHS: c - esto es *más pequeño*, por lo tanto, ¡esta cláusula termina! Y ya está. Entonces, en resumen, siempre que haya una llamada recursiva en el lado derecho, simplemente compare sus argumentos con los patrones correspondientes en el lado izquierdo, uno por uno, hasta que uno sea más pequeño. Sencillo, ¿no? (Ojalá pudieran haberlo explicado así...) Ahora, considere: foo : Par -> Par foo (Par (S a) (S b)) = foo (P a (S (S (S b)))) foo x = x ¿Esta función está finalizando? Bueno, según Agda... ¡no! Sin embargo, claramente lo es, por la misma lógica: dado que el primer componente es más pequeño, que el segundo sea más grande es irrelevante. Parece que el verificador de Agda está codificado para fragmentar los argumentos. Por lo tanto, esta cláusula, tal como está escrita, no pasará su verificador, aunque termine. ¿Por qué hablo de esto? Estaba revisando el generador de recursión de SupGen y me di cuenta de que podría ser más limpio *y* rápido con algunos cambios. ¿Pero son válidos estos cambios? Hice pruebas y, para mi sorpresa, SupGen generaba programas que no terminaban... según Agda. Al principio asumí que mi enfoque era incorrecto, pero resultó que Agda sí lo era. Ahora tienes un nuevo conocimiento. ¡Estoy seguro de que esto te resultará útil con el tiempo!
¡El nuevo algoritmo utilizado por SupGen para generar llamadas recursivas de terminación es mucho más simple *y* más general!
