Tengo una pregunta interesante, pero no estoy seguro exactamente cómo expresarlo ...¿Cómo encontrar la orden de procesamiento óptima?
Considere el cálculo lambda. Para una expresión dada de lambda, hay varias órdenes de reducción posibles. Pero algunos de ellos no terminan, mientras que otros lo hacen.
En el cálculo lambda, resulta que hay una orden de reducción particular que es garantizada para terminar siempre con una solución irreductible, si es que realmente existe. Se llama Orden normal.
He escrito un simple solucionador de lógica. Pero el problema es que el orden en que procesa las restricciones parece tener un gran efecto sobre si encuentra alguna solución o no. Básicamente, me pregunto si existe algo así como un orden normal para mi lenguaje de programación lógica. (O carnero que es imposible que una simple máquina para resolver este problema de forma determinista.)
Así que eso es lo que busco. Es de suponer que la respuesta depende críticamente de lo que es exactamente el "solucionador de lógica simple". Así que intentaré brevemente describirlo.
Mi programa se basa estrechamente en el sistema de combinadores en el capítulo 9 de La diversión de Programación (Jeremy Gibbons & Oege de Moor). El lenguaje tiene la siguiente estructura:
la entrada al solucionador es un solo predicado . Los predicados pueden involucrar variables. La salida del solucionador es cero o más soluciones. Una solución es un conjunto de asignaciones variables que hacen que el predicado se vuelva verdadero.
Variables hold expresiones. Una expresión es un número entero, un nombre de variable o una tupla de subexpresiones.
Hay un predicado de igualdad, que compara expresiones (no predicados) para la igualdad. Está satisfecho si la sustitución de cada variable (vinculada) por su valor hace que las dos expresiones sean idénticas. (En particular, cada variable se iguala a sí misma, unida o no). Este predicado se resuelve mediante la unificación.
También hay operadores para AND y OR, que funcionan de la manera obvia. No hay operador NO.
Existe un operador "exists", que crea esencialmente variables locales.
La facilidad para definir predicados con nombre habilita el bucle recursivo.
Una de las "cosas interesantes" sobre la programación lógica es que una vez que se escribe un predicado llamado, por lo general funciona fowards y hacia atrás (e incluso a veces de lado ). Ejemplo canónico: un predicado para concatenar dos listas también se puede usar para dividir una lista en todos los pares posibles.
Pero a veces ejecutar un predicado hacia atrás da como resultado una búsqueda infinita, a menos que reordene el orden de los términos. (Por ejemplo, intercambie el LHS y el RHS de un AND o un OR). Me pregunto si hay alguna manera automática de detectar el mejor orden para ejecutar los predicados, para asegurar la terminación inmediata en todos los casos donde el conjunto de soluciones es exacto finito.
¿Alguna sugerencia?
Probablemente le ayudará si usted pone algunos ejemplos de los programas en su idioma, y mostrar cómo las diferentes estrategias de reducción conducen a diferentes resultados –
@ n.m. Buena idea. Trataré de llegar a un ejemplo mínimo ... – MathematicalOrchid
Véase también [Aritmética de Presburger] (http://en.wikipedia.org/wiki/Presburger_arithmetic) en caso de que no lo haya visto antes - la validez es decidible , y permite y, o no, por completo, e inducción (aunque tal vez la inducción no sea tan poderosa como la recursión que describes). –