2 puntos por GN⁺ 2024-08-05 | 1 comentarios | Compartir por WhatsApp
  • La idea de que “si no es Turing-complete, entonces es seguro” no coincide con el significado matemático del término, y la no completitud de Turing en su mayoría es independiente de propiedades prácticas como terminación, determinismo o sandboxing
  • Un cálculo de una Máquina de Turing cuyo tiempo de ejecución esté acotado por una función recursiva primitiva respecto a la entrada puede reescribirse también como una función recursiva primitiva
  • Las funciones recursivas primitivas siempre terminan, pero también pueden construir funciones que crecen muy rápido, como 2^(2^N), así que garantizar terminación no significa automáticamente un tiempo de ejecución práctico
  • En la práctica, un programa que no se detiene y otro que termina dentro de decenas de miles de millones de años generan problemas muy parecidos, y hasta un lenguaje Turing-complete puede detenerse de forma forzada con un contador de pasos
  • La calidad de un lenguaje de configuración depende más de la determinación, una semántica clara, pureza, seguridad y sandboxing, control del tiempo de ejecución y simplicidad, que de si es o no Turing-complete

El malentendido central en la discusión sobre Turing-completeness

  • En internet, muchos programadores hablan de “no ser Turing-complete” como si fuera una ventaja o un requisito en ciertos dominios
  • Pero Turing completeness es un término técnico concreto que viene de las matemáticas, así que usarlo como sustituto de varias propiedades que quieren los desarrolladores termina diluyendo su significado
  • Las propiedades que realmente hacen falta son garantía de terminación, ejecución rápida, comportamiento determinista, sandboxing o un lenguaje de configuración simple, y casi todas son ortogonales a Turing completeness
  • Para entender esta diferencia, hace falta un resultado teórico sencillo sobre funciones recursivas primitivas (Primitive Recursive Functions, PRF)

Una Máquina de Turing suficientemente rápida puede convertirse a PRF

  • Incluso si un programa está escrito en un lenguaje Turing-complete, si se sabe que su tiempo de ejecución es más rápido que O(2^(2^N)), entonces el mismo algoritmo puede implementarse también en un lenguaje no Turing-complete
  • La mayoría de los problemas prácticos caen dentro del rango que termina más rápido que 2^(2^N)
  • Por eso, un lenguaje no Turing-complete no limita de forma significativa la capacidad de cálculo en la práctica, ni otorga automáticamente una capacidad especial para controlar el cómputo
  • Desde la perspectiva práctica, los siguientes dos programas generan casi el mismo problema
    • Un programa que no termina
    • Un programa que solo termina después de algo como mil millones de mil millones de pasos
  • Incluso en un lenguaje Turing-complete, si en la implementación se cuentan los pasos y se aborta con error al superar cierto límite, el problema de no terminación puede bloquearse de manera simple

FSM: siempre termina, pero su expresividad es limitada

  • Una Finite State Machine (FSM) es un reconocedor que recibe una cadena como entrada y devuelve “yes” o “no”
  • Una FSM está compuesta por un conjunto finito de estados, un estado inicial, un conjunto de estados yes y una función de transición
  • Tras aplicar repetidamente la función de transición a cada símbolo de la entrada, el resultado queda determinado según si el estado final pertenece o no al conjunto de estados yes
  • La expresividad de una FSM es equivalente a la de una expresión regular (regular expression)
  • Una FSM funciona en tiempo lineal respecto al largo de la entrada y siempre termina, pero no puede reconocer cualquier conjunto de cadenas
    • Por ejemplo, no puede reconocer el conjunto de cadenas como 1, 010, 00100, 0001000, donde hay la misma cantidad de 0 a ambos lados del 1
    • En entradas lo suficientemente largas, los estados se repiten y aparece un ciclo; si se replica ese tramo cíclico, la FSM sigue llegando a un estado yes, pero la condición de la cadena ya se rompe

