core.logic.nominal

core.logic.nominal extends core.logic with three primitives for nominal logic programming: fresh, hash and tie. fresh introduces new noms, hash constraints a nom to be free in a term, and tie constructs a binder: a term in which a given nom is bound.

Examples

For these examples, set your namespace as follows:

(ns nominal-tutorial
  (:refer-clojure :exclude [==])
  (:use [clojure.core.logic :exclude [is] :as l]
        [clojure.core.logic.nominal :exclude [fresh hash] :as nom]
        [clojure.test]))

Like a unique object, a nom unifies only with itself or an unbound variable:

(is (= (run* [q] (nom/fresh [a] (== a a))) '(_0)))
(is (= (run* [q] (fresh [x] (nom/fresh [a] (== a x)))) '(_0)))
(is (= (run* [q] (nom/fresh [a] (== a 5))) ()))
(is (= (run* [q] (nom/fresh [a b] (== a b))) ()))

Like a variable, a nom in the answer is reified to a canonical form, prefixed by a to distinguish it from a variable:

(is (= (run* [q] (nom/fresh [b] (== b q))) '(a_0)))

A binder unifies with another binder up to alpha-equivalence.

(is (= (run* [q] (nom/fresh [a b] (== (nom/tie a a) (nom/tie b b)) '(_0)))))
(is (= (run* [q] (nom/fresh [a b] (== (nom/tie a b) (nom/tie b b)) ()))))
(is (= (run* [q] (nom/fresh [a b] (== (nom/tie a b) (nom/tie b a)) ()))))

A # constraint ensures that a given term contains no free occurrences of a given nom:

(is (= (run* [q] (nom/fresh [a] (nom/hash a a))) ()))
(is (= (run* [q] (nom/fresh [a b] (nom/hash a b))) '(_0)))
(is (= (run* [q] (nom/fresh [a b] (nom/hash a (nom/tie a a)))) '(_0)))

Like other constraints, # constraints may get propagated and reified.

(is (= (run* [q] (fresh [x] (nom/fresh [a] (nom/hash a x) (== q [a x]))))
      '(([a_0 _1] :- a_0#_1))))
(is (= (run* [q] (fresh [x y] (nom/fresh [a b] (nom/hash a [x y b]) (== q [a b x y]))))
      '(([a_0 a_1 _2 _3] :- a_0#_3 a_0#_2))))

For simplicity, we only reify # constraints when its nom and variables are reified too:

(is (= (run* [q] (fresh [x y] (nom/fresh [a b] (nom/hash a [x y b])))) '(_0)))