Explicitar el "éxito determinista" de los objetivos de Prolog

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

Ver el ejemplo:

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

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

EDIT : Permítanme ilustrar la genialidad de esta construcción, o más bien del predicado muy estrechamente relacionado call_cleanup/2, con un simple ejemplo:

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

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

Esto es realmente una garantía fuerte, y al principio puede ser difícil de creer que siempre se mantiene. Afortunadamente para nosotros, es extremadamente fácil formular y generar casos de prueba sistemáticos en Prolog para verificar tales propiedades, en esencia utilizando el sistema Prolog para pruébese a sí mismo.

Comenzamos describiendo sistemáticamente 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 limitémonos al subconjunto anterior de expresiones CLP(B) por ahora.

¿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 .

Así, yo soy usar el DCG solo para indicar cuántos "tokens" disponibles ya se han consumido al generar expresiones, limitando 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 un punto de elección todavía permanece. Aquí es donde call_cleanup/2 entra:

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 muy convenientemente describir 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 de labeling/1.

Describamos así 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 tal contraejemplo. Si el solucionador funciona como está documentado, entonces 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 retener. 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: {[28]]}

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

Estoy no dando este ejemplo para criticar el comportamiento de cualquiera SICStus Prolog o SWI: A nadie le importa realmente si se deja o no un punto de elección superfluo en labeling/1, menos aún en un ejemplo artificial que involucra variables universalmente cuantificadas (lo cual es atípico para tareas en las que se usa labeling/1).

I am dando este ejemplo para mostrar cuán agradable y convenientemente las garantías que están documentadas y previstas pueden ser probadas con predicados de inspección tan poderosos...

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

En un giro inesperado de los acontecimientos, el caso de prueba anterior ha encontrado una discrepancia en las implementaciones 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, encuentra muchos obstáculos que están en el camino de probar la propiedad real.

En el proyecto de propuesta de la ISO , vemos:

El fracaso de [el objetivo de limpieza] es ignorado.

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

La limpieza tiene éxito determinadamente después de realizar algún efecto secundario; de lo contrario, puede resultar un comportamiento inesperado.

Y en la variante SWI , vemos:

El éxito o el fracaso de la limpieza es ignorado

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).