summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorpukkamustard <pukkamustard@posteo.net>2020-09-27 08:02:10 +0200
committerpukkamustard <pukkamustard@posteo.net>2020-09-27 08:02:10 +0200
commite8f4af287a327cf8e9954b2d1ba70f9425fb7e70 (patch)
treea29eb690b9cf581bad8be5be3bdddecfeb8fc9f5
parent96bd70d5ffbeab6c955950752b9ad60b255223ff (diff)
(schemantic datalog): export datalog-eval and add an example to tests
-rw-r--r--schemantic/datalog.scm140
-rw-r--r--tests/schemantic/datalog.scm34
2 files changed, 70 insertions, 104 deletions
diff --git a/schemantic/datalog.scm b/schemantic/datalog.scm
index 92161b7..a75182d 100644
--- a/schemantic/datalog.scm
+++ b/schemantic/datalog.scm
@@ -30,7 +30,9 @@
fact?
make-fact
- :- !))
+ :- !
+
+ datalog-eval))
;; Atom
@@ -111,12 +113,26 @@
(syntax
(make-fact head-atom)))))))
-;; (let ((a (lvar))
-;; (b (lvar))
-;; (c (lvar)))
-;; (:- (path a b) (edge a c) (path c b)))
+;; VHash helpers
+
+(define* (vhash-ref key vhash #:key (default #f))
+ (cond
+ ((vhash-assoc key vhash) (cdr (vhash-assoc key vhash)))
+ (else default)))
+
+(define (vhash-map proc vhash)
+ (vhash-fold
+ (lambda (key value result)
+ (vhash-cons
+ key (proc key value)
+ result))
+ vlist-null
+ vhash))
;; Substitution
+;;
+;; A substitution is a VHash from the term to be replaced to the term to be
+;; replaced with.
(define-method (substitute (x <atom>) s)
(make-atom
@@ -137,77 +153,19 @@
((vhash-assoc x s) (cdr (vhash-assoc x s)))
(else x)))
-(define (substitution-compose s t)
- (vhash-fold
- (lambda (x y result)
- (vhash-cons x (substitute y t) result))
- t s))
-
-;; Returns the most general unifier for literals l and m.
-(define-method (mgu (l <atom>) (m <atom>))
- (if (not (equal? (atom-predicate l) (atom-predicate m)))
- ;; predicates do not match. No unifier exists.
- #nil
-
- ;; fold over terms in l and m
- (vector-fold
- (lambda (_ s tl tm)
- (unless (nil? s)
- (let ((tls (substitute tl s))
- (tms (substitute tm s)))
- (cond
-
- ;; do nothing if tl and tm already unified
- ((equal? tls tms) s)
-
- ;;
- ((lvar? tms)
- (substitution-compose s (vhash-cons tms tls vlist-null)))
-
- ;;
- ((lvar? tls)
- (substitution-compose s (vhash-cons tls tms vlist-null)))
-
- ;; can not unify
- (else #nil)))))
-
- ;; initialize emtpy substitution
- vlist-null
-
- (atom-terms l) (atom-terms m))))
-
-;; The Elemementary Production (EP) rule
-(define (produce rule facts)
- (let ((result (vector-fold
-
- (lambda (i rule k_i f_i)
- (let ((s (mgu k_i f_i)))
- (if (nil? s) #nil
- (substitute rule s))))
-
- rule
-
- (clause-body rule)
- (vector-map (lambda (_ fact) (clause-head fact)) facts))))
- (unless (nil? result)
- (make-fact (clause-head result)))))
-
-;; (produce
-;; (let ((x (lvar))) (:- (p x) (q x)))
-;; (vector (! (q 1))))
-
-;; (:- (p (lvar 'x)) (q (lvar 'x)) (s 1))
-
-;; (:- (p (lvar 'x)) (q (lvar 'x)))
-
-;; (produce
-;; (:- (p (lvar 'x)) (q (lvar 'x)) (s (lvar)))
-;; (vector (! (q 2))
-;; (! (s 3))))
+;; # Algebraic Naive Evaluation
+;;
+;; The implemented evaluator computes the fixpoint of a system of algebraic equation (relational algebra).
+;;
+;; Clauses are first translated to relational algebra expressions, formulated as
+;; a system of equations and resolved until the solutions sets stabilize (a
+;; fixpoint is found).
+;;
+;; This is a naive implementation with much room for optimization, clean-up and
+;; fixing.
;; Transform clause to relational expression
-
(define (substitute-constants atoms)
"Returns a substitution that replaces all constants in the atoms with fresh logical variables"
(vector-fold
@@ -288,6 +246,7 @@
(define (clause->relational-expr clause)
+ "Transform a Datalog clause to a Relational Algebra expression."
(let* ( ;; normalize clause to remove constants and duplicate lvars in head
(clause (normalize-head clause))
;; susbstitute constants in body with fresh variables
@@ -313,21 +272,9 @@
base-cartesian-product
substitution))))
-(define* (vhash-ref key vhash #:key (default #f))
- (cond
- ((vhash-assoc key vhash) (cdr (vhash-assoc key vhash)))
- (else default)))
-
-(define (vhash-map proc vhash)
- (vhash-fold
- (lambda (key value result)
- (vhash-cons
- key (proc key value)
- result))
- vlist-null
- vhash))
(define (clauses->relational-expr clauses)
+ "Transfrom a VHash of Datalog clauses (keys are predicate symbols and values are VLists of clauses) to a system of Relational Algebra expressions."
(vhash-map
(lambda (predicate clauses)
(apply ra:make-union
@@ -338,6 +285,7 @@
clauses))
(define (sort-clauses clauses)
+ "Sort a list of clauses by predicate symbol of head. Returns a VHash with predicate symbol as keys."
(fold
(lambda (clause result)
(let ((predicate (atom-predicate (clause-head clause))))
@@ -350,6 +298,7 @@
clauses))
(define (make-evaluation-context clauses)
+ "Creates a VHash from predicate symbols in list of clauses to empty sets."
(fold
(lambda (clause result)
(let ((head (clause-head clause)))
@@ -362,6 +311,7 @@
;; Algebraic Naive Evaluation (Section 9.1.1 of Logic Programming and Databases)
(define (datalog-eval clauses)
+ "Evaluate a Datalog program"
(let ((relational-exprs (clauses->relational-expr (sort-clauses clauses))))
(let loop ((context (make-evaluation-context clauses)))
@@ -377,21 +327,3 @@
(if (cdr context+changes?)
(loop (car context+changes?))
context)))))
-
-
-(set->list
- (vhash-ref
- 'path
- (datalog-eval
- (list
- (:- (path (lvar 'x) (lvar 'y)) (path (lvar 'x) (lvar 'z)) (edge (lvar 'z) (lvar 'y)))
- (:- (path (lvar 'x) (lvar 'y)) (edge (lvar 'x) (lvar 'y)))
- (! (edge 0 1))
- (! (edge 1 2))
- (! (edge 2 4))
- (! (edge 4 5))
- (! (edge 2 3))
- (! (edge 3 6))))))
-
-;; ;; (clause-head
-;; (:- (path (lvar 'a) (lvar 'b)) (edge (lvar 'a) (lvar 'c)) (path (lvar 'c) (lvar 'c))))
diff --git a/tests/schemantic/datalog.scm b/tests/schemantic/datalog.scm
index fc15766..617c5a0 100644
--- a/tests/schemantic/datalog.scm
+++ b/tests/schemantic/datalog.scm
@@ -5,7 +5,11 @@
(define-module (tests schemantic datalog)
#:use-module (schemantic lvar)
#:use-module (schemantic datalog)
+ #:use-module (schemantic datalog vhash-set)
+ #:use-module (ice-9 vlist)
+
+ #:use-module (srfi srfi-43)
#:use-module (srfi srfi-64))
(test-begin "datalog")
@@ -22,4 +26,34 @@
(clause?
(! (p 2))))
+;; Example
+
+;; A Datalog program that computes reachability (path) in a graph.
+(define graph-program
+ (list
+ (:- (path (lvar 'x) (lvar 'y)) (path (lvar 'x) (lvar 'z)) (edge (lvar 'z) (lvar 'y)))
+ (:- (path (lvar 'x) (lvar 'y)) (edge (lvar 'x) (lvar 'y)))
+ (! (edge 0 1))
+ (! (edge 1 2))
+ (! (edge 1 3))
+ (! (edge 4 5))
+ (! (edge 5 6))))
+
+(define paths
+ (cdr (vhash-assoc 'path (datalog-eval graph-program))))
+
+(test-assert "Graph has 8 paths"
+ (eq? 8 (set-size paths)))
+
+(test-assert "All edges are a path"
+ (and
+ (set-contains? paths (vector 0 1))
+ (set-contains? paths (vector 1 2))
+ (set-contains? paths (vector 1 3))
+ (set-contains? paths (vector 4 5))
+ (set-contains? paths (vector 5 6))))
+
+(test-assert "Node 3 is reachable from 0"
+ (set-contains? paths (vector 0 3)))
+
(test-end "datalog")