Usando una variable restringida con `length / 2`

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.

Lo que probablemente sea más útil que una length/2 ligeramente no determinista length/2 es una restricción adecuada de longitud de lista. Puede encontrar una implementación de ECLiPSe aquí , 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) 

A continuación, puede enumerar las listas válidas 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 antigua 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) 

Comencemos por el más obvio. Si cambia los objectives, tiene:

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

que tiene las mismas propiedades de terminación que:

 ? - longitud (L, N), falso , N en 1..3 .

Entonces, 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 probar que no hay N de 4 en adelante. ¿Cómo puede probar esto en un sistema sin restricciones, es decir, solo con la unificación sintáctica presente? Bueno, no puedes. Y la length/2 se define comúnmente solo sin restricciones presentes. Con library(clpfd) cosas son triviales, para N #>= 4, N in 1..3 simplemente falla 1 . 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 restricción que le interese. Eso es un poco lamentable, pero actualmente no hay una forma genérica de hacerlo a la vista. ((Es decir, si estás interesado y piensas un poco al respecto, podrías obtener una buena API que todos los sistemas de restricción deberían cumplir. Por desgracia, esto tomará más décadas, sospecho. Actualmente, también hay mucho mucha divergencia.))

Así que aquí hay una primera manera 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). 

De nuevo, 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 de fd. Además, las expresiones aritméticas probablemente no son una buena idea para permitir; pero tendría que esperar (#)/1 en SWI …


1: Estrictamente hablando, esto “simplemente falla” solo para SICStus, SWI y YAP. Porque en esos sistemas, no hay falla accidental debido al agotamiento de la representación actual. Es decir, su fracaso siempre puede tomarse como un honesto no.

¿Qué tal el siguiente trabajo de limpieza barroco basado en clpfd y meta-predicate tcount/3 ?

 : - use_module ([ library (clpfd) , library (lambda) ]).

 list_FDlen (Xs, N): -
    tcount ( \ _ ^ = (verdadero), Xs, N).

¡Vamos a preguntar!

 ? - N en 1..3, list_FDlen (Xs, N).
    N = 1, Xs = [_A]
 ;  N = 2, Xs = [_A, _B]
 ;  N = 3, Xs = [_A, _B, _C]
 ;  falso.  % termina universalmente

 ? - N en inf..2, list_FDlen (Xs, N).
    N = 0, Xs = []
 ;  N = 1, Xs = [_A]
 ;  N = 2, Xs = [_A, _B]
 ;  falso.  % termina universalmente, también

¿Qué pasa con esta consulta en particular?

 ? - N en 2..sup, list_FDlen (Xs, N).
    N = 2, Xs = [_A, _B]
 ;  N = 3, Xs = [_A, _B, _C]
 ;  N = 4, Xs = [_A, _B, _C, _D]
 ...% no termina (como se esperaba)

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

 : - use_module ( library (clpfd) ).
 : - use_module ( biblioteca (dialecto / sicstus) ).

 : - clffd multilente: run_propagator / 2.

El predicado “exportado” lazy_len/2 se define así:

 lazy_len (Es, N): -
    N en 0..sup,% longitudes son siempre enteros no negativos
    lazylist_acc_len (Es, 0, N),
    create_mutable (Es + 0, Estado),
    clpfd: make_propagator (list_FD_size (State, N), Propagator),
    clpfd: init_propagator (N, Propagator),
    clpfd: trigger_once (Propagator).

El controlador de restricción global list_FD_size/3 modifica de forma incremental su estado interno a medida que se produce la propagación de restricción. Todas las modificaciones son rastreadas y no se realizan al retroceder.

 clpfd: run_propagator (list_FD_size (State, N), _MState): - 
    get_mutable (Es0 + Min0, estado),
    fd_inf (N, Min),
    Diff es Min - Min0,
    longitud (Delta, Diff),
    añadir (Delta, Es, Es0),
    (entero (N)
    -> Es = []
    ;  Delta = []
    ->% verdadero sin cambios
    ;  update_mutable (Es + Min, Estado)
    )

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

 lazylist_acc_len (_, _, N): -
    entero (N),
    !  .
 lazylist_acc_len (Es, N0, N): -
    var (Es),
    !,
    cuando ((nonvar (N); nonvar (Es)), lazylist_acc_len (Es, N0, N)).
 lazylist_acc_len ([], N, N).
 lazylist_acc_len ([_ | Es], N0, N): -
    N1 es N0 + 1,
    N en N1..sup,
    lazylist_acc_len (Es, N1, N).   

Consultas de muestra:

 ? - lazy_len (Xs, N).
 cuando ((nonvar (N); nonvar (Xs)), lazylist_acc_len (Xs, 0, N)),
 N en 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],
 cuando ((nonvar (L); nonvar (_B)), lazylist_acc_len (_B, 1, L)),
 L en 1..sup,
 list_FD_size (_B + 1, L).

 ? - lazy_len (Xs, L), L #> 2.
 Xs = [_A, _B, _C | _D],
 cuando ((nonvar (L); nonvar (_D)), lazylist_acc_len (_D, 3, L)),
 L en 3.sup,
 list_FD_size (_D + 3, L).

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

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

 ? - L en 1..4, lazy_len (Xs, L), etiquetado ([ arriba ], [L]).
    L = 1, Xs = [_A]
 ;  L = 2, Xs = [_A, _B]
 ;  L = 3, Xs = [_A, _B, _C]
 ;  L = 4, Xs = [_A, _B, _C, _D].

 ? - L en 1..4, lazy_len (Xs, L), etiquetado ([ abajo ], [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 objectives retrasados.

    Intereting Posts