Evolving a logic programming language

part1.clj

;; Evolving a logic programming language
;; Based on sketches at https://github.com/frenchy64/Logic-Starter/blob/master/src/logic_introduction/decl_model.clj

;; A logic statement reduces to true or false.

true
;=> true

false
;=> false

;; These two primitive logic statements are our building blocks.

;; A means of combination for logic statements is logical conjunction (and).

;; `choose-all` returns true if all arguments are true logic statements, 
;; and otherwise returns false.
;; Therefore, choose-all is itself a logic statement.

(defmacro choose-all [& stmts]
  `(every? true? ~@stmts)))

;; choose-all does not short-circuit.

(choose-all true true true)
;=> true

(choose-all false true false)
;=> false

(choose-all)
;=> true


;; Another means of combination for logic statements is logical disjunction (or).

;; choose-one returns true if 1+ arguments are true logic statements, 
;; and otherwise returns false.
;; Therefore, choose-one is a logic statement.

(defmacro choose-one [& stmts] 
  `(boolean (some true? ~@stmts)))

;; choose-one does not short-circuit.

(choose-one true false)
;=> true

(choose-one false false)
;=> false

(choose-one)
;=> true



;; A predicate is a function that returns either true or false, therefore
;; a predicate is a logic statement.

;; clojure.core/= is a predicate

(= 'John 'John)
;=> true

(= 'Andrew 'John)
;=> false

;; If our building blocks and tools are exclusively logic statements, 
;; then our result will be a logic statement.

