¿Hay idiomas casi completos de Turing?

El Asistente de pruebas Coq, que “proporciona un lenguaje formal para escribir definiciones matemáticas, algoritmos ejecutables y teoremas junto con un entorno para el desarrollo semi-interactivo de pruebas verificadas por máquina”. En Coq, hay una inducción bien fundada en lugar de recurrencia. Para escribir funciones autorreferenciales, el programador debe mostrar que la auto-llamada se basa en un argumento que cada vez es más pequeño. Debido a esto, todos los programas de Coq probablemente terminen.

Sin embargo, Coq sigue siendo bastante expresivo. Investigadores en Francia han utilizado Coq para verificar la corrección del compilador C CompCert, una de las hazañas más impresionantes de la verificación de software. ¡Este compilador nos ayuda a asegurarnos de que el software en los aviones franceses de Airbus no tenga errores inesperados! (Consulte Hacia una compilación de optimización verificada formalmente en el software de control de vuelo).

Un secreto a voces en ciencias de la computación es que todos los idiomas en los que programa no son Turing Complete.

La integridad de Turing permite la ejecución de cualquier algoritmo definible, dada una cantidad de almacenamiento arbitrariamente grande (algunos dicen infinito).

Por lo tanto, si bien su programa puede verse en una versión ideal platónica de C, Java, Python o cualquier otra cosa, que es Turing Complete, el lenguaje implementado tiene una restricción que impide que sea así en lo que generalmente se considera una manera trivial. Si su programa requiere billones de líneas de código, buena suerte para obtener un compilador para manejarlo, básicamente.

De manera similar, ocasionalmente tropezará con un lenguaje de secuencias de comandos patentado que solo ha contado (es decir, bucles similares) y sin subrutinas. Si no hay forma de “repetir hasta que se termine”, desaparece una enorme clase de algoritmos.

Además de restricciones artificiales como esa, vale la pena considerar que un curso de Teoría de la Computación lo guiará esencialmente a través de cuatro “niveles” de computación.

  • Un autómata de estado finito (máquina de estado) puede pasar de su estado actual a un conjunto finito de otros estados basándose en la prueba de una condición.
  • Un autómata pushdown (máquina de pila) es el mismo, excepto que agrega la parte superior de una pila a la decisión del siguiente estado, y la acción en cada estado puede incluir empujar o saltar desde dicha pila.
  • Un autómata con límites lineales convierte la pila en una cinta de longitud arbitraria / infinita, pero restringe la capacidad de escribir en alguna región específica.
  • Una máquina de Turing elimina la restricción de escritura.

Hay un par de otras máquinas intercaladas y es posible que haya visto un modelo similar con gramáticas regulares, sin contexto, sensibles al contexto y sin restricciones, que son equivalentes. Puede ver el conjunto completo en varios campos en una práctica tabla en la parte inferior de la página de Wikipedia del autómata Pushdown o cualquier página similar.

En general, si restringe un idioma de una manera no trivial (como poner un límite en el espacio de almacenamiento máximo), empujará el idioma a un modelo de nivel inferior.

Si. Existe toda una clase de lenguajes de programación llamados “lenguajes funcionales totales”, que a través de una serie de restricciones semánticas aseguran que solo se permitan los programas que terminen de manera demostrable. Debido a esto, el problema de detención no se aplica y estos idiomas no están completos. Ejemplos son Coq y Agda.

Puede hacer una cantidad notable en dichos lenguajes: casi cualquier problema práctico puede resolverse fuera de algunos algoritmos matemáticos o abstractos, aunque requiere un poco de desorden para mostrarle al compilador que se puede probar que su programa termina.

Sin embargo, todo el dominio de la programación funcional total es algo oscuro e intimidante, ya que la aplicación principal de estos lenguajes es crear pruebas en matemática constructiva, que es la matemática convencional como la programación funcional total es la programación normal. Tienen sistemas de tipos bastante complejos similares a Haskell, y no tienen un mejor soporte para la construcción de pruebas que para proyectos más prácticos como escribir un sitio web.

Un ejemplo es BlooP, que aparece en “Godel, Escher, Bach” de Douglas Hofstadter. Es muy similar a un lenguaje tradicional, excepto que debe declarar un límite superior en el número de iteraciones en cualquier bucle.

Es fácil ver que cualquier programa BlooP finalmente se detendrá, por lo que BlooP no está completo en Turing.

El subconjunto más utilizado de SQL no es Turing completo.

Pig Latin no está Turing completo.

Cualquier cosa con una cantidad limitada de memoria. El ensamblado es un ejemplo, ya que su espacio de direcciones suele ser parte de la definición del lenguaje.

El cálculo lambda simplemente escrito no está completo