Comprensión finita de una lista infinita

Question

Escribí lo siguiente en ghci, pensando que sucedería una de dos cosas: 1) El intérprete se bloqueaba, buscando en cada miembro de una lista infinita las coincidencias con un predicado; o 2) a través de las cortinas Haskell Jujitsu, el intérprete de alguna manera descubriría que la secuencia termina en 4 y se detiene allí.

[x | x <- [1..],5>x] 

Resultado 1 fue lo que sucedió. Ahora, el resultado 2 era mucho pedir. Pero dado que un humano puede probar que la secuencia termina en 4, ¿podría haber alguna manera de lograr que el intérprete lo haga? ¿Podría ser reescrito de tal manera que termine? De hecho, ¿hay alguna vez un predicado que hace una comprensión finita de una lista infinita?

Answer 1

Pero como un humano puede demostrar que la secuencia termina en 4, ¿podría haber alguna manera de conseguir que el intérprete lo haga?

En este caso simple, sí. Pero no puede existir un algoritmo general para determinar si una expresión es verdadera o falsa para todos los números naturales >n para algunos n, porque Haskell es Turing-completo, por lo que es imposible probar que una expresión represente un programa de terminación para todos los números naturales.

Incluso si su expresión estuviera limitada a la aritmética entera básica, su verdad aún sería indecidible en el caso general.

¿Podría reescribirse de tal manera que termine?

Como Mog escribió en el comentario, es takeWhile (< 5) [1..].

Answer 2

takewhile es la solución correcta para su problema específico, como se mencionó anteriormente.

Sin embargo, esto es solo porque en su caso, todos los argumentos aceptables vienen antes que todos los argumentos inaceptables, y la comprensión general de la lista no obedece a esa restricción. Sin duda sería posible agregar un razonamiento simbólico al intérprete para que pueda probar que no se aceptarán más elementos y luego terminar. (De hecho, el sofisticado sistema de tipos en Haskell sería bastante útil para implementar dicho razonamiento). Pero no tendría sentido agregar esto al operador estándar [|], ya que el detector debería ejecutarse en todas las listas de comprensión de que están evaluado, y muy a menudo no contribuiría nada, excepto mucho más gasto de computación.

Answer 3

Este es un problema de IU.

Prolog tiene cut operador; en Haskell podemos especificar de antemano cuántas soluciones esperamos. Al igual que en su ejemplo complejo (en los comentarios), take 5 $ map f [1..] funcionaría, pero take 6 ... seguiría en un bucle. Para superar eso, necesitaríamos un sistema de tiempo de ejecución que sea un probador de teoremas (como han dicho otros), y/o un evaluador parcial especulativo optimista de tiempo que retiene que abriría "buzones de respuesta" en vivo para cada solicitud del usuario. Eso implicaría posiblemente cálculos de etiquetado con un valor de prioridad (también en el nivel de idioma).

Creo que esto sería muy práctico en todos los sentidos.Nos dejaría salir con la escritura de código simple intuitivo que era la promesa inicial del enfoque de razonamiento ecuacional de todos modos. Inicialmente, un código se ejecutaba en el modo Haskell normal, pero luego el analizador se activaba para los cálculos rezagados.

Los intérpretes están inactivos la mayor parte del tiempo, de todos modos. Computadoras también, principalmente.

---

(más tarde Además) Véase, por ejemplo, the speculation package-"Un marco para paralelismo segura, programable, especulativa".

Y, por supuesto, V8, donde "código compilado se optimiza adicionalmente (y re-optimizado) de forma dinámica en tiempo de ejecución, basado en la heurística de perfil de ejecución del código".

Answer 4

"Pero dado que un ser humano puede demostrar que la secuencia termina en 4, podría haber una manera de conseguir el intérprete de hacerlo?"

Buena pregunta. Lo difícil no es la prueba de que termine en 4, sino la idea de que posiblemente podría terminar en 4, seguido por la percepción de que esto es así.