(defn person [n]
   (choose-one (= n 'John)
               (= n 'Andrew)
               (= n 'Billy))

(person 'John)
;=> true

(person 'Tokyo)
;=> false

(choose-one (person 'John)
            (person 'Tokyo))
;=> true

(choose-all (choose-one (person 'Billy))
            true
            (choose-all (person 'Andrew)
                        true)))
;=> true

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;; A logic variable is an abstraction of uncertainty.
;; It can represent different degrees of uncertainty

;; State 0: Unbound
;;   - represents no knowledge

;; State 1a: Bound to an unground value (contains uncertain logic variables)
;;   - represents semi-definite knowledge

;; State 1b: Bound to a ground value (contains no uncertain logic variables)
;;   - represents definite knowledge

;; Logic variables are initialized to Unbound then can be bound at most once.

(defprotocol SetOnce
  (set-once! [this v]))

(deftype LogicVariable [d]
  SetOnce
  (set-once! [_ v]
    (if (unbound? d)
      (do 
        (dosync (swap! d (fn [_] v)))
        true)
      false))

  clojure.lang.IDeref
  (deref [this] @d))

(deftype UnboundValue [])

(defn unbound? [d]
  (instance? UnboundValue @d))

(defn logic-variable []
  (LogicVariable. (atom (UnboundValue.))))


;; Unbound
(let [v (logic-variable)]
  @v)
;=> :UNBOUND

;; Bound to a ground value
(let [v (logic-variable)]
  (set-once! v 1)
  @v)
;=> 1

;; Bound to an unground value
(let [v1 (logic-variable)
      v2 (logic-variable)]
  (set-once! v1 v2)
  @v)
;=> <LogicVariable :UNBOUND>

;; `reify-result` prepares the value of a logic variable as a ground value by
;; recursively replacing logic variables by their values.

(defn reify-result [v]
  (prewalk (fn [e]
             (if (instance? LogicVariable e)
               (reify-solved @e)
               e))
             v))

;; Try again, with reify-result
(let [v1 (logic-variable)
      v2 (logic-variable)]
  (set-once! v1 v2)
  (reify-result v1))
;=> :UNBOUND

;; `(set-once! l v)` is a predicate that returns true if l is unbound 
;; and performs a side effect of binding l to v. 
;; If l is not unbound, it returns false.

;; This implementation of person assumes n is an unbound logic variable.

(defn person [n]
   (choose-one (set-once! n 'John)
               (set-once! n 'Andrew)
               (set-once! n 'Billy))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;; Logical disjunction is an interesting means of combination. It potentially allows
;; a logic statement to return false, without affecting the result. 

;; If a statement returns false in a disjunction, we must not only ignore its
;; return value, but also reset the state of any logic variables to what they
;; were before the statement executed.

(defn person [n]
   (choose-one (undo-if-false [n]
                 (set-once! n 'John))
               (undo-if-false [n]
                 (set-once! n 'Andrew))
               (undo-if-false [n]
                 (set-once! n 'Billy)))

;; `undo-if-false` takes a vector of logic variables names and a logic statement.
;; If the logic statement is false, the logic variables are reset to their previous state
;; before the statement was executed.

(defmacro undo-if-false [[& dfvars] stmt]
  `(let [~'old-vals (map deref (list ~@dfvars))]
     (if (= false ~stmt)
       (do (map #(unsafe-lvar-set! %1 %2) (list ~@dfvars) ~'old-vals)
           false)
       true)))

;; `unsafe-lvar-set!` is like `set-once!` but it can be called multiple times.
;; It should never be used in normal circumstances.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;; Query

(let [v1 (logic-variable)]         ;; setup
  (match [(person v1)]             ;; query
         [true] (reify-result v1)  ;; if successful
         [false] :NORESULT)))      ;; if failed
;=> 'John

;; This form is a common pattern called a query. 
;; It initializes a scoped logic variable, executes a logic statement (person v1), 
;; and reifies that logic variable if the statement is true, 
;; otherwise returns :NORESULT.

;; `solve` abstracts this workflow.

(defmacro solve [[n] stmt]
  `(let [~n (logic-variable)]
     (match [~stmt]
            [true] (reify-result ~n)
            [false] :NORESULT)))

(solve [v1]
  (person v1))
;=> 'John

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;; We have two complementary implementations of person.

;; The first is for ground values.

(defn person [n]
   (choose-one (= n 'John)
               (= n 'Andrew)
               (= n 'Billy))

;; And the second for unbound logic variables.

(defn person [n]
   (choose-one (undo-if-false [n]
                 (set-once! n 'John))
               (undo-if-false [n]
                 (set-once! n 'Andrew))
               (undo-if-false [n]
                 (set-once! n 'Billy)))

;; Note: Neither work for bound logic variables

;; We can combine these implementations by introducing `set-or-equals`.
;; `set-or-equals` takes two arguments, and depending on the value of the arguments
;; either "sets" variables or performs "equals" tests in order to make both
;; arguments equal.


(defmulti set-or-equals (fn [l r] [(class l) (class r)]))

(defmethod set-or-equals 
  [LogicVariable LogicVariable]
  [l r]
  (if (identical? l r)
    true
    (match [(unbound? l) (unbound? r)] 
           [true true] (set-once! l r)
           [true false] (set-once! l @r)
           [false true] (set-once! r @l)
           [false false] (set-or-equals @l @r))))

(defmethod set-or-equals 
  [LogicVariable Object]
  [l r]
  (set-once! l r))

(defmethod set-or-equals 
  [Object LogicVariable]
  [l r]
  (set-once! r l))

(defmethod set-or-equals 
  [Object Object]
  [l r]
  (or
    (and (composite? l) (composite? r)
         (set-or-equals (first l) (first r))
         (set-or-equals (rest-nil l) (rest-nil r)))
    (= l r)))

(defmethod set-or-equals
  [nil nil]
  [l r]
  true)
(defmethod set-or-equals
  [LogicVariable nil]
  [l r]
  (set-once! l r))
(defmethod set-or-equals
  [nil LogicVariable]
  [l r]
  (set-once! r l))
(defmethod set-or-equals
  [Object nil]
  [l r]
  false)
(defmethod set-or-equals
  [nil Object]
  [l r]
  false)


;; Our reimplemented person predicate using `set-or-equals` accepts these types of arguments:
;; - ground values
;; - unbound logic variables
;; - logic variables bound to ground or nonground values

(defn person [n]
   (choose-one (undo-if-false [n]
                 (set-or-equals n 'John))
               (undo-if-false [n]
                 (set-or-equals n 'Andrew))
               (undo-if-false [n]
                 (set-or-equals n 'Billy)))


(solve [v1]
  (person v1))
;=> John

(solve [v1]
  (let [n (logic-variable)]
    (set-or-equals n 'Andrew)
    (person n))
;=> :UNBOUND             ;; Query was successful, and v1 is unbound after execution

(solve [v1]
  (let [n (logic-variable)]
    (set-or-equals n 'Tokyo)
    (person n))
;=> :NORESULT           ;; Query was not successful

(solve [v1]
  (person 'Andrew))
;=> :UNBOUND

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;; A predicate is *relational* if its arguments can be any combination of 
;; ground or unground values.

;; `set-or-equals` is relational, and predicates built with relations are
;; themselves relational, as is `person`.

;; A notable exception is `set-or-equals`, which is not built from relational parts.

;; `set-or-equals` is the most fundamental relational predicate in our language.

;; It's our "secret sauce" to building relational predicates.  

part2.clj

;; Part 2

;; Limitations of our approach

;; By making our logic variables locally scoped objects that manage their
;; own state, we must manually coordinate each logic variable carefully.

(defn person [n]
   (choose-one (undo-if-false [n]
                 (set-or-equals n 'John))
               (undo-if-false [n]
                 (set-or-equals n 'Andrew))
               (undo-if-false [n]
                 (set-or-equals n 'Billy)))

;; undo-if-false is necessary for choose-one to fulfil its contract: we can
;; pretend that logic statements that return false never happened.

;; There are two steps to ignoring an executed logic statement:
;; 1. ignore the return value of the logic statement
;; 2. reset all logic variables changed by the logic statement to before
;;    the statement was executed

;; To automate step 2, we must introduce a coordination mechanism for logic variables.

;; This mechanism should allow us to take a "snapshot" of all scoped
;; logic variables. With this, we can automate step 2 by saving a snapshot
;; of the current scope before executing a "failable" logic statement. On
;; failure, we can just "roll back" the current state to this snapshot.

;; A simple solution to this problem is a substitution list (or substitution).
;; A substitution is a list of associations, which pair logic variables with values.

;; For example, 

(let [a (logic-variable)
      b (logic-variable)
      c (logic-variable)]
  ;; Current substitution: ((a :UNBOUND) (b :UNBOUND) (c :UNBOUND))

  (choose-all
    (set-or-equals a 1)
    ;; Current substitution: ((a 1) (b :UNBOUND) (c :UNBOUND))

    (set-or-equals b 2)
    ;; Current substitution: ((a 1) (b 2) (c :UNBOUND))

    (set-or-equals c 3)
    ;; Current sustitution: ((a 1) (b 2) (c 3))
))


;; `choose-one` can automate rolling back changes by managing the substitution
;; list that propagates through it.

(let [a (logic-variable)
      b (logic-variable)
      c (logic-variable)]
   ;; Current substitution: ((a :UNBOUND) (b :UNBOUND) (c :UNBOUND))

  (choose-one
    (set-or-equals a 1)
    ;; Current substitution: ((a 1) (b :UNBOUND) (c :UNBOUND))

    (choose-all 
      (set-or-equals b 2)
      ;; Current substitution: ((a 1) (b 2) (c :UNBOUND))

      (set-or-equals a 3)) ;; FAILURE!
    ;; FAILURE! Roll back!
    ;; Current substitution: ((a 1) (b :UNBOUND) (c :UNBOUND))
))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;; How do we create and manipulate a substitution?

(def empty-substitution '())

(defn extend-substitution [x v s]                                                               
  (cons (list x v) s)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;; Who manages these substitutions?

;; Our representation of a logic statement is not sufficient to accommodate
;; substitutions. We introduce the "goal", which encapsulates a logic statement
;; and also manages substitutions.

;; A goal is a function that takes a substitution, and returns either
;; - the next substitution, representing a successful goal or
;; - nil, representing an unsuccessful goal.

;; There two fundamental goals. 

;; `succeed` is like `true`, a "successful" logic statement.
;; It is a goal because it is a function that takes a substitution, and returns
;; the next substitution.

(def succeed 
  (fn [s] s))

;; `fail` is like `false`, a "failed" logic statement.
;; It is a goal because it is a function that takes a substitution and returns
;; nil.

(def fail 
  (fn [s] nil))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;; We are no longer working in a language that understands our primitives.

succeed
;=> <fn succeed [s] ...>

fail
;=> <fn fail [s] ...>

;; Clojure understood logic statements because the values `true` and `false`
;; already had semantic meaning to other Clojure primitives (like `if`).

;; We must now build a language that provides primitives for combining and abstracting goals.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;; Now that our state is controlled by substitutions, logic variable objects
;; no longer control their state.

;; We can change our logic variable representation to be much simpler, as they
;; now are only responsible for their "identity".

(deftype LogicVariable [name])

(defn logic-variable [name]
   (LogicVariable. name))

(defn logic-variable? [v]
   (instance? LogicVariable v))