Máquina de Turing: un modelo que añade una cinta mutable a la FSM

  • Una Máquina de Turing (TM) tiene estados y una función de transición como una FSM, pero opera sobre una cinta mutable en vez de una entrada inmutable
  • En cada paso, la TM lee el símbolo actual de la cinta y realiza la siguiente operación
    • Reemplaza el símbolo actual por uno nuevo
    • Cambia su estado interno
    • Mueve la cabeza una posición a la izquierda o a la derecha
  • Cuando la TM llega a un estado halt, se detiene, y el contenido de la cinta en ese momento es el resultado
  • Mientras que una FSM es un reconocedor binario, una TM es un dispositivo que calcula funciones
  • Una TM no necesariamente se detiene; puede seguir yendo y viniendo por la cinta y cambiando de estado sin alcanzar nunca un estado final

Universal Turing Machine y capacidad de cómputo

  • El programa de una TM no se da como código de entrada del usuario, sino que está codificado directamente en la propia función de transición
  • Pero se puede codificar como archivo de texto una TM arbitraria junto con su entrada, y construir una TM “intérprete” que lo ejecute
  • Esa TM es una Universal Turing Machine, y simula otra TM recibida como entrada
  • Se puede construir un intérprete de TM en Python y, al revés, también un intérprete de Python en una TM, así que ambos pueden verse como equivalentes en capacidad de cómputo
  • Una FSM es más débil que una TM
    • Una TM puede simular una FSM
    • Una TM puede decidir mediante manipulación de cinta si una cadena tiene la misma cantidad de 0 a ambos lados de un 1 central
    • Una FSM no puede resolver ese mismo problema

La cinta puede verse como dos pilas

  • La cinta de una TM es una abstracción incómoda de implementar directamente en un lenguaje de programación general
  • La cinta y la posición de la cabeza pueden representarse con dos pilas
    • El contenido a la izquierda de la cabeza va en la pila izquierda
    • El contenido a la derecha de la cabeza va en la pila derecha, en orden invertido
  • Mover la cabeza a la izquierda o derecha se convierte en hacer pop de una pila y push en la otra
  • Por tanto, una TM tiene una capacidad de cómputo equivalente a una “FSM con dos pilas”
  • Si los símbolos de la pila son solo 0 y 1, la pila misma también puede representarse como un único número natural
    • ver tope: stack % 2
    • pop: stack / 2
    • push x: stack * 2 + x

Límites de la Máquina de Turing: Halting Problem y resultados tipo Rice

  • Como toda TM puede codificarse como texto, es posible enumerar las TM posibles en una lista infinita
  • Usando el argumento de diagonalización, puede demostrarse que existen funciones que una TM no puede calcular
  • Un ejemplo más concreto es el Halting Problem
    • Dado el código fuente de una TM y una entrada, consiste en decidir si esa TM se detendrá alguna vez
  • Si se supone que halts(program, input) siempre termina correctamente, aparece una contradicción con un programa weird que recibe su propio código fuente como entrada
    • Si decide que se detiene, entonces entra en un bucle infinito y no se detiene
    • Si decide que no se detiene, entonces termina de inmediato
  • Por tanto, halts en algunos casos debe equivocarse o no terminar
  • Más en general, para una TM arbitraria no puede decidirse algorítmicamente ninguna propiedad no trivial que preserve el comportamiento
    • Las propiedades sintácticas sí pueden verificarse, pero las propiedades de comportamiento que se conservan tras un refactor normalmente no pueden decidirse

