haskell - ¿Cuál es el significado matemático de "todo(== 1)[1,1..]" que no termina?
math data-structures (3)
Intuitivamente, esperaría que la respuesta "matemática" a all (==1) [1,1..] sea True porque todos los elementos en una lista que solo contiene 1 son iguales a 1. Sin embargo, entiendo que "computacionalmente" ", el proceso de evaluación de la lista infinita para verificar que cada elemento de hecho es igual a 1 nunca terminará, por lo tanto, la expresión en su lugar" evalúa "a la parte inferior o ⊥ .
Encuentro este resultado contrario a la intuición y un poco desconcertante. Creo que el hecho de que la lista sea infinita confunde el problema matemática y computacionalmente, y me encantaría saber de alguien que tenga alguna idea y experiencia en esta área.
Mi pregunta es, ¿cuál es la respuesta más matemáticamente correcta? ⊥ o True ? También se apreciará mucho la elaboración de por qué una respuesta es más correcta que la otra.
editar: Esto podría tener algo que ver indirectamente con el isomorfismo de Curry-Howard (los programas son pruebas y los tipos son teoremas) y los teoremas de incompletitud de Gödel . Si no recuerdo mal, uno de los teoremas de incompletitud puede resumirse (increíblemente) como diciendo que "sistemas formales suficientemente poderosos (como las matemáticas o un lenguaje de programación) no pueden probar todas las afirmaciones verdaderas que se pueden expresar en el sistema"
El valor
all (==1) [1,1..]
es el límite superior mínimo de la secuencia
all (==1) (⊥)
all (==1) (1 : ⊥)
all (==1) (1 : 1 : ⊥)
...
y todos los términos de esta secuencia son ⊥, por lo que el límite superior mínimo también es ⊥. (Todas las funciones de Haskell son continuas: preservar los límites superiores mínimos).
Esto está usando la semántica de denotación para Haskell y no depende (directamente) al elegir cualquier estrategia de evaluación en particular.
En la programación, utilizamos la lógica no clásica, sino la lógica intuitiva (constructiva). Todavía podemos interpretar tipos como teoremas, pero no nos importa la verdad de estos teoremas; en cambio, hablamos sobre si son demostrables de forma constructiva . Aunque all (== 1) [1, 1 ..] es verdadero , no podemos probarlo en Haskell, así que obtenemos ⊥ (aquí, un ciclo infinito).
En la lógica constructiva, no tenemos como resultado la ley del medio excluido ni la eliminación de doble negación. La función Haskell escribe all (== 1) :: [Int] -> Bool no representa el teorema [Int] → Bool, que sería una función total; representa el teorema [Int] → ¬¬Bool. Si all pueden demostrar el teorema produciendo un resultado, entonces ese resultado será del tipo Bool ; de lo contrario, el resultado es inferior.
No sé lo suficiente sobre computabilidad para responder esto correctamente, pero me gusta la simplicidad en el diseño del lenguaje. En este caso, me parece simple y elegante que no all tiene que saber nada sobre la entrada que se le da. Es posiblemente más fácil para un humano razonar sobre el fragmento que usted ha dado.
Claro, ahora sería bueno para la lista infinita de comprensión de alguna manera decir a all que es una lista infinita de unos. Pero ... eso es lo que dice "por ser de ese valor". Tener un poco más de metadatos genéricos sobre la secuencia repetida sería más exitoso para fines de optimización, pero creo que se reduciría la simplicidad y se introduciría la complejidad.