Goal-Bestellung in Clojure `core.logic`

Question

The following Clojure code verwendet core.logic, um das gleiche logische Problem mit den gleichen Zielen in zwei verschiedenen Ordnungen zu lösen. Diese Wahl der Reihenfolge bewirkt, dass man schnell fertig wird und der andere hängt.

(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])))) 

Gibt es eine allgemeine Lösung oder gängige Praxis, um dieses Problem zu vermeiden?

Answer 1

Wenn Sie membero verwenden, gibt es keine allgemeine Lösung für dieses Problem. Das Aufrufen von membero mit frischen vars wird dazu führen, dass es alle (gelesenen, unendlichen) möglichen Listen erzeugt, für die q ein Mitglied ist. Natürlich gelten Listen, die größer als 3 sind, nicht - aber seit du run* benutzt hast, versuchst du weiterhin, Listen zu versuchen, die größer als 3 sind, auch wenn jeder Fehler auftritt.

Es ist möglich, eine bessere Version von membero in neueren Versionen von core.logic unter Verwendung der Constraint-Infrastruktur zu schreiben, aber die Details, wie man dies tun könnte, werden sich wahrscheinlich in den kommenden Monaten ändern. Bis es eine solide öffentliche API für die Definition von Einschränkungen gibt, sind Sie mit den subtilen Problemen bei der Bestellung und Nicht-Beendigung von Problemen konfrontiert, die Prolog Probleme bereiten.

Answer 2

Hier ist mein Verständnis:

Mit core.logic, möchten Sie den Suchraum zu reduzieren, so früh wie möglich. Wenn Sie die membero-Einschränkung zuerst setzen, wird der Lauf mit der Suche nach dem membero-Leerzeichen und der Rückverfolgung bei Fehlern, die durch die ==-Einschränkung erzeugt wurden, gestartet. Aber der membero Raum ist RIESIG, da weder q noch x vereinheitlicht oder zumindest begrenzt ist.

Aber wenn Sie die == Einschränkung die erste Stelle setzen, können Sie direkt x vereinigen mit [1 2 3], und der Suchraum für membero nun eindeutig auf die Elemente der x begrenzt.