L'ordinamento degli obiettivi in ​​`core.logic` di Clojure

Question

The following Clojure code utilizza core.logic per risolvere lo stesso problema logico con gli stessi obiettivi in ​​due ordini diversi. Questa scelta di ordini fa sì che uno finisca rapidamente e l'altro si blocchi.

(use `clojure.core.logic) 

;; Runs quickly. Prints (1 2 3). 
(clojure.pprint/pprint (run* [q] (fresh [x] (== x [1,2,3]) 
              (membero q x)))) 

;; Hangs 
(clojure.pprint/pprint (run* [q] (fresh [x] (membero q x) 
              (== x [1,2,3])))) 

Esiste una soluzione generale o una pratica comune per evitare questo problema?

Answer 1

Se si sta utilizzando membero non esiste una soluzione generale a questo problema. Chiamando membero con vars freschi, genererà tutti gli elenchi possibili (letti, infiniti) per i quali q è membro. Ovviamente gli elenchi più grandi di 3 non si applicano - ma dal momento che hai utilizzato run* continuerà a cercare ciecamente elenchi più grandi del conteggio 3, anche se ognuno fallirà.

È possibile scrivere una versione migliore di membero nelle versioni più recenti di core.logic utilizzando l'infrastruttura di vincoli, ma è probabile che i dettagli di come si potrebbe farlo cambino nei prossimi mesi. Fino a quando non ci sarà una solida aqua pubblica per definire i vincoli, rimarrai bloccato dal tipo di ordine sottile e dai problemi di non terminazione che causano problemi a Prolog.

Answer 2

Qui è la mia comprensione:

Con core.logic, si vuole ridurre lo spazio di ricerca il più presto possibile. Se si imposta per primo il vincolo membero, la corsa inizierà cercando lo spazio membero e il backtrack in caso di errore prodotto dal vincolo ==. Ma lo spazio membero è ENORME, poiché né lo q né lo x sono unificati o almeno delimitati.

Ma se si mette prima il vincolo ==, di unificare direttamente x con [1 2 3], e lo spazio di ricerca per membero ora è chiaramente delimitata a elementi di x.