Funciones recursivas primitivas: un modelo de cálculo que siempre termina

  • Una función recursiva primitiva (PRF) se define como una función que recibe una tupla de números naturales y devuelve un único número natural
  • Las funciones básicas son zero y succ
    • zero = 0
    • succ(x) = x + 1
  • Mediante composición de funciones pueden construirse constantes
    • succ(zero) = 1
    • succ(succ(zero)) = 2
  • No se permite recursión general, pero sí un bucle restringido con número de iteraciones fijado de antemano: LOOP(init, f, n)
    • LOOP(init, f, 0) = init
    • LOOP(init, f, 1) = f(init)
    • LOOP(init, f, 2) = f(f(init))
  • La restricción clave es que el número de iteraciones n queda fijado antes de empezar el bucle, y el cuerpo del bucle no puede modificar el contador

Construir componentes básicos de programación con PRF

  • La suma puede definirse como add(x, y) = LOOP(x, succ, y)
  • La multiplicación puede definirse como mul(x, y) = LOOP(0, add x, y)
  • La exponenciación puede definirse como pow(x, y) = LOOP(1, mul x, y)
  • A partir de eso también pueden construirse funciones de crecimiento rápido
    • pow_2(n) = pow(2, n)
    • pow_2_2(n) = pow_2(pow_2(n))
  • Si se añade pred a las funciones básicas, pueden construirse resta saturada y operaciones booleanas
    • sub(x, y) = LOOP(x, pred, y)
    • and(x, y) = mul(x, y)
    • not(x) = sub(1, x)
    • if(cond, a, b) también puede expresarse como fórmula aritmética
  • También pueden implementarse comparaciones, residuo y división usando iteraciones acotadas y condicionales

Estructuras de datos en PRF y simulación de TM

  • PRF puede recibir varios argumentos, pero su resultado es un único número natural, así que las estructuras de datos deben codificarse como números naturales
  • El par (a, b) puede representarse como 2^a * 3^b
  • Para extraer los componentes, basta con encontrar el exponente máximo de un primo dado
    • fst(p) es el mayor exponente de 2 que divide a p
    • snd(p) es el mayor exponente de 3 que divide a p
  • Del mismo modo, tres valores (S, stack1, stack2) pueden empaquetarse dentro de un solo número natural
  • La configuración de una TM puede representarse con los siguientes tres elementos
    • El estado actual S
    • La pila izquierda de la cinta
    • La pila derecha de la cinta
  • Como las operaciones sobre pilas pueden implementarse con residuo, multiplicación y división, un solo paso de una TM puede codificarse como PRF
  • Usando LOOP(initial_config, single_step, n), una TM puede simularse exactamente durante n pasos
  • El problema es que no siempre se conoce un n suficiente, pero si el tiempo de ejecución está acotado por alguna PRF, entonces puede hacerse repetir exactamente esa cantidad
  • En última instancia, todo cálculo de TM cuyo tiempo de ejecución esté acotado por una función recursiva primitiva puede reemplazarse por una PRF

Límites de las PRF: aunque siempre terminan, no son tan fuertes como una TM

  • Las PRF siempre terminan, pero no expresan todas las funciones que sí terminan
  • Existen funciones calculables por una TM que no pueden calcularse con PRF
  • Para demostrarlo, se establece una cota superior de crecimiento basada en la profundidad del árbol sintáctico de una PRF
  • Puede fijarse una cota tal que ninguna PRF de profundidad d o menor crezca más rápido que cierta función unaria A_d
  • A(d, x) se define así
    • A(1, x) = x + 1
    • A(d + 1, 0) = A(d, A(d, 0))
    • A(d + 1, x) = A(d, A(d + 1, x - 1))
  • Esta definición termina cuando se calcula en una TM porque en cada llamada recursiva (d, x) disminuye en orden lexicográfico
  • a(x) = A(x, x) crece más rápido que cualquier PRF; puede calcularse con una TM, pero no con una PRF

De vuelta a la práctica: la no completitud de Turing por sí sola no alcanza

  • Una Máquina de Turing puede no detenerse
  • Incluso modelos que siempre terminan, como FSM y PRF, no garantizan por eso una finalización rápida
  • Las PRF pueden calcular funciones enormes como 2^(2^N), así que garantizar terminación no garantiza un tiempo de ejecución práctico
  • Muchos algoritmos reales tienen tiempo de ejecución acotado por una PRF, así que también pueden expresarse con modelos no Turing-complete
  • El método general para hacer que un cálculo Turing-complete se comporte como una PRF es añadir un contador de iteraciones y forzar la detención cuando el contador crece demasiado

