swi - ¿Qué se entiende por "pureza lógica" en Prolog?

swi prolog e

Question

¿Qué se entiende por "pureza lógica" (en el contexto de la programación Prolog)? La información de la etiqueta de pureza lógica dice "programas que usan solo cláusulas de Horn" , pero entonces, ¿cómo calificarían los predicados como if_/3 , utilizando tanto como lo hace el corte, y los diversos meta-logical (¿cuál es la terminología adecuada? var/1 y tales) predicados, es decir, las cosas de bajo nivel.

Entiendo que logre algún efecto "puro", pero ¿qué significa esto, precisamente?

Para una ilustración más concreta, explique cómo califica if_/3 como lógicamente puro, visto en uso, por ejemplo, en esta respuesta .

Answer 1

Permítanos primero acostumbrarnos a una lectura declarativa de los programas lógicos.

Declarativamente, un programa Prolog declara lo que es verdad .

Por ejemplo

natural_number(0).
natural_number(s(X)) :-
        natural_number(X).

La primera cláusula dice: 0 es un número natural.

La segunda cláusula dice: Si X es un número natural, entonces s(X) es un número natural.

Consideremos ahora el efecto de los cambios en este programa. Por ejemplo, ¿qué cambia cuando cambiamos el orden de estas dos cláusulas?

natural_number(s(X)) :-
        natural_number(X).
natural_number(0).

Declarativamente, cambiar el orden de las cláusulas no cambia el significado previsto del programa de ninguna manera (la disyunción es conmutativa).

Operativamente , es decir, teniendo en cuenta la estrategia de ejecución real de Prolog, los diferentes órdenes de cláusulas a menudo hacen una diferencia significativa.

Sin embargo , se conserva una propiedad extremadamente agradable del código de Prolog puro, independientemente del orden de la cláusula elegida:

Si una consulta Q tiene éxito con respecto a una cláusula que ordena O1 , entonces Q no falla con un ordenamiento diferente de O2 .

Tenga en cuenta que no estoy diciendo que Q también siempre tenga éxito con un orden diferente: Esto se debe a que la consulta también puede generar un bucle o producir un error con diferentes ordenamientos.

Para dos consultas Q1 y Q2 , decimos que G1 es más general si incluye a G2 con respecto a la unificación sintáctica. Por ejemplo, la consulta ?- parent_child(P, C). es más general que la consulta ?- parent_child(0, s(0)). .

Ahora, con programas Prolog puros, otra propiedad extremadamente agradable tiene:

Si una consulta Q1 tiene éxito, entonces cada consulta general Q2 no falla .

Tenga en cuenta, una vez más, que Q2 puede bucle en lugar de tener éxito.

Considere ahora el caso de var/1 que menciona, y piense en el predicado relacionado nonvar/1 . Supongamos que tenemos:

my_pred(V) :-
        nonvar(V).

¿Cuándo se sostiene esto? Claramente, es válido si el argumento no es una variable.

Como era de esperar, obtenemos:

?- my_pred(a).
true.

Sin embargo, para la consulta más general ?- my_pred(X). , obtenemos:

?- my_pred(X).
false.

Tal predicado se llama no monótono , y no se puede tratar como una verdadera relación debido a esta propiedad: Esto se debe a que la respuesta false anterior lógicamente significa que no hay soluciones en absoluto , sin embargo, en el ejemplo inmediatamente anterior, vemos que hay es una solución. Entonces, ilógicamente, una consulta más específica , creada al agregar una restricción , hace que la consulta tenga éxito :

?- X = a, my_pred(X).
true.

Por lo tanto, el razonamiento sobre dichos predicados es extremadamente complicado, hasta el punto de que no es nada divertido programar con ellos. Hace imposible la depuración declarativa y es difícil establecer las propiedades que se conservan. Por ejemplo, simplemente intercambiando el orden de los objetivos secundarios en la consulta conjuntiva anterior hará que falle:

?- my_pred(X), X = a.
false.

Por lo tanto, sugiero encarecidamente que permanezca dentro del subconjunto monotónico puro de Prolog, lo que permite el razonamiento declarativo a lo largo de las líneas descritas anteriormente.

Las restricciones CLP (FD), dif/2 etc. son todas puras en este sentido: no se puede engañar a estos predicados para que den respuestas lógicamente inválidas, sin importar los modos, órdenes, etc. en que los use. if_/3 también satisface esta propiedad. Por otro lado, var/1 , nonvar/1 , integer/1 nonvar/1 !/0 , predicados con efectos secundarios, etc., todos hacen referencia extra lógica a algo fuera del mundo declarativo que se está describiendo, y por lo tanto no se puede considerar puro.

EDITAR : Para aclarar: las buenas propiedades que menciono aquí no son de ninguna manera exhaustivas. El código Pure Prolog exhibe muchas otras propiedades extremadamente valiosas a través de las cuales puede percibir la gloria de la programación lógica. Por ejemplo, en el código de Prolog puro, agregar una cláusula puede, como máximo, ampliar , nunca restringir, el conjunto de soluciones; agregar un objetivo puede, como máximo, estrecharlo , nunca extenderlo, etc.

El uso de una sola primitiva extra-lógica puede, y generalmente lo hará, destruir muchas de estas propiedades. Por lo tanto, por ejemplo, cada vez que use !/0 , considérelo un corte en el corazón de la pureza, y trate de sentir arrepentimiento y vergüenza por herir estas propiedades.

Un buen libro de Prolog al menos comenzará a presentar o contener muchos consejos para fomentar una visión declarativa, guiarlo a pensar en consultas más generales, propiedades que se conservan, etc. Los libros de Bad Prolog no dicen mucho sobre esto y generalmente terminan usando exactamente esos elementos impuros del lenguaje que destruyen las propiedades más valiosas y bellas del idioma.

Un entorno de enseñanza de Prolog impresionante que hace un uso extensivo de estas propiedades para implementar la depuración declarativa se llama GUPU , le recomiendo que revise estas ideas. Ulrich Neumerkel ha hecho generosamente una idea central que se utiliza en su entorno, en parte disponible como biblioteca (diadema) . Consulte el archivo fuente para ver un buen ejemplo sobre cómo depurar declarativamente un objetivo que falla inesperadamente: la biblioteca genera sistemáticamente generalizaciones de la consulta que aún fallan. Este razonamiento, por supuesto, funciona perfectamente con código puro .