¿Cuáles son las limitaciones prácticas de un lenguaje completo no turing como Coq?

Primero, asumo que ya has oído hablar de la tesis de Church-Turing, que establece que cualquier cosa que llamemos "computación" es algo que se puede hacer con una máquina de Turing (o cualquiera de los muchos otros modelos equivalentes). Así que un lenguaje Turing-completo es uno en el que cualquier cálculo puede ser expresado. Por el contrario, un lenguaje Turing-incompleto es aquel en el que hay algún cálculo que no se puede expresar.

Ok, eso no fue muy informativo. Permítanme dar un ejemplo. Hay una cosa que no puede hacer en ningún lenguaje Turing-incomplete: no puede escribir un simulador de máquina de Turing (de lo contrario, podría codificar cualquier cálculo en la máquina de Turing simulada).

Ok, eso aún así no fue muy informativo. la verdadera pregunta es, ¿qué programa útil no puede ser escrito en un lenguaje Turing-incompleto? Bueno, a nadie se le ha ocurrido una definición de "programa útil" que incluya todos los programas que alguien en algún lugar ha escrito para un propósito útil, y eso no incluye todos los cálculos de la máquina de Turing. Por lo tanto, diseñar un lenguaje Turing incompleto en el que se puedan 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 por ahí, y difieren en lo que no pueden hacer. Sin embargo, hay un tema común. Si está diseñando un lenguaje, hay dos formas principales de asegurarse de que el lenguaje sea Turing-completo:

• Requieren que el el lenguaje tiene bucles arbitrarios (while) y asignación de memoria dinámica(malloc)

• Requiere que el lenguaje soporte funciones recursivas arbitrarias

Echemos un vistazo a algunos ejemplos de lenguajes completos que no son de Turing y que algunas personas podrían llamar lenguajes de programación.

• Las primeras versiones de FORTRAN no tenían asignación de memoria dinámica. Tenías que averiguar de antemano cuánta memoria necesitaría tu cálculo y asignarla. A pesar de eso, FORTRAN fue una vez el lenguaje de programación más utilizado.

  La limitación práctica obvia es que usted tiene que 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 era a menudo 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 demostrando teoremas. Ahora probar teoremas y ejecutar programas están muy estrechamente relacionados, por lo que puede escribir programas en Coq al igual que probar un teorema. Intuitivamente, una prueba del teorema "A implica B" es una función que toma una prueba del teorema como un argumento y devuelve una prueba del teorema B.

  Dado que el objetivo del sistema es probar teoremas, no puede dejar que el programador escriba funciones arbitrarias. Imagine que el lenguaje le permitió escribir una función recursiva tonta que acaba de llamarse a sí misma (elija la línea que utiliza 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 puede dejar que la existencia de tal función le convenza de que A implica B, o de lo contrario sería capaz de probar cualquier cosa y no solo verdaderos teoremas! Así que Coq (y probadores de teoremas similares) prohíben la recursión arbitraria. Cuando escribe una función recursiva, debe demostrar que siempre termina, de modo que cada vez que la ejecuta una prueba del teorema A usted sabe que construirá una prueba del teorema B.

  La limitación práctica inmediata de Coq es que no se pueden escribir funciones recursivas arbitrarias. Dado que el sistema debe ser capaz de rechazar todas las funciones no terminantes, la indecibilidad del problema de detención (o más generalmente teorema de Rice) asegura que hay funciones terminantes que también son rechazadas. Una dificultad práctica adicional es que usted tiene que ayudar al sistema a demostrar que su función termina.

  Hay mucha investigación en curso sobre cómo hacer que los sistemas de prueba sean más parecidos al lenguaje de programación sin comprometer su garantía de que si tienes una función de A a B, es tan bueno como una prueba matemática de que A implica B. Extender el sistema para aceptar más funciones terminantes es uno de los temas de investigación. Otras direcciones de extensión incluyen lidiar con preocupaciones del "mundo real" como entrada/salida y concurrencia. Otro desafío es hacer que estos sistemas sean accesibles a los meros mortales (o tal vez convencer a los meros mortales de que de hecho son accesibles).

• Los lenguajes de programación síncronos 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 idiomas ofrecen fuertes garantías sobre cuánto tiempo tardará un programa en ejecutarse y cuánta memoria puede asignar.

  Por supuesto, la contraparte de tales garantías fuertes es que no puede escribir programas cuyo consumo de memoria y tiempo de ejecución no puede predecir de antemano. En particular, no se 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 y por lo tanto pueden permanecer cómodamente lejos de la integridad de Turing: expresiones regulares, lenguajes de datos, la mayoría de lenguajes de marcado,...

Por cierto, Douglas Hofstadter escribió varios libros de ciencia popular muy interesantes sobre computación, en particularGödel, Escher, Bach: an Eternal Golden Braid . No recuerdo si él discute explícitamente las limitaciones de Turing-incompletitud, pero la lectura de sus libros definitivamente le ayudará a entender más material técnico.