Las propiedades que de verdad hacen falta en un lenguaje de configuración

  • A menudo un lenguaje de configuración presenta como meta de diseño el hecho de ser “no Turing-complete”, pero en realidad hacen falta varias propiedades más fuertes
  • Determinismo

    • Un lenguaje de configuración debe ser determinista
    • Un comportamiento como id([]) de Python, que puede devolver valores distintos en cada ejecución, puede tolerarse en programación general, pero no sirve para configuración
    • La configuración suele usarse como clave de sistemas de caché o de builds incrementales, y la no determinación vuelve inestable el comportamiento de la caché
  • Semántica clara

    • El comportamiento del lenguaje debe quedar fijado con claridad mediante una referencia consultable
    • Se puede volver determinista id([]) de Python desactivando ASLR y usando un allocator específico, pero eso no garantiza que el resultado sea predecible ni igual entre implementaciones
    • Para garantizar el mismo comportamiento entre distintas implementaciones o cambios de versión de Python, hace falta una semántica bien definida
  • Pureza

    • Si la configuración puede leer variables de entorno o archivos en disco, entonces su significado depende del entorno de evaluación
    • Para que la caché funcione bien, el lenguaje de configuración debe tener pureza
  • Seguridad y sandboxing

    • Tanto la pureza como la seguridad pueden lograrse evitando exponer IO general
    • Pero ambas propiedades persiguen objetivos distintos
    • La pureza busca evitar que el resultado se vuelva no determinista
    • La seguridad busca no exponer al atacante recursos como tokens de acceso
  • Control del tiempo de ejecución

    • Aunque se controle el IO, una configuración maliciosa todavía puede hacer un ataque de denegación de servicio consumiendo CPU
    • Para garantizar el tiempo de ejecución pueden usarse dos enfoques
    • Restringir la estructura para que el procesamiento sea una forma obviamente lineal y proporcional al tamaño de la entrada
    • Usar ejecución medida (metered execution), decrementando un contador en cada paso atómico y deteniendo el proceso cuando el contador llega a 0
  • Simplicidad

    • Un lenguaje de configuración debe guiar a los usuarios a escribir programas simples
    • Prohibir recursión y bucles infinitos puede servir como tope de velocidad que empuje hacia la simplicidad
    • Pero, como muestra el ejemplo de PRF, esa prohibición no impide por completo escribir programas recursivos arbitrarios; solo obliga a hacerlo de forma más indirecta
    • Como ejemplo relacionado, puede verse some roundabout code

Resumen final

  • Un algoritmo de Máquina de Turing cuyo tiempo de ejecución sobre la entrada esté acotado por alguna función recursiva primitiva también puede implementarse como una función recursiva primitiva
  • La no completitud de Turing puede dar una sola propiedad, la garantía de terminación, pero no garantiza automáticamente los límites de tiempo de ejecución ni la calidad de un lenguaje de configuración en la práctica
  • En el diseño de lenguajes de configuración, lo importante no es tanto Turing completeness en sí, sino el determinismo, una semántica clara, pureza, sandboxing, medición del tiempo de ejecución y simplicidad

1 comentarios

 
GN⁺ 2024-08-05
Opiniones de Hacker News
  • Autopromoción: https://www.nayuki.io/page/primitive-recursive-functions

    • Es mucho mejor que el artículo original, pero hoy en día parece que todos prefieren más las explicaciones sencillas estilo ELI5
  • En la conclusión del artículo hay criterios bastante buenos relacionados con los lenguajes de configuración, y me pregunto si entre los lenguajes actuales hay alguno que cumpla todos o la mayoría de esos criterios

    • Ejemplos que cumplen esos criterios son Dhall [1] y Cue [2], aunque en cierto sentido no son ejemplos interesantes
      Dhall es intencionalmente un lenguaje funcional total, así que va por el lado de “no ser Turing completo”, y Cue no tiene funciones, así que tampoco hay nada que pueda ser recursivo
      Creo que RCL [3] cumple los criterios. Es determinista y puro, ofrece ejecución medida y trata el acceso al sistema de archivos dentro de un sandbox. Si la política del sandbox lo permite, puede leer archivos, pero esos archivos se consideran parte del código fuente y se comportan igual que un import
      En RCL no quise ir por el camino de “no ser Turing completo” por las razones que menciona el autor. Que un programa finalmente termine no es una propiedad muy útil en la práctica y, a la inversa, incluso en lenguajes funcionales totales como Agda se pueden escribir programas muy complejos, así que no ser Turing completo no garantiza programas/configuraciones simples
      En RCL todos los bucles tienen límites, pero como hay funciones, también es posible la recursión. No hay llamadas de cola, así que al principio puse un límite de profundidad de recursión para evitar desbordamientos de la pila nativa, pero el fuzzer encontró una función que se ejecuta con espacio de pila constante y aun así se detiene, y todavía no la entiendo del todo: let f = g => g(g(h => k => g(g(h)))); f(f)
      Al final, que se puedan expresar funciones patológicas como esa no es un problema en la práctica. Basta con poner un límite al número de pasos de ejecución, es decir, un “límite de gas” o la “ejecución medida” de la que habla el autor. Para mantener el código simple, ayuda que las estructuras de iteración incorporadas tengan límites y que la recursión sea incómoda, pero al final las herramientas más valiosas son la revisión de código y el buen criterio
      [1]: https://dhall-lang.org/
      [2]: https://cuelang.org/
      [3]: https://rcl-lang.org/
    • Aunque es imperativo y tampoco es “puro”, incluso C fue diseñado con la intención de que antes de entrar en cualquier bucle se pudiera conocer una cota superior del número de iteraciones, y por eso es primitivamente recursivo
      La investigación de Dennis Ritchie en el MIT se enfocó en lo que él llamaba programación de bucles
      The complexity of loop programs - ALBERT R. MEYER and DENNIS M. RITCHIE
      https://people.csail.mit.edu/meyer/meyer-ritchie.pdf
      La programación estructurada, que casi todos los programadores modernos siguen por defecto, es en la práctica un paradigma que empuja hacia las funciones recursivas primitivas. Como la programación estructurada fue aceptada casi universalmente frente a otros dos tipos, como pop y la programación funcional, parece que se malinterpreta el artículo de Dijkstra “goto considered harmful”
      Las funciones recursivas primitivas no abarcan todas las funciones computables, pero sí casi todas las funciones intuitivas cuya terminación está garantizada. Por supuesto, hay casos en los que realmente se necesitan bucles cuyo número de iteraciones no se conoce al entrar, pero si se usan solo cuando son estrictamente necesarios, son una forma evitable de pegarse un tiro en el pie
      Incluso COBOL se modernizó moviendo los goto ilimitados al comando ALTER. No se me ocurre ningún lenguaje moderno y útil que no permita funciones PR
      Incluso en C, si se evita while y se evita explícitamente el fall through, casi siempre se puede escribir código de funciones totales que necesariamente termina
      También hay casos patológicos, como la inferencia de tipos de ML. Su costo real es mucho más barato de lo que sugeriría su clase de complejidad, así que aunque el lenguaje no sea total y sea difícil restringir ese uso, vale la pena aceptarlo
      En términos prácticos, todos los lenguajes en general ofrecen valores por defecto que soportan la mayoría de estos criterios, pero imponer esas restricciones limitaría seriamente la utilidad del lenguaje. Incluso diría que los criticados frameworks SOLID y Clean empujan hacia este modelo
      La programación estructurada se volvió tan universal que es fácil olvidar esto, e incluso dejar de enseñarlo. Como viejo barbón, recuerdo haber aprendido los peligros de WHILE y cosas similares
    • Creo que se podría elegir Dhall y ver en qué criterio falla. Parece lo más cercano
  • Decir que corre más rápido que O(2^(2^N)) probablemente sea una simplificación, pero la parte de “un número muy grande” le resta un poco de credibilidad
    Para ser precisos, habría que decir “una función que crece muy rápido”. O parece querer decir que el programa termina en menos de O(2^(2^N)) pasos

  • Si uno mira solo la primera parte, donde dice que un lenguaje restringido es mejor para algunas aplicaciones, me parece que la ventaja es que se puede calcular estáticamente una cota superior de la cantidad de pasos necesarios.
    Entonces se podría rechazar cualquier cálculo que viole el límite para cualquier entrada y devolver un error significativo.
    En cambio, al imponer límites en tiempo de ejecución a un lenguaje Turing completo, podrías fijar un límite demasiado bajo para algunas entradas que sí te interesan. No lo sabes hasta ejecutarlo y topar con el límite. A veces veo esto con la recursión de plantillas en C++.
    Puede que esté totalmente confundido, así que me gustaría que alguien que sepa más lo explique.

    • Después de que un excompañero puso un número cercano al triple y, años después, una carga de trabajo real chocó contra ese límite, yo uso un límite de 10 veces la cantidad razonable de cómputo.
      Aunque un flujo de trabajo malo tarde varias veces más en fallar, sigue siendo del orden de milisegundos, así que no veo mucho daño.
      Normalmente uno se encuentra con este problema cuando alguien trató el dominio del problema como un grafo dirigido acíclico, pero no logró imponer lo de “acíclico”. Modelar un problema como un grafo dirigido acíclico es como Dark Galadriel pensando si aceptar el anillo de Frodo. “Todos me amarán y desesperarán”. Quienes construyen estas cosas siempre se sienten mucho más orgullosos de lo que sería razonable.
      Al final, los clientes arrastrados hacia soluciones caras y complejas se quedan sin dinero, y sus problemas empiezan a verse mucho más pequeños. Entonces, literalmente, solo queda una app cuyo costo por trabajo no puede bajar lo suficiente como para sostener el negocio del cliente.
    • Predecir con exactitud el uso de combustible de un cálculo en blockchain puede ser interesante para otros, pero no para mí.
      A mí me interesa más como otro martillo en la caja de herramientas para atrapar bugs que pasaron los martillos anteriores, como verificación estática de tipos, ausencia de null y ausencia de mutación.
      El hecho de que termine en tiempo finito no demuestra su corrección, pero si yo declaro que el código termina en tiempo finito y el compilador no está de acuerdo, creeré que ese código está mal.
    • Una cota determinada estáticamente puede sobreestimar mucho la complejidad real de tiempo de ejecución en los casos comunes. Esto se debe a que, en general, no se puede predecir cómo se evaluarán las condiciones que provocan terminación anticipada en la recursión.
      Para que la terminación anticipada afecte el tiempo de ejecución habría que asumir evaluación diferida o condiciones con cortocircuito, pero un lenguaje práctico normalmente tendrá eso.
    • ¿Qué pasa si esa cota es extremadamente laxa? Por ejemplo, quicksort determinista suele ser n log n, pero tiene una cota cuadrática respecto del tamaño de la entrada.
      ¿Entonces vas a rechazar el cálculo de quicksort? Más extremo aún: el algoritmo de Hindley–Milner tiene una cota exponencial de tiempo, pero en la práctica muchas veces corre en tiempo lineal.
    • No sé si se “calcula estáticamente”, pero veo que la única ventaja de restringir mucho la capacidad del lenguaje es poder poner límites de cómputo que no dependan de los datos.
      Dicho eso, me cuesta pensar en una situación en la que eso sea un requisito realmente fuerte. ¿Cuántos sistemas no pueden emitir un error de “la consulta tardó demasiado”?
  • Quería probar un lenguaje de programación web backend basado en el principio de no terminación/acotamiento.
    La idea es que el compilador demuestre que toda función, para un estado e argumentos dados, se ejecuta dentro de un límite, y que pueda mostrar que X es la cota inferior e Y la cota superior. Esa información se propaga hasta el punto de entrada.
    Coincido con el autor en que se necesitan semánticas más fuertes, y por eso pensé en este lenguaje. Muchas veces uno quiere garantías sobre el tiempo de ejecución del programa.
    La base serían funciones recursivas primitivas, pero en la práctica podría ser Turing completo. Así como Rust rechaza préstamos incorrectos pero ofrece unsafe para punteros primitivos, este lenguaje calcularía cotas a partir de primitivas simples de iteración, o permitiría usar un operador unsafe y proporcionar una fórmula alternativa para los límites.

  • No entiendo bien la breve queja/motivación del artículo.
    Me refiero a la parte que dice: “Normalmente, en ciertos ámbitos, no ser Turing completo se elogia como una ventaja o un requisito. Creo que la mayoría de esas discusiones están equivocadas: no ser Turing completo no significa lo que la gente espera”.
    ¿Por qué esas discusiones están equivocadas? La mayoría de las herramientas de análisis formal, como Coq, Isabelle y Agda, normalmente exigen una prueba de que una función termina. Eso equivale a demostrar que la función es total y, por lo tanto, ¿no significa que es recursiva primitiva?

    • No leí hasta el final, pero este artículo parece venir de que algunos lenguajes de configuración promocionan “no ser Turing completos” como una funcionalidad. Cuando en realidad la funcionalidad que quieren promocionar probablemente sea un tiempo de ejecución razonablemente acotado.
      También salió en una discusión reciente sobre CEL:
      https://news.ycombinator.com/item?id=40954652
    • Si estás hablando de pruebas formales, no de contraejemplos científicos usados en la programación moderna, demostrar que una función es total en el caso general es un problema de búsqueda NP-completo.
      Si no recuerdo mal, eso equivale a NP con un oráculo co-NP, o al segundo nivel de la jerarquía polinómica. Incluso si es posible en problemas pequeños, es caro.
      Estas herramientas funcionan mejor cuando estructuras el programa para que sea una función total. La forma más común de hacerlo es usar solo FOR en programación estructurada, o WHILE/recursión con un número de iteraciones limitado.
      Aunque solo se relaciona con SAT, las formas tratables que cubre el teorema de dicotomía de Schaefer son el lente más accesible que se me ocurre.
    • Como muestra el artículo, hay funciones que terminan pero no son recursivas primitivas, así que una prueba de totalidad no implica que sean recursivas primitivas.
      Agda, y probablemente otras herramientas también, pueden demostrar terminación para algunas funciones recursivas no primitivas que terminan. Por supuesto, no pueden hacerlo para todas.
      El malentendido del que se queja el artículo parece ser, a grandes rasgos: “Turing-completitud significa poder hacer cómputo, y no ser Turing completo significa no poder computar y tener buenas propiedades para un lenguaje de configuración”.
      El punto del artículo es que, aun sin ser Turing completo, se pueden hacer muchas cosas costosas o complicadas, y que un lenguaje de configuración necesita restricciones mucho más estrictas que simplemente no ser Turing completo.
    • Puede haber más formas de no ser Turing completo además de ser una función total que termina limpiamente. Por ejemplo, un bucle infinito no puede realizar cómputo universal y tampoco termina.
  • Soy desarrollador de CUE. CUE es recursivo primitivo y también cumple con los criterios que uno esperaría de un “buen” lenguaje de configuración.