Permalink
Browse files

Moved to core.logic 0.6.7. Arithmetic examples are more relational

  • Loading branch information...
1 parent b830980 commit db6d3f4f4681409f59b3323f27d4a39971ec77f8 @frenchy64 committed Dec 21, 2011
Showing with 86 additions and 54 deletions.
  1. +1 −1 project.clj
  2. +85 −53 src/logic_introduction/numbers.clj
View
2 project.clj
@@ -3,4 +3,4 @@
:dependencies [[org.clojure/clojure "1.3.0"]
[match "0.2.0-SNAPSHOT"]
[org.clojure/data.json "0.1.1"]
- [org.clojure/core.logic "0.6.5"]])
+ [org.clojure/core.logic "0.6.7"]])
View
138 src/logic_introduction/numbers.clj
@@ -4,96 +4,128 @@
;; From "Art of Prolog", Chapter 3
-(defn s [n]
- "Returns n's succeeding natural number"
- (llist n []))
+(defn s [a d]
+ (conso a [] d))
-(def zero 0)
-(def one (s zero))
-(def two (s one))
-(def three (s two))
-(def four (s three))
-(def five (s four))
-(def six (s five))
+(def zero 0)
+(def one (first (run 1 [q] (s zero q))))
+(def two (first (run 1 [q] (s one q))))
+(def three (first (run 1 [q] (s two q))))
+(def four (first (run 1 [q] (s three q))))
+(def five (first (run 1 [q] (s four q))))
+(def six (first (run 1 [q] (s five q))))
(defn natural-number [x]
"A relation where x is a natural number"
- (matche [x]
- ([zero])
- ([(s ?x)] (natural-number ?x))))
+ (conde
+ [(== zero x)]
+ [(fresh [p]
+ (s p x)
+ (natural-number p))]))
(defn <=o [x y]
"x and y are natural numbers, such that x is less than or
equal to y"
- (matche [x y]
- ([zero _] (natural-number y))
- ([(s ?x) (s ?y)] (<=o ?x ?y))))
+ (conde
+ [(== x zero)
+ (natural-number y)]
+ [(fresh [xp yp]
+ (s xp x)
+ (s yp y)
+ (<=o xp yp))]))
(defn <o [x y]
"x and y are natural numbers, such that x is less than y"
- (matche [x y]
- ([zero _] (natural-number y) (!= x y))
- ([(s ?x) (s ?y)] (<=o ?x ?y))))
+ (conde
+ [(== x zero)
+ (natural-number y)
+ (!= x y)]
+ [(fresh [xp yp]
+ (s xp x)
+ (s yp y)
+ (<=o xp yp))]))
(defn plus [x y z]
"x, y, and z are natural numbers such that z is the sum of
x and y"
- (matche [x y z]
- ([zero ?x ?x] (natural-number ?x))
- ([(s ?x) _ (s ?z)] (plus ?x y ?z))))
+ (conde
+ [(fresh [a]
+ (== [zero a a] [x y z])
+ (natural-number a))]
+ [(fresh [xp zp]
+ (s xp x)
+ (s zp z)
+ (plus xp y zp))]))
(defn times [x y z]
"x, y, and z are natural numbers such that z is the product
of x and y"
- (matche [x y z]
- ([zero _ zero])
- ([(s ?x) _ _] (fresh [xy]
- (times ?x y xy)
- (plus xy y z)))))
+ (conde
+ [(== [zero zero] [x z])]
+ [(fresh [xp xy]
+ (s xp x)
+ (times xp y xy)
+ (plus xy y z))]))
(defn exp [n x y]
"n, x, and y are natural numbers such that y equals x raised
to the power n"
- (matche [n x y]
- ([(s ?x) zero zero])
- ([zero (s ?x) (s zero)])
- ([(s ?n) _ _] (fresh [z]
- (exp ?n x z)
- (times z x y)))))
+ (conde
+ [(fresh [np]
+ (== [zero zero] [x y])
+ (s np n))]
+ [(fresh [xp]
+ (== [zero one] [n y])
+ (s xp x))]
+ [(fresh [np z]
+ (s np n)
+ (exp np x z)
+ (times z x y))]))
(defn factorial [n f]
"f equals n factorial"
- (matche [n f]
- ([zero (s zero)])
- ([(s ?n) _] (fresh [f1]
- (factorial ?n f1)
- (times (s ?n) f1 f)))))
+ (conde
+ [(== [zero one] [n f])]
+ [(fresh [np f1]
+ (s np n)
+ (factorial np f1)
+ (times n f1 f))]))
(defn minimum [n1 n2 min]
"The minimum of the natural numbers n1 and n2 is min"
- (matche [n1 n2 min]
- ([_ _ n1] (<=o n1 n2))
- ([_ _ n2] (<=o n2 n1))))
+ (conde
+ [(== n1 min)
+ (<=o n1 n2)]
+ [(== n2 min)
+ (<=o n2 n1)]))
(defn modo [x y z]
"z is the remainder of the integer division of x by y"
- (<o z y)
(fresh [q qy]
- (times y q qy)
- (plus qy z x)))
+ (<o z y)
+ (times y q qy)
+ (plus qy z x)))
(defn ackermann [x y a]
"a is the value of Ackermann's function for the natural
numbers x and y"
- (matche [x y a]
- ([zero ?n (s ?n)])
- ([(s ?m) zero ?val] (ackermann ?m (s zero) ?val))
- ([(s ?m) (s ?n) ?val] (fresh [val1]
- (ackermann (s ?m) ?n val1)
- (ackermann ?m val1 ?val)))))
+ (conde
+ [(s y a)
+ (== zero x)]
+ [(fresh [xp]
+ (s xp x)
+ (== zero y)
+ (ackermann xp one a))]
+ [(fresh [xp yp val1]
+ (s xp x)
+ (s yp y)
+ (ackermann x yp val1)
+ (ackermann xp val1 a))]))
(defn gcd [x y z]
"z is the greatest common divisor of the natural numbers x and y"
- (matche [x y z]
- ([_ _ ?gcd] (modo x y z) (gcd y z ?gcd))
- ([x zero x] (<o zero x))))
+ (conde
+ [(modo x y z)
+ (gcd y z z)]
+ [(== [x zero x] [x y z])
+ (<o zero x)]))

0 comments on commit db6d3f4

Please sign in to comment.