prolog - Variable de ocurrencia en una lista de variables.

iso-prolog

Question

Considere un predicado (meta-lógico) var_in_vars(Var, Vars) que toma una variable Var y una lista de variables Vars y tiene éxito si Var ocurre en Vars . Por lo tanto, no necesitamos asegurarnos de que Var sea ​​una variable, ni que Vars sea ​​una lista de variables.

¿Cuál es la forma más compacta y canónica de expresar esto en ISO Prolog? Aquí hay una descripción general de los elementos incorporados en ISO / IEC 13211-1: 1995, incluyendo Cor.2: 2012.

?- var_in_vars(V, [U,V,W]).
true.

?- var_in_vars(V, [X,Y,Z]).
false.

Answer 1

Síntesis de la solución

Solución: Corto

var_in_vars(V, Vs) :- /+ subsumes_term(V, Vs).

Alternativa 1: Simple

var_in_vars(V, Vs) :- /+ unify_with_occurs_check(V, Vs).

Alternativa 2: Dependiendo de las circunstancias, esto podría ser más adecuado

var_in_vars(V, Vs) :-
        must_be(list, Vs),
        once((member(X, Vs), V == X)).

Alternativa 3: más compleja

var_in_vars(V, Vs) :-
   term_variables(Vs+V, Ws),
   Ws == Vs.

Alternativa 4: Otra posibilidad

var_in_vars(V, [H|_]) :- V == H, !.
var_in_vars(V, [_|T]) :- var_in_vars(V, T).

Enlaces:

Estándar

Nota: El contexto de la pregunta, que es un desafío de compacidad específico que involucra la expresividad de los predicados de ISO en determinadas circunstancias.

Answer 2

La solución @false se puede simplificar para:

var_in_vars(V, Vs) :-
    term_variables(Vs+V, Vs).

Cuando V es un miembro de la lista de Vs , el segundo argumento devuelve Vs (debido al cruce de izquierda a derecha del término Vs+V ). Cuando V no es miembro de Vs , el segundo argumento devuelve una lista que tiene un elemento más que Vs y, por lo tanto, no se puede unificar con ella. Aunque hay una unificación implícita en el segundo argumento, en ningún caso existe el peligro de crear un término cíclico. Es decir, la unificación siendo STO no es un problema en esta solución simplificada.

Pero, ¿vale la pena la simplificación con el rendimiento? El uso de la igualdad, (==)/2 tiene el potencial de fallar antes y por lo tanto hacer que la solución original sea más rápida.

Answer 3

Una posibilidad:

var_in_vars(V, Vs) :- /+ unify_with_occurs_check(V, Vs).

y más corto:

var_in_vars(V, Vs) :- /+ subsumes_term(V, Vs).

EDITAR : Futuros lectores, tenga en cuenta el contexto de la pregunta, que es un desafío de compacidad específico que involucra la expresividad de los predicados ISO en determinadas circunstancias.

En otras circunstancias, es probable que se beneficie más de una definición como:

var_in_vars(V, Vs) :-
        must_be(list, Vs),
        once((member(X, Vs), V == X)).

Answer 4

Una solución alternativa es:

var_in_vars(V, Vs) :-
    /+ (V = Vs, acyclic_term(Vs)).

Pero las soluciones de @mat son mejores y más elegantes y la solución de @CapelliC fue durante mucho tiempo la más portátil (el predicado subsumes_term/2 se estandarizó recientemente y no todos los sistemas proporcionaron el predicado unify_with_occurs_check/2 ).

Answer 5

Y aquí va otro, aunque un poco más complejo:

var_in_vars(V, Vs) :-
   term_variables(Vs+V, Ws),
   Ws == Vs.

Así que esto depende del orden preciso en que se visitan las variables. Y como esto está bien definido en la norma, podemos confiar en que

... aparecen de acuerdo con su primera aparición en el recorrido de izquierda a derecha ...

Un inconveniente de esta definición es que tiene un costo mínimo proporcional a la longitud de Vs Pero como un recorrido interno a menudo se implementa de manera bastante eficiente, este no es un problema de este tipo.

Tiene una gran ventaja: solo tiene éxito si Vs es una lista de variables.

Answer 6

esta definición pasa las pruebas, pero ... ¿echo de menos alguna sutileza?

var_in_vars(V, [H|_]) :- V == H, !.
var_in_vars(V, [_|T]) :- var_in_vars(V, T).