Skip to content

Instantly share code, notes, and snippets.

@whodidthis
Created March 27, 2015 20:15
Show Gist options
  • Select an option

  • Save whodidthis/98317fcc23881f712a4f to your computer and use it in GitHub Desktop.

Select an option

Save whodidthis/98317fcc23881f712a4f to your computer and use it in GitHub Desktop.
natural numbers in core.logic
(ns logic.numbers
(:refer-clojure :exclude [==])
(:use clojure.core.logic))
; s is a list with a single element
(defn s [x y]
(conso x [] y))
; natural_number(0). natural_number(s(X)) :- natural_number(X).
(defn natural-number [x]
(conde
[(== x 0)]
[(fresh [p]
(s p x)
(natural-number p))]))
; natural_number(s(s(0))). should be yes
(run 1 [q]
(natural-number '((0)))
(== q true)) ;for a 'nicer' yes.
; => (true)
; natural_number(s(s(s(1)))). should be no
(run 1 [q]
(natural-number '(((1))))
(== q true))
; => ()
; plus(0, X, X). plus(s(X), Y, s(Z)) :- plus(X, Y, Z).
(defn plus [x y z]
(conde
[(fresh [a]
(== [0 a a] [x y z]))]
[(fresh [x1 z1]
(s x1 x)
(s z1 z)
(plus x1 y z1))]))
; plus(s(s(0)), s(0), X). should be X = s(s(s(0)))
(run 1 [q]
(fresh [z]
(plus '((0)) '(0) z)
(== q z)))
; => ((((0)))), it's a (((0))) inside resulting list!
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment