tutorial - Haciendo explícito el "éxito determinista" de los objetivos de Prolog.

prolog tutorial

Question

La cuestión del éxito determinista de algún objetivo de Prolog ha aparecido una y otra vez en, al menos, las siguientes preguntas:

• Reificación del término igualdad / desigualdad
• Intersección y unión de 2 listas.
• Eliminar duplicados en la lista (Prolog)
• Prólogo: ¿Cómo puedo implementar la suma de cuadrados de dos números más grandes de cada tres?
• Ordenar listas con programación de lógica de restricción )

Se utilizaron diferentes métodos (p. Ej., Provocando ciertos errores de recursos, o mirando de cerca las respuestas exactas dadas por el nivel de Prolog), pero todos me parecen un tanto piratas.

Estoy buscando una forma genérica, portátil y conforme con ISO para averiguar si la ejecución de algún objetivo Prolog (que tuvo éxito) dejó atrás algunos puntos de elección. ¿Algún predicado meta, tal vez?

¿Podría por favor insinuarme en la dirección correcta? ¡Gracias de antemano!

Answer 1

No hay garantía en setup_call_cleanup / 3 de que detecte determinismo, es decir, que falten puntos de elección en el éxito de un objetivo. La propuesta de borrador de la Descripción 7.8.11.1 solo dice:

c) El controlador de limpieza se llama exactamente una vez; no mas tarde que
Al fracaso de G. Momentos anteriores son:
Si G es verdadero o falso, se llama a C en una implementación
Momento dependiente después de la última solución y después de la última.
efecto observable de G.

Así que actualmente no hay ningún requisito que:

setup_call_cleanup(true, true, Det=true)

Devuelve Det = true en primer lugar. Esto también se refleja en los casos de prueba 7.8.11.4 Ejemplos que da la propuesta de borrador, encontramos un caso de prueba que dice:

setup_call_cleanup(true, true, X = 2).
Either: Succeeds, unifying X = 2.
Or: Succeeds.

Entonces es tanto una implementación válida, para detectar determinismo y no para detectar determinismo.

Answer 2

Buenas noticias para todos: setup_call_cleanup/3 (actualmente un borrador de propuesta para ISO) le permite hacerlo de una manera bastante portátil y hermosa.

Vea el example :

setup_call_cleanup(true, (X=1;X=2), Det=yes)

tiene éxito con Det == yes cuando no quedan más puntos de elección.

EDITAR : Permítame ilustrar la genialidad de este constructo, o más bien del predicado muy cercano call_cleanup/2 , con un ejemplo simple:

En la excelente documentación CLP (B) de SICStus Prolog , encontramos en la descripción de labeling/1 una garantía muy sólida:

Enumera todas las soluciones por retroceso, pero crea puntos de elección solo si es necesario .

Esto es realmente una garantía sólida, y al principio puede ser difícil creer que siempre se cumple. Por suerte para nosotros, es extremadamente fácil formular y generar casos de prueba sistemáticos en Prolog para verificar dichas propiedades, en esencia usando el sistema Prolog para probarse a sí mismo.

Comenzamos con la descripción sistemática de cómo se ve una expresión booleana en CLP (B):

:- use_module(library(clpb)).
:- use_module(library(lists)).

