prolog - Usando una variable restringida con `length/2`

clpfd

Question

Aquí está el problema:

$ swipl
Welcome to SWI-Prolog (Multi-threaded, 64 bits, Version 7.3.6-5-g5aeabd5)
Copyright (c) 1990-2015 University of Amsterdam, VU Amsterdam
SWI-Prolog comes with ABSOLUTELY NO WARRANTY. This is free software,
and you are welcome to redistribute it under certain conditions.
Please visit http://www.swi-prolog.org for details.
For help, use ?- help(Topic). or ?- apropos(Word).
?- use_module(library(clpfd)).
true.
?- N in 1..3, length(L, N).
N = 1,
L = [_G1580] ;
N = 2,
L = [_G1580, _G1583] ;
N = 3,
L = [_G1580, _G1583, _G1586] ;
ERROR: Out of global stack % after a while

(Puedo cambiar el orden de las subconsultas, el resultado es el mismo).

Supongo que necesito etiquetar N antes de poder usarlo, pero me pregunto cuál es el problema. No he logrado estrangular length/2 antes.

Answer 1

¿Qué tal la siguiente clpfd baroque basada en clpfd y meta-predicate tcount/3 ?

:- use_module([library(clpfd), library(lambda)]). list_FDlen(Xs, N) :- tcount/3(/_^ =(true), Xs, N).

¡Vamos a consultar!

?- N in 1..3, list_FDlen(Xs, N). N = 1, Xs = [_A] ; N = 2, Xs = [_A,_B] ; N = 3, Xs = [_A,_B,_C] ; false. % terminates universally ?- N in inf..2, list_FDlen(Xs, N). N = 0, Xs = [] ; N = 1, Xs = [_A] ; N = 2, Xs = [_A,_B] ; false. % terminates universally, too

¿Qué pasa con esta consulta en particular?

?- N in 2..sup, list_FDlen(Xs, N). N = 2, Xs = [_A,_B] ; N = 3, Xs = [_A,_B,_C] ; N = 4, Xs = [_A,_B,_C,_D] ... % does not terminate (as expected)

Answer 2

Comencemos con el más obvio. Si cambia los objetivos, tiene:

?- length(L, N), N in 1..3.

que tiene las mismas propiedades de terminación que:

?- length(L, N), false, N in 1..3.

Obviamente, esto no debe terminar con el mecanismo de ejecución de Prolog.

Sin embargo, si coloca N in 1..3 al frente, esto podría afectar la terminación. Para hacerlo, debe ser posible con medios finitos demostrar que no hay N partir de 4. ¿Cómo puede probar esto en un sistema sin restricciones, es decir, solo con unificación sintáctica presente? Pues no puedes. Y length/2 se define comúnmente sin restricciones presentes. Con la library(clpfd) cosas son triviales, para N #>= 4, N in 1..3 simplemente falla ¹ . Tenga en cuenta también que la library(clpfd) no colabora mucho con la library(clpq) que también podría ser un candidato interesante.

Como consecuencia, necesitaría definir su propia longitud, para cada paquete de restricciones que le interese. Es una pena, pero actualmente no hay una forma genérica de hacerlo a la vista. ((Es decir, si está interesado y lo piensa un poco, podría encontrar una buena API a la que se debe adherir cada sistema de restricción. Por desgracia, esto tomará algunas décadas más, sospecho. Actualmente, hay demasiado). mucha divergencia.))

Así que aquí hay una primera forma ingenua para fd_length/2 :

fd_length([], N) :-
N #= 0.
fd_length([_|L], N0) :-
N0 #>= 1,
N1 #= N0-1,
fd_length(L, N1).

OK, esto podría optimizarse para evitar el punto de elección superfluo. Pero hay un problema más fundamental: si está determinando la longitud de una lista de longitud N , ¡esto creará N variables de restricción! Pero solo necesitamos uno.

fd_length(L, N) :-
N #>= 0,
fd_length(L, N, 0).
fd_length([], N, N0) :-
N #= N0.
fd_length([_|L], N, N0) :-
N1 is N0+1,
N #>= N1,
fd_length(L, N, N1).

Nuevamente, esto no es perfecto por muchas razones: podría usar el algoritmo de Brent como lo hacen los sistemas actuales; y combinarlo con todas las propiedades fd. Además, las expresiones aritméticas probablemente no sean una buena idea permitir; pero tendría que esperar por (#)/1 en SWI ...

^{1: Hablando estrictamente, esto "simplemente falla" solo para SICStus, SWI y YAP. En esos sistemas, no existe una falla accidental debido al agotamiento de la representación actual. Es decir, su fracaso siempre se puede tomar como un honesto no.}

Answer 3

Lo que probablemente sea más útil que una length/2 no determinista ligeramente menor es una restricción de longitud de lista adecuada. Puede encontrar una implementación de ECLiPSe here , llamada len/2 . Con esto obtienes el siguiente comportamiento:

?- N :: 1..3, len(Xs, N).
N = N{1 .. 3}
Xs = [_431|_482] % note it must contain at least one element!
There is 1 delayed goal.
Yes (0.00s cpu)

Luego puede enumerar las listas válidas ya sea enumerando N :

?- N :: 1..3, len(Xs, N), indomain(N).
N = 1
Xs = [_478]
Yes (0.00s cpu, solution 1, maybe more)
N = 2
Xs = [_478, _557]
Yes (0.02s cpu, solution 2, maybe more)
N = 3
Xs = [_478, _557, _561]
Yes (0.02s cpu, solution 3)

o generando listas con buena length/2 estándar length/2 :

?- N :: 1..3, len(Xs, N), length(Xs, _).
N = 1
Xs = [_488]
Yes (0.00s cpu, solution 1, maybe more)
N = 2
Xs = [_488, _555]
Yes (0.02s cpu, solution 2, maybe more)
N = 3
Xs = [_488, _555, _636]
Yes (0.02s cpu, solution 3)

Answer 4

Presentamos una variante clpfd -ish de length/2 que se adapta a la implementación clpfd de @ mat.

:- use_module(library(clpfd)). :- use_module(library(dialect/sicstus)). :- multifile clpfd:run_propagator/2.

El predicado "exportado" lazy_len/2 se define así:

lazy_len(Es, N) :- N in 0..sup, % lengths are always non-negative integers lazylist_acc_len(Es, 0, N), create_mutable(Es+0, State), clpfd:make_propagator(list_FD_size(State,N), Propagator), clpfd:init_propagator(N, Propagator), clpfd:trigger_once(Propagator).

El controlador de restricciones globales list_FD_size/3 modifica incrementalmente su estado interno a medida que se produce la propagación de restricciones. Todas las modificaciones se siguen y no se realizan al retroceder.

clpfd:run_propagator(list_FD_size(State,N), _MState) :- get_mutable(Es0+Min0, State), fd_inf(N, Min), Diff is Min - Min0, length/2(Delta, Diff), append(Delta, Es, Es0), ( integer(N) -> Es = [] ; Delta = [] -> true % unchanged ; update_mutable(Es+Min, State) ).

lazy_len/2 aborda el problema desde dos lados; la parte de restricción clpfd se muestra arriba. El lado del árbol utiliza el prolog-coroutining para recorrer la lista hasta donde la instanciación parcial permita ¹ :

lazylist_acc_len(_, _, N) :- integer(N), !. lazylist_acc_len(Es, N0, N) :- var(Es), !, when((nonvar(N);nonvar(Es)), lazylist_acc_len(Es,N0,N)). lazylist_acc_len([], N, N). lazylist_acc_len([_|Es], N0, N) :- N1 is N0+1, N in N1..sup, lazylist_acc_len(Es, N1, N).

Consultas de muestra:

?- lazy_len(Xs, N). when((nonvar(N);nonvar(Xs)), lazylist_acc_len(Xs,0,N)), N in 0..sup, list_FD_size(Xs+0, N). ?- lazy_len(Xs, 3). Xs = [_A,_B,_C]. ?- lazy_len([_,_], L). L = 2. ?- lazy_len(Xs, L), L #> 0. Xs = [_A|_B], when((nonvar(L);nonvar(_B)), lazylist_acc_len(_B,1,L)), L in 1..sup, list_FD_size(_B+1, L). ?- lazy_len(Xs, L), L #> 2. Xs = [_A,_B,_C|_D], when((nonvar(L);nonvar(_D)), lazylist_acc_len(_D,3,L)), L in 3..sup, list_FD_size(_D+3, L). ?- lazy_len(Xs, L), L #> 0, L #> 2. Xs = [_A,_B,_C|_D], when((nonvar(L);nonvar(_D)), lazylist_acc_len(_D,3,L)), L in 3..sup, list_FD_size(_D+3, L).

Y, por fin, una consulta más ... bueno, en realidad dos más: una subiendo y la otra bajando.

?- L in 1..4, lazy_len(Xs, L), labeling([up], [L]). L = 1, Xs = [_A] ; L = 2, Xs = [_A,_B] ; L = 3, Xs = [_A,_B,_C] ; L = 4, Xs = [_A,_B,_C,_D]. ?- L in 1..4, lazy_len(Xs, L), labeling([down], [L]). L = 4, Xs = [_A,_B,_C,_D] ; L = 3, Xs = [_A,_B,_C] ; L = 2, Xs = [_A,_B] ; L = 1, Xs = [_A].

^{Nota al pie 1: Aquí, nos enfocamos en preservar el determinismo (evitar la creación de puntos de elección) mediante el uso de objetivos retrasados.}