¿Cuáles son los límites de la programación funcional total?

¿Cuáles son las limitaciones de la programación funcional total? No es completo de Turing, pero aún admite un gran subconjunto de los posibles programas. ¿Hay construcciones importantes que podrías escribir en un lenguaje completo de Turing, pero no en un lenguaje funcional total?

¿Y es correcto decir que los programas escritos en lenguajes funcionales totales se pueden analizar completamente estáticamente, mientras que el análisis estático en lenguajes completos de Turing está limitado por cosas como el problema de detención? Con eso no quiero decir que en lenguajes funcionales totales todo se pueda determinar estadísticamente, porque algunas cosas solo se conocen en tiempo de ejecución, pero quiero decir que en teoría, los programas escritos en un lenguaje de programación funcional total ideal, se pueden analizar para que todo lo que en teoría podría determinarse estáticamente puede determinarse estáticamente. ¿O todavía hay problemas indecidibles heredados en lenguajes funcionales totales que hacen que el análisis estático sea incompleto? Algunos problemas siempre serán indecidibles, sin importar en qué idioma estén escritos, pero estoy interesado en los problemas que se heredan del idioma,

computability pl.programming-languages functional-programming Matthijs Steen
fuente

Respuestas:

Depende del lenguaje funcional total .

Esta respuesta suena como una evasión, pero no se puede decir nada más específico. Después de todo, considere cualquier programa decisivo importante que le interese. Escriba un programa en su idioma favorito de Turing-complete para resolverlo. Como el problema es decidible, su programa se detendrá en todas las entradas.

(Podría decirse que un problema no decidible podría tener programas interesantes, pero no tales que la gente pueda usar, porque nunca podrán esperar lo suficiente como para saber la respuesta).

Ahora, defina un nuevo lenguaje de modo que tenga solo un programa de entrada válido: el programa que acaba de escribir, con la misma semántica que tenía antes. Ciertamente es total, ya que todas las entradas a todos los programas escritos en él (de los cuales solo hay uno) siempre terminan.

Este truco barato es realmente útil: el lenguaje Coq , por ejemplo, es un lenguaje funcional total en el que ningún programa verifica a menos que haya una prueba de que termina. (Si tuviera que renunciar a ese requisito, sería Turing completo, por lo que el único obstáculo es encontrar una prueba de finalización).

No estoy seguro de lo que quiere decir con "todo lo que en teoría podría determinarse estáticamente puede determinarse estáticamente"; Suena tautológicamente cierto. No obstante, los idiomas totales no son inherentemente fáciles de analizar; sabes que nada diverge, lo cual es un hecho útil, pero la relación entre entrada y salida sigue siendo compleja. (En particular, todavía hay infinitas entradas posibles, por lo que no puede probarlas exhaustivamente, incluso en teoría).

Paul Stansifer
fuente

Gracias por tu respuesta. Por lo tanto, ser total ayuda un poco, pero sigue siendo un problema muy difícil. Lo que quise decir con "todo lo que en teoría podría determinarse estáticamente puede determinarse estáticamente" es que sería posible, extremadamente difícil o no, analizar todas las relaciones entre entrada y salida, si tuviera suficientes recursos para hacerlo. . ¿O son las razones fundamentales por las que esto es limitado? Al igual que la prueba de la prueba de Rice de que este es el caso de las funciones parciales. ¿O estoy malentendido el teorema de Rice?

Matthijs Steen

Creo que puede depender de lo que quieres decir con "relación". En particular, si solo quiere decir "la entrada A va a la salida B", esto es trivialmente determinable en un lenguaje funcional total; solo ejecuta el programa. Pero probablemente le interesen los análisis que dicen algo sobre una clase infinita de entradas.

Paul Stansifer

(Ups; pulsa Intro accidentalmente) ... pero esto abre otro truco tonto, porque puedo hacer preguntas indecisas sobre la función de identidad si quiero: "Para algunos X, ¿hay (identity X)una máquina de Turing que se detiene?" Claro, eso no parece ser sobre identity , pero ¿cómo define "acerca de"?

Paul Stansifer

Sí, quiero saber si se cumple para todos los valores de entrada posibles de alguna definición, no para entradas individuales. Entonces, si te entiendo correctamente, ¿quieres decir que siempre habrá algunas preguntas indecidibles, sin importar qué tipo de lenguaje de programación se use? Aunque algunas de estas preguntas indecidibles se pueden eludir evitando que el problema ocurra en primer lugar, como los lenguajes funcionales totales para el problema de detención. ¿Porque su pregunta sobre la función de identidad no sería decidible en un lenguaje funcional total?

Matthijs Steen

Si; una versión modificada del problema, en la que "Máquina de Turing" se reemplaza por "Se descompone después de que caduca su garantía, la Máquina de Turing" es trivialmente solucionable. Es un poco problemático para estos propósitos que el problema de detención sea el ejemplo de un problema indecidible cuando el examen de programas está lleno de indecidibilidad.

Paul Stansifer

¿Cuáles son las limitaciones de la programación funcional total? No es completo de Turing, pero aún admite un gran subconjunto de los posibles programas. ¿Hay construcciones importantes que podrías escribir en un lenguaje completo de Turing, pero no en un lenguaje funcional total?

$L$ $L$ $L$

$L$ $L$ $L$ $L$ es consistente. Esto es justo lo que descarta el teorema de Goedel, suponiendo que pueda hacer aritmética. Entonces sabemos que no podemos escribir autointerpretadores en lenguajes funcionales totales.
Sin embargo, la otra cara de esto es que los límites del poder expresivo de las lenguas totales son esencialmente los límites del poder expresivo de las matemáticas mismas . Por ejemplo, las funciones definibles en Coq (un asistente de prueba) son aquellas que pueden demostrarse que son computables usando ZFC, con innumerables cardenales inaccesibles. Por lo tanto, esencialmente cualquier función que pueda probar total para la satisfacción de un matemático que trabaja es definible en Coq.
El otro lado del otro lado es que las matemáticas son difíciles. Por lo tanto, no hay un sentido fácil en el que los lenguajes totales sean "completamente analizables", incluso si sabe que una función termina, es posible que aún tenga que hacer mucho trabajo creativo para demostrar que tiene una propiedad que desea. Por ejemplo, el simple hecho de saber que una función de listas a listas es total, no te lleva muy lejos al demostrar que es una función de clasificación ...

Neel Krishnaswami
fuente

Gracias por tu respuesta. He leído la publicación sobre este problema en el weblog de Lambda the Ultimate , pero algunas personas en los comentarios afirman que, aunque no es posible tener su propio evaluador como un término regular explícitamente constructivo, sería posible crear un trabajo propio. evaluador con algunos trucos. Entonces, me pregunto, ¿hay problemas que no se puedan resolver (o aproximar) en un lenguaje funcional total con algunos trucos de desvíos?

Matthijs Steen

Yo diría que la autoevaluación no cuenta como un problema, ya que varía según el idioma. El problema "evaluar un programa en el lenguaje X" es el mismo problema, independientemente de si intenta resolverlo en el lenguaje X o Y. En particular, si el lenguaje X es un lenguaje funcional total, el problema se puede resolver en algún lenguaje funcional total , usando el mismo truco tonto que usé antes.

Paul Stansifer

Neel, parece que debería ser considerablemente más fácil que eso demostrar que un lenguaje total no puede soportar su propio intérprete. ¿Te estoy malentendiendo? Por una simple diagonalización, cualquier lenguaje con una función sin puntos fijos no puede soportar su propio intérprete (ya sea que soporte aritmética o no). El argumento es elaborado por Conor McBride aquí: mail.haskell.org/pipermail/haskell-cafe/2003-May/004343.html

Tom Ellis

@TomEllis: Mi argumento es esencialmente el mismo que el de Conor. De hecho, su publicación ya hace esta observación (con el ingenio característico de Conor) cuando la llama "el argumento Epiménides / Cantor / Russell / Quine / Godel / Turing".

Neel Krishnaswami