sat(_) --> [].
sat(a) --> [].
sat(~_) --> [].
sat(X+Y) --> [_], sat(X), sat(Y).
sat(X#Y) --> [_], sat(X), sat(Y).

De hecho, hay muchos más casos, pero por ahora nos limitamos al subconjunto anterior de expresiones CLP (B).

¿Por qué estoy usando un DCG para esto? Porque me permite describir convenientemente (un subconjunto de) todas las expresiones booleanas de profundidad específica y, por lo tanto, enumerarlas todas. Por ejemplo:

?- length(Ls, _), phrase(sat(Sat), Ls). Ls = [] ; Ls = [], Sat = a ; Ls = [], Sat = ~_G475 ; Ls = [_G475], Sat = _G478+_G479 .

Por lo tanto, estoy usando el DCG solo para indicar cuántas "fichas" disponibles ya se han consumido al generar expresiones, lo que limita la profundidad total de las expresiones resultantes.

A continuación, necesitamos un pequeño predicado auxiliar labeling_nondet/1 , que actúa exactamente como labeling/1 , pero solo es cierto si aún queda un punto de elección. Aquí es donde call_cleanup/2 :

labeling_nondet(Vs) :-
        dif(Det, true),
        call_cleanup(labeling(Vs), Det=true).

Nuestro caso de prueba (y con esto, en realidad nos referimos a una secuencia infinita de casos de prueba pequeños, que podemos describir muy convenientemente con Prolog) ahora tiene como objetivo verificar la propiedad anterior, es decir:

Si hay un punto de elección, entonces hay una solución adicional.

En otras palabras:

El conjunto de soluciones de labeling_nondet/1 es un subconjunto adecuado del de labeling/1 .

Describamos cómo se ve un contraejemplo de la propiedad anterior:

counterexample(Sat) :- length(Ls, _), phrase(sat(Sat), Ls), term_variables(Sat, Vs), sat(Sat), setof(Vs, labeling_nondet(Vs), Sols), setof(Vs, labeling(Vs), Sols).

Y ahora usamos esta especificación ejecutable para encontrar ese contraejemplo. Si el solucionador funciona como se documenta, nunca encontraremos un contraejemplo. Pero en este caso, inmediatamente obtenemos:

| ?- counterexample(Sat). Sat = a+ ~_A, sat(_A=:=_B*a) ? ;

Así que, de hecho, la propiedad no se mantiene. Desglosado a la esencia, aunque no quedan más soluciones en la siguiente consulta, Det no está unificado con true :

| ?- sat(a + ~X), call_cleanup(labeling([X]), Det=true).
X = 0 ? ;
no

En SWI-Prolog, el punto de elección superfluo es obvio:

?- sat(a + ~X), labeling([X]). X = 0 ; false.

No estoy dando este ejemplo para criticar el comportamiento de SICStus Prolog o SWI: a nadie realmente le importa si queda un punto de elección superfluo en el labeling/1 , y menos en un ejemplo artificial que involucra variables cuantificadas universalmente (que es atípico para tareas en las que se utiliza labeling/1 ).

Estoy dando este ejemplo para mostrar cómo se pueden probar las garantías de forma amable y conveniente que se documentan y pretenden con tan poderosos predicados de inspección ...

... asumiendo que los implementadores están interesados ​​en estandarizar sus esfuerzos, ¡de modo que estos predicados realmente funcionen de la misma manera en diferentes implementaciones! El atento lector habrá notado que la búsqueda de contraejemplos produce resultados bastante diferentes cuando se usa en SWI-Prolog.

En un giro inesperado de eventos, el caso de prueba anterior ha encontrado una discrepancia en las implementaciones de call_cleanup/2 de SWI-Prolog y SICStus. En SWI-Prolog (7.3.11):

?- dif(Det, true), call_cleanup(true, Det=true). dif(Det, true). ?- call_cleanup(true, Det=true), dif(Det, true). false.

mientras que ambas consultas fallan en SICStus Prolog (4.3.2).

Este es el caso bastante típico: una vez que esté interesado en probar una propiedad específica, encontrará muchos obstáculos que impiden probar la propiedad real.

En el proyecto de propuesta de la ISO, vemos:

El fallo de [el objetivo de limpieza] se ignora .

En la documentación de call_cleanup/2 de call_cleanup/2 , vemos:

La limpieza se realiza con éxito después de realizar algún efecto secundario; de lo contrario, puede producirse un comportamiento inesperado .

Y en la example , vemos:

El éxito o el fracaso de la limpieza se ignora

Por lo tanto, para la portabilidad, deberíamos escribir labeling_nondet/1 como:

labeling_nondet(Vs) :-
        call_cleanup(labeling(Vs), Det=true),
        dif(Det, true).