programming-languages - programming languages 2018

¿Cuáles son las limitaciones prácticas de un lenguaje completo no vinculante como Coq? (4)

En primer lugar, supongo que ya ha oído hablar de la tesis de Church-Turing , que afirma que todo lo que llamamos "computación" es algo que se puede hacer con una máquina de Turing (o cualquiera de los muchos modelos equivalentes). Entonces, un lenguaje completo de Turing es aquel en el que se puede expresar cualquier cálculo. Por el contrario, un lenguaje incompleto de Turing es aquel en el que hay algún cálculo que no se puede expresar.

Ok, eso no fue muy informativo. Déjame dar un ejemplo. Hay una cosa que no puedes hacer en un lenguaje incompleto de Turing: no puedes escribir un simulador de máquina de Turing (de lo contrario, podrías codificar cualquier cálculo en la máquina de Turing simulada).

Ok, eso todavía no fue muy informativo. la verdadera pregunta es, ¿qué programa útil no se puede escribir en un lenguaje incompleto de Turing? Bueno, nadie ha encontrado una definición de "programa útil" que incluya todos los programas que alguien haya escrito en algún lugar para un propósito útil, y eso no incluye todos los cálculos de máquinas de Turing. Entonces, diseñar un lenguaje incompleto de Turing en el que pueda escribir todos los programas útiles sigue siendo un objetivo de investigación a muy largo plazo.

Ahora hay varios tipos muy diferentes de Turing: idiomas incompletos, y difieren en lo que no pueden hacer. Sin embargo, hay un tema en común. Si está diseñando un idioma, existen dos formas principales de garantizar que el idioma sea Turing-completo:

requiere que el lenguaje tenga bucles arbitrarios ( while ) y asignación de memoria dinámica ( malloc )
requiere que el lenguaje admita funciones recursivas arbitrarias

Veamos algunos ejemplos de lenguajes no completos de Turing que algunas personas podrían llamar lenguajes de programación.

Las primeras versiones de FORTRAN no tenían una asignación de memoria dinámica. Debes averiguar de antemano cuánta memoria necesitaría tu computación y asignarla. A pesar de eso, FORTRAN alguna vez fue el lenguaje de programación más utilizado.
La limitación práctica obvia es que debe predecir los requisitos de memoria de su programa antes de ejecutarlo. Eso puede ser difícil, y puede ser imposible si el tamaño de los datos de entrada no está limitado de antemano. En ese momento, la persona que alimentaba los datos de entrada solía ser la persona que había escrito el programa, por lo que no era tan importante. Pero eso no es cierto para la mayoría de los programas escritos hoy.
Coq es un lenguaje diseñado para probar teoremas . Ahora probar teoremas y ejecutar programas están muy relacionados , por lo que puede escribir programas en Coq tal como lo demuestra un teorema. Intuitivamente, una prueba del teorema "A implica B" es una función que toma una prueba del teorema A como argumento y devuelve una prueba del teorema B.
Como el objetivo del sistema es probar teoremas, no puede permitir que el programador escriba funciones arbitrarias. Imagine que el lenguaje le permite escribir una función recursiva tonta que se acaba de llamar a sí mismo (elija la línea que usa su idioma favorito):
theorem_B boom (theorem_A a) { return boom(a); } let rec boom (a : theorem_A) : theorem_B = boom (a) def boom(a): boom(a) (define (boom a) (boom a))
¡No puedes dejar que la existencia de tal función te convenza de que A implica B, o de lo contrario serías capaz de probar cualquier cosa y no solo teoremas verdaderos! Así que Coq (y otros proponentes de teoremas similares) prohíben la recursión arbitraria. Cuando escribe una función recursiva, debe probar que siempre termina , de modo que cada vez que la ejecute en una prueba del teorema A sepa que construirá una prueba del teorema B.
La limitación práctica inmediata de Coq es que no puede escribir funciones recursivas arbitrarias. Como el sistema debe poder rechazar todas las funciones no terminales, la indecidibilidad del problema de detención (o, más en general, el teorema de Rice ) garantiza que haya funciones de terminación que también se rechazan. Una dificultad práctica añadida es que debe ayudar al sistema a demostrar que su función finaliza.
Hay una gran cantidad de investigaciones en curso sobre cómo hacer que los sistemas de prueba tengan más lenguaje de programación sin comprometer su garantía de que si tienes una función de A a B, es tan buena como una demostración matemática de que A implica B. Extender el sistema para aceptar más funciones de terminación es uno de los temas de investigación. Otras direcciones de extensión incluyen hacer frente a las preocupaciones del "mundo real" como entrada / salida y concurrencia. Otro desafío es hacer que estos sistemas sean accesibles a los simples mortales (o quizás convencer a los simples mortales de que de hecho son accesibles).
Los lenguajes de programación síncrona son lenguajes diseñados para programar sistemas en tiempo real, es decir, sistemas donde el programa debe responder en menos de n ciclos de reloj. Se utilizan principalmente para sistemas de misión crítica, como controles de vehículos o señalización. Estos lenguajes ofrecen garantías sólidas sobre cuánto tiempo tardará en ejecutarse un programa y cuánta memoria puede asignar.
Por supuesto, la contraparte de tales garantías sólidas es que no puede escribir programas cuyo consumo de memoria y tiempo de ejecución no pueda predecir con anticipación. En particular, no puede escribir un programa cuyo consumo de memoria o tiempo de ejecución depende de los datos de entrada.
Hay muchos lenguajes especializados que ni siquiera intentan ser lenguajes de programación, por lo que pueden permanecer cómodamente lejos de la completitud de Turing: expresiones regulares, lenguajes de datos, la mayoría de los lenguajes de marcado, ...

Por cierto, Douglas Hofstadter escribió varios libros de ciencia populares muy interesantes sobre cómputo, en particular Gödel, Escher, Bach: una trenza dorada eterna . No recuerdo si él explícitamente discute las limitaciones de Turing-incompletitud, pero leer sus libros definitivamente lo ayudará a entender más material técnico.

Como hay idiomas completos que no son de Turing, y dado que no estudié Comp Sci en la universidad, ¿alguien podría explicar algo que un lenguaje incompleto de Turing (como Coq ) no puede hacer?

¿O la completitud / incompletitud de ningún interés práctico real (es decir, no hace mucha diferencia en la práctica)?

EDITAR - Estoy buscando una respuesta en la línea de que no se puede construir una tabla hash en un lenguaje que no sea de Turing debido a X , ¡o algo así!

La respuesta más directa es: una máquina / idioma que no es Turing completo no se puede usar para implementar / simular máquinas de Turing. Esto proviene de la definición básica de completitud de Turing: una máquina / lenguaje está completamente completa si puede implementar / simular máquinas de Turing.

Entonces, ¿cuáles son las implicaciones prácticas? Bueno, hay una prueba de que todo lo que puede demostrarse que está completo puede resolver todos los problemas computables. Lo que significa, por definición, que todo lo que no está completo tiene la desventaja de que hay algunos problemas computables que no puede resolver. Cuáles son esos problemas depende de qué características faltan que completan el sistema no Turing.

Por ejemplo, si un idioma no admite el bucle o la recursividad o los bucles implícitos no pueden completarse porque las máquinas de Turing se pueden programar para que se ejecuten para siempre. En consecuencia, ese lenguaje no puede resolver problemas que requieren bucles.

Otro ejemplo es si un idioma no admite listas o matrices (o le permite emularlas, por ejemplo, usando el sistema de archivos), entonces no puede implementar una máquina Turing porque las máquinas Turing requieren acceso aleatorio arbitrario a la memoria. En consecuencia, ese lenguaje no puede resolver problemas que requieren un acceso aleatorio arbitrario a la memoria.

Por lo tanto, la característica que falta que clasifica un lenguaje para que no sea completo es exactamente lo que limita la utilidad del lenguaje. Entonces la respuesta es, depende: ¿qué hace que el lenguaje no Turing esté completo?

No puede escribir una función que simule una máquina de Turing. Puede escribir una función que simule una máquina de Turing para 2^128 (o 2^2^2^2^128 pasos) e informa si la máquina de Turing aceptó, rechazó o ejecutó por más tiempo que el número permitido de pasos.

Dado que "en la práctica" se habrá ido antes de que su computadora pueda simular una máquina de Turing para 2^128 pasos, es justo decir que la incompletitud de Turing no hace mucha diferencia "en la práctica".

Una clase importante de problemas que no encajan bien en idiomas como Coq es aquellos cuya finalización es conjeturada o difícil de probar. Puedes encontrar muchos ejemplos en teoría de números, tal vez la más famosa es la conjetura de Collatz

function collatz(n) while n > 1 if n is odd then set n = 3n + 1 else set n = n / 2 endif endwhile

Esta limitación lleva a tener que expresar dichos problemas de una manera menos natural.