regex finite-automata turing-complete halting-problem

regex - ¿Lenguajes prácticos que no son Turing completos?



finite-automata turing-complete (8)

"eliminar la necesidad de memoria teóricamente infinita". -- bueno sí. Cualquier computadora física está limitada por la entropía del universo e, incluso antes de eso, por la velocidad de la luz (== velocidad máxima a la que se puede propagar la información).

Aún más fácil, en una computadora físicamente realizable, simplemente monitoree el consumo de recursos y ponga un límite en ello. (es decir, cuando la memoria o el consumo de tiempo> MY_LIMIT, mata el proceso).

Si lo que estás preguntando es una solución puramente matemática / teórica, ¿cómo defines el "propósito general"?

Casi todos los lenguajes de programación utilizados son Turing Complete , y aunque esto le permite al lenguaje representar cualquier algoritmo computable , también viene con su propio conjunto de problemas . Dado que todos los algoritmos que escribo están destinados a detenerse, me gustaría poder representarlos en un lenguaje que garantice que se detendrán.

Las expresiones regulares usadas para hacer coincidir cadenas y máquinas de estados finitos se usan cuando se lee , pero me pregunto si hay un lenguaje más amplio que no esté completo.

editar: debo aclarar que, por ''propósito general'', no necesariamente quiero poder escribir todos los algoritmos de detención en el lenguaje (no creo que ese lenguaje exista) pero sospecho que hay hilos comunes en detener las pruebas que pueden generalizarse para producir un lenguaje en el que se garantice que todos los algoritmos se detienen.

También hay otra forma de abordar este problema: eliminar la necesidad de una memoria teóricamente infinita. Una vez que limita la cantidad de memoria que tiene la máquina, la cantidad de estados en que se encuentra la máquina es finita y contable, y por lo tanto puede determinar si el algoritmo se detendrá (al no permitir que la máquina entre en un estado anterior )


Cualquier lenguaje no completo de Turing no sería muy útil como lenguaje de propósito general. Es posible que pueda encontrar algo que se anuncie a sí mismo como un lenguaje de propósito general sin ser completo, pero nunca he visto uno.


BlooP (abreviatura de B ounded loop ) es un lenguaje interesante que no es Turing completo. Es esencialmente un lenguaje completo de Turing, con una advertencia (mayor): cada ciclo debe contener un límite en el número de iteraciones. Los bucles infinitos no están permitidos. Como resultado, el problema de detención se puede resolver para los programas BlooP.


La caridad todavía no es completa, no es solo teórica, didácticamente interesante (teoría de categorías), sino que además puede resolver problemas prácticos (torres de Hanoi). Su fuerza es tan grande que puede expresar incluso la función de Ackermann .


No escuches a los detractores. Hay muy buenas razones para preferir un lenguaje completo que no sea Turing en algunos contextos, si desea garantizar la finalización o simplificar el código, por ejemplo, eliminando la posibilidad de errores en el tiempo de ejecución. A veces, simplemente ignorar cosas puede no ser suficiente.

El documento Total Functional Programming argumenta de forma más o menos persuasiva que, de hecho, casi siempre deberíamos preferir un lenguaje tan restringido porque las garantías del compilador son mucho más fuertes. Ser capaz de demostrar que un programa se detiene puede ser significativo en sí mismo, pero en realidad este es el producto del razonamiento mucho más fácil que ofrecen los lenguajes más simples. Como un componente en una jerarquía de lenguajes de capacidad variable, el rango de utilidad de los lenguajes no universales es bastante amplio.

Otro sistema que aborda este concepto de capas mucho más completamente es Hume . El Informe Hume ofrece una descripción completa del sistema y sus cinco capas de idiomas progresivamente más completos y progresivamente menos seguros.

Y, por último, no olvides a Charity . Es un poco abstracto, pero también es un enfoque muy interesante para un lenguaje de programación útil pero no universal, que se basa muy directamente en los conceptos de la teoría de categorías.


La forma correcta de hacerlo, en mi humilde opinión, es tener un lenguaje que esté completo, pero proporcionar un sistema para indicar la semántica susceptible de ser procesado por un verificador de pruebas.

Entonces, suponiendo que está escribiendo deliberadamente un programa de terminación, tiene en mente un buen argumento sobre por qué se detiene, y con este nuevo tipo de lenguaje debería poder expresar ese argumento y hacerlo probar.

Como un aparte en mi compilador de producción, tengo recurrencias que, de hecho, sé que NO se detendrán en ciertas entradas ... Utilizo un hack desagradable para detener esto: un contador con un límite "sensible". Para su información, el código real implica la monomorfización del código polimórfico y la expansión infinita ocurre cuando se usa la recursión polimórfica. Haskell capta esto, mi compilador para Felix no (es un error en el compilador que no sé cómo solucionarlo).

Siguiendo mi argumento general ... Me gustaría saber qué tipo de anotaciones servirían para el propósito declarado: tengo el control de un lenguaje y compilador, así que podría agregar fácilmente dicho soporte si supiera exactamente qué add :) He visto la adición de una cláusula "invariante" y "variante" para bucles para este propósito, aunque no creo que el lenguaje se extendiera a usar esa información como prueba de terminación (más bien verificó la invariante y la variante de tiempo de ejecución si mal no recuerdo).

Quizás eso merece otra pregunta ...


El problema no está en la máquina de Turing, sino en el "algoritmo". La razón por la cual no se puede predecir si un algoritmo se detendrá o no se debe a esto:

function confusion() { if( halts( confusion ) ) { while True: no-op } else return; }

Cualquier lenguaje que no puede hacer recursividad o bucles no sería realmente "de propósito general".

¡Las expresiones regulares y las máquinas de estados finitos son lo mismo! ¡Lexing y la coincidencia de cuerdas son lo mismo! La razón por la cual los FSM se detienen es porque nunca buclean; simplemente pasan la entrada char-by-char y salen.

EDITAR:

Para muchos algoritmos, es obvio si se detendrían o no.

por ejemplo:

function nonhalting() { while 1: no-op }

Esta función claramente nunca se detiene.

Y, esta función obviamente se detiene:

function simple_halting_function() { return 1; }

Entonces, la conclusión: PUEDE garantizar que su algoritmo se detiene, solo diseñe de modo que lo haga.

Si no está seguro de si el algoritmo se detendrá todo el tiempo; entonces probablemente no pueda implementarlo en ningún idioma que garantice la "detención".


Resulta que es bastante fácil de completar. Por ejemplo, solo necesitas las 8 instrucciones ala BrainF ** k , y más al punto que realmente solo necesitas una instrucción .

El corazón de estos lenguajes es un constructo de bucle, y tan pronto como tienes bucles sin límites tienes un problema de detención inherente. ¿Cuándo terminará el ciclo? Incluso en un lenguaje completo que no sea de Turing que admite bucles sin límites, es posible que aún tenga el problema de detención en la práctica .

Si desea que todos sus programas finalicen, entonces solo necesita escribir su código cuidadosamente. Un lenguaje específico puede ser más de su gusto y estilo, pero no creo que ningún lenguaje pueda garantizar absolutamente que el programa resultante se detendrá.