Finite Choice Programming In Clojure

(ns finite-choice.core)

;; Finite Choice Programming in Clojure 
;; 
;; References:
;;    https://popl25.sigplan.org/details/POPL-2025-popl-research-papers/13/Finite-Choice-Logic-Programming
;;    https://dusa.rocks/docs/

;; The following code is mostly AI generated (Grok). Some iteration required.
;; 
;; The following does not implement Dusa’s full feature set. It is missing the following: 
;;  - No multiple solution sets—just one combined fact set.
;;  - Only closed choices, no open choice flexibility.
;;  - Basic constraint flagging (invalid) but no full #forbid/#demand solving.
;;  - Simplified procedural semantics without Dusa’s nuanced rule firing.
;;  - No built-ins like arithmetic.
;;  - Implicit rather than explicit relational/functional distinction.



(defn unify [pattern fact subst]
  (cond
    (empty? pattern) subst
    (symbol? (first pattern)) (unify (rest pattern) (rest fact) (assoc subst (first pattern) (first fact)))
    (= (first pattern) (first fact)) (unify (rest pattern) (rest fact) subst)
    :else nil))

(defn match [facts body subst]
  (if (empty? body)
    [subst]
    (let [first-body (first body)]
      (mapcat #(match facts (rest body) %) 
              (filter some? (map #(unify first-body % subst) facts))))))

(defn deduce [facts rules]
  (for [[head body choices] rules
        subst (match facts body {})
        choice (if (empty? choices) [{}] choices)
        :let [inst (merge subst choice)
              new-fact (mapv #(if (symbol? %) (get inst % %) %) head)]
        :when (and (not (contains? facts new-fact))
                   (or (not= (first head) "invalid")
                       (not= (second new-fact) (nth new-fact 2))))]
    new-fact))

(defn solve [db]
  (loop [facts (:facts db)]
    (let [new-facts (into facts (deduce facts (:rules db)))]
      (if (= facts new-facts)
        facts
        (recur new-facts)))))

;; Test 1: Graph coloring with a linear chain graph
;; This test defines a simple graph with two edges (1-2 and 2-3), forming a chain (1 → 2 → 3).
;; It infers nodes from edges and assigns each node a color from a finite set ("red", "blue", "green").
;; The rules deduce nodes from edge sources and targets separately,
;; then assign all possible colors to each inferred node, testing the finite choice mechanism without constraints.
(def chain-db {:facts #{["edge" 1 2] ["edge" 2 3]}
               :rules [[["color" '?n '?c]
                        [["node" '?n]]
                        [{'?c "red"} {'?c "blue"} {'?c "green"}]]
                       [["node" '?n]
                        [["edge" '?n '?m]]
                        []]
                       [["node" '?m]
                        [["edge" '?n '?m]]
                        []]]})

;; Test 2: Shape assignment in a triangle graph with adjacency constraint
;; This test models a cyclic graph—a triangle with three nodes (1, 2, 3) and edges (1-2, 2-3, 3-1)—to explore
;; Finite Choice Programming in a more complex structure than the linear chain of Test 1.
;; The rules:
;; 1. Assign each inferred node a shape from a finite set ("circle", "square", "triangle"), generating all possible
;;    assignments (3 nodes × 3 shapes = 27 combinations before constraints).
;; 2. & 3. Infer nodes from edge sources (?n) and targets (?m) separately, ensuring all three nodes (1, 2, 3) are
;;    deduced from the cyclic edge relationships (e.g., 1 from 1-2, 2 from 2-3 and 1-2, 3 from 3-1 and 2-3).
;; 4. Flag pairs of adjacent nodes (?n and ?m connected by an edge) that share the same shape (?s) as "invalid",
;;    testing the system's ability to deduce constraints alongside choices.
;; Expected behavior: Outputs all edges, nodes, shape assignments, and invalid pairs (e.g., [invalid 1 2] when node 1
;; and node 2 have the same shape). Since this is an undirected graph, it generates bidirectional invalid facts
;; (e.g., [invalid 1 2] and [invalid 2 1]) when adjacency conditions are met, reflecting exhaustive constraint checking.
;; This tests Finite Choice Programming’s capacity to handle cyclic graphs, deduce facts from bidirectional relationships,
;; and layer choice generation with constraint identification, contrasting with Test 1’s simpler, unconstrained approach.
(def triangle-db {:facts #{["edge" 1 2] ["edge" 2 3] ["edge" 3 1]}
                  :rules [[["shape" '?n '?s]
                           [["node" '?n]]
                           [{'?s "circle"} {'?s "square"} {'?s "triangle"}]]
                          [["node" '?n]
                           [["edge" '?n '?m]]
                           []]
                          [["node" '?m]
                           [["edge" '?n '?m]]
                           []]
                          [["invalid" '?n '?m]
                           [["edge" '?n '?m] ["shape" '?n '?s] ["shape" '?m '?s]]
                           []]]})

(println "Chain test result:" (solve chain-db))
(println "Triangle test result:" (solve triangle-db))