tutorial - Pruebas de tipo más seguras en Prolog

reglas en prolog

Question

ISO-Prolog (ISO / IEC 13211-1: 1995 incluyendo Cor.1: 2007, Cor.2: 2012) ofrece los siguientes predicados integrados para probar el tipo de término:

8.3 Prueba de tipo

1 var / 1. 2 átomos / 1. 3 enteros / 1. 4 flotadores / 1. 5 atómico / 1. 6 compuesto / 1. 7 nonvar / 1. 8 número / 1. 9 invocables / 1. 10 suelo / 1. 11 acyclic_term / 1.

Dentro de este grupo hay aquellos cuyo propósito es únicamente probar una determinada instanciación, que es 8.3.1 var/1 , 8.3.7 nonvar/1 , 8.3.10 ground/1 , y aquellos que suponen que un término está suficientemente instanciado tal que la prueba de tipo sea segura. Desafortunadamente, se combinan con pruebas para una instanciación concreta.

Considere el integer(X) objetivo integer(X) que falla si X es un término no variable que no es un entero y cuando X es una variable. Esto destruye muchas propiedades declarativas deseables:

?- X = 1, integer(X).
true.
?- integer(X), X = 1.
false.

Idealmente, la segunda consulta tendría éxito utilizando alguna forma de coroutining; o emitiría un error de instanciación ^{1 de} acuerdo con la clasificación del error . Después de todo:

7.12.2 Clasificación de errores

Los errores se clasifican según la forma de Error_term:

a) Habrá un error de instanciación cuando un
argumento o uno de sus componentes es una variable y un
Se requiere argumento o componente instanciado. Tiene
el formulario instantiation_error .

...

Tenga en cuenta que esta combinación implícita de pruebas de instanciación y pruebas de tipo conduce a muchos errores en los programas Prolog y también aquí en SO.

Una solución rápida a esta situación sería agregar una prueba explícita frente a cada prueba incorporada, ya sea de forma vergonzosa como

 ( var(T) -> throw(error(instantiation_error,_)) ; true),
integer(T), ....

o más compacto como

functor(T, _,_),
integer(T), ....

podría ser incluso

T =.. _,
integer(T), ...

Mi pregunta es doble:

¿Cómo proporcionar esta funcionalidad a nivel de usuario?

y, para hacer esto también un poco desafiante:

¿Cuál es la implementación más compacta de un atomic/1 más seguro escrito en ISO-Prolog?

^{1 Otras opciones menos deseables serían hacer un bucle o producir un error de recurso. Todavía preferible a un resultado incorrecto.}

Answer 1

Este es un intento muy ingenuo para implementar ambas soluciones sugeridas.

Primero, has_type(Type, Var) que tiene éxito o falla con un error de instanciación:

has_type(Type, X) :-
var(X), !,
throw(error(instantiation_error, _)).
has_type(Type, X) :-
nonvar_has_type(Type, X).
nonvar_has_type(atom, X) :- atom(X).
nonvar_has_type(integer, X) :- integer(X).
nonvar_has_type(compound, X) :- compound(X).
% etc

En segundo lugar, un could_be(Type, Var) (analogía a must_be/2 ) que utiliza la rutina para permitir que la consulta tenga éxito en algún momento en el futuro:

could_be(Type, X) :-
var(X), !,
freeze_type(Type, X).
could_be(Type, X) :-
nonvar_has_type(Type, X).
freeze_type(integer, X) :- freeze(X, integer(X)).
freeze_type(atom, X) :- freeze(X, atom(X)).
freeze_type(compound, X) :- freeze(X, compound(X)).
% etc

Hay varios puntos débiles en este enfoque, pero sus comentarios podrían ayudarme a comprender mejor los casos de uso.

EDITAR: sobre "tipos" en Prolog

Los tipos en Prolog, según tengo entendido, no son "tipos": son solo información que se puede consultar en tiempo de ejecución, y que existe porque es una abstracción útil de la implementación subyacente.

La única forma en que he podido hacer un uso práctico de un "tipo" ha sido "etiquetar" mis variables, como en los términos compuestos number(1) , number(pi) , operator(+) , date(2015, 1, 8) , y así sucesivamente. Luego puedo poner variables allí, escribir predicados deterministas o semi-deterministas, entender lo que significa mi código cuando lo veo una semana después ...

Entonces, una variable libre y un entero son solo términos; principalmente porque, como su pregunta señala muy inteligentemente, una variable libre puede convertirse en un número entero, un átomo o un término compuesto. Puede utilizar la rutina para asegurarse de que una variable libre solo puede convertirse en un cierto "tipo" de término más adelante, pero esto es inferior al uso de términos compuestos, desde un punto de vista práctico.

Es muy probable que esté confundiendo temas muy diferentes aquí; y para ser honesto, mi experiencia con Prolog es limitada en el mejor de los casos. Acabo de leer la documentación de la implementación que estoy usando, y trato de encontrar la mejor manera de usarla en mi beneficio.

Answer 2

La prueba de tipos debe distinguirse de las incorporaciones tradicionales de "prueba de tipo" que implícitamente también prueban una instanciación suficiente. Por lo tanto, probamos de manera efectiva solo para términos suficientemente instanciados ( si ). Y si no están suficientemente instanciados, se emite un error apropiado. Para un tipo nn , existe un predicado de prueba de tipo nn_si/1 con la única condición de error

a) Si hay un θ y σ tal que nn_si(Xθ) es verdadero y nn_si(Xσ) es falso
- instantiation_error .

atom_si(A) :-
functor(A, _, 0), % for the instantiation error
atom(A).
integer_si(I) :-
functor(I, _, 0),
integer(I).
atomic_si(AC) :-
functor(AC,_,0).
list_si(L) :-
/+ /+ length(L, _), % for silent failure
sort(L, _). % for the instantiation error

En SWI, debido a su comportamiento diferente en length/2 , use más bien:

list_si(L) :-
''$skip_list''(_, L, T),
functor(T,_,_),
T == [].