Usando uma variável restrita com `length / 2`

Aqui está o 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 

(Eu posso mudar a ordem das subconsultas, o resultado é o mesmo).

Acho que preciso rotular N antes de poder usá-lo, mas me pergunto qual é o problema? Eu não consegui engolir o length/2 antes.

O que é provavelmente mais útil do que um length/2 um pouco menos não determinístico length/2 é uma restrição de comprimento de lista adequada. Você pode encontrar uma implementação do ECLiPSe aqui , chamada len/2 . Com isso, você obtém o seguinte comportamento:

 ?- 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) 

Você pode enumerar as 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) 

ou gerando listas com bom length/2 padrão antigo 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) 

Vamos começar com o mais óbvio. Se você mudar as metas, você tem:

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

que possui as mesmas propriedades de terminação que:

 - comprimento (L, N), falso , N em 1..3 .

Então, obviamente, isso não deve terminar com o mecanismo de execução do Prolog.

No entanto, se você colocar N in 1..3 na frente, isso pode afetar a finalização. Para fazê-lo, deve ser possível, com meios finitos, provar que não há N de 4 em diante. Como você pode provar isso em um sistema sem restrições – isto é, apenas com a unificação sintática presente? Bem, você não pode. E length/2 é comumente definido apenas sem restrições presentes. Com a library(clpfd) coisas são triviais, para N #>= 4, N in 1..3 simplesmente falha 1 . Note também que a library(clpfd) não colabora muito com a library(clpq) que pode ser um candidato interessante também.

Como conseqüência, você precisaria definir seu próprio tamanho – para cada pacote de restrições em que está interessado. Isso é um pouco desagradável, mas atualmente não há uma maneira genérica de fazer isso à vista. ((Ou seja, se você estiver interessado e pensar um pouco sobre isso, você pode criar uma boa API que todo sistema de restrições deve aderir. Infelizmente, isso vai levar mais algumas décadas, eu suspeito. Atualmente, há também muita divergência.))

Então aqui está um primeiro caminho ingênuo para fd_length/2 :

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

OK, isso pode ser otimizado para evitar o ponto de escolha supérfluo. Mas há um problema mais fundamental: se você está determinando o comprimento de uma lista de comprimento N , isso criará variables ​​de restrição N ! Mas precisamos apenas de um.

 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). 

Novamente, isso não é perfeito por muitas razões: ele poderia usar o algoritmo de Brent como os sistemas atuais; e combiná-lo com todas as propriedades fd. Além disso, expressões aritméticas provavelmente não são uma boa ideia para permitir; mas eu teria que esperar por (#)/1 no SWI …


1: Estritamente falando, isso “simplesmente falha” apenas para SICStus, SWI e YAP. Para nesses sistemas, não há falha acidental devido ao esgotamento da representação atual. Ou seja, o fracasso deles sempre pode ser considerado um não honesto.

Como sobre a seguinte alternativa barroca baseada em clpfd e meta-predicado tcount/3 ?

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

 list_FDlen (Xs, N): -
    contagem ( \ _ ^ = (true), Xs, N).

Vamos perguntar!

 ? - N em 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 em inf..2, list_FDlen (Xs, N).
    N = 0, Xs = []
 ;  N = 1, Xs = [_A]
 ;  N = 2, Xs = [_A, _B]
 ;  falso.  % termina universalmente também

E essa consulta específica?

 ? - N em 2..sup, list_FDlen (Xs, N).
    N = 2, Xs = [_A, _B]
 ;  N = 3, Xs = [_A, _B, _C]
 ;  N = 4, Xs = [_A, _B, _C, _D]
 ...% não termina (como esperado)

Apresentamos uma variante clpfd -ish de length/2 adaptada à implementação clpfd de @ mat.

 : - use_module ( biblioteca (clpfd) ).
 : - use_module ( biblioteca (dialeto / sicstus) ).

 : - multifile clpfd: run_propagator / 2.

O predicado “exportado” lazy_len/2 é definido assim:

 lazy_len (Es, N): -
    N em 0..sup,% lengths são sempre inteiros não 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).

O manipulador de restrição global list_FD_size/3 modifica incrementalmente seu estado interno à medida que ocorre a propagação de restrição. Todas as modificações são rastreadas e não são concluídas após o retrocesso.

 clpfd: run_propagator (list_FD_size (State, N), _MState): - 
    get_mutable (Es0 + Min0, Estado),
    fd_inf (N, Min),
    Diferença é Min - Min0,
    comprimento (Delta, Diff),
    acrescentar (Delta, Es, Es0),
    (inteiro (N)
    -> Es = []
    ;  Delta = []
    -> verdadeiro% inalterado
    ;  update_mutable (Es + Min, Estado)
    ).

lazy_len/2 aborda o problema de dois lados; a parte da restrição clpfd foi mostrada acima. O lado da tree usa a sorting de prólogo para percorrer a lista até onde a instanciação parcial permitir 1 :

 lazylist_acc_len (_, _, N): -
    inteiro (N),
    !  .
 lazylist_acc_len (Es, N0, N): -
    var (Es)
    !
    quando ((nonvar (N); nonvar (Es)), lazylist_acc_len (Es, N0, N)).
 lazylist_acc_len ([], N, N).
 lazylist_acc_len ([_ | Es], N0, N): -
    N1 é N0 + 1,
    N em N1..sup,
    lazylist_acc_len (Es, N1, N).   

Exemplos de consultas:

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

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

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

E, finalmente, mais uma pergunta … bem, na verdade mais duas : uma subindo – a outra caindo.

 ? - L em 1..4, lazy_len (Xs, L), rotulagem ([ 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 em 1..4, lazy_len (Xs, L), rotulagem ([ baixo ], [L]).
    L = 4, Xs = [_A, _B, _C, _D]
 ;  L = 3, Xs = [_A, _B, _C]
 ;  L = 2, Xs = [_A, _B]
 ;  L = 1, Xs = [_A].

Nota de Rodapé 1: Aqui, nos concentramos em preservar o determinismo (evitar a criação de pontos de escolha) usando metas atrasadas.

    Intereting Posts