staged-miniKanren/tests/applications/dl.rkt at main · namin/staged-miniKanren · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
#lang racket/base

(require "../../all.rkt")

;; Adapted from the nnf code in 'The Semantic Web Explained' by Péter
;; Szeredi, Gergely Lukácsy, and Tamás Benkő. Cambridge University
;; Press, 2014.
(define-term-syntax-rule (nnf the-concept)
  `(letrec ((positive?
             (lambda (n)
               (match n
                 [`z #f]
                 [`(s . ,n-1) #t]))))
     (letrec ((add1
               (lambda (n)
                 (cons 's n))))
       (letrec ((sub1
                 (lambda (n)
                   (match n
                     [`(s . ,n-1) n-1]))))
         (letrec ((nnf
                   (lambda (concept)
                     (match concept
                       [`(Not (Not ,c)) (nnf c)]
                       [`(Not (And ,c1 ,c2))
                        (list 'Or (nnf (list 'Not c1)) (nnf (list 'Not c2)))]
                       [`(Not (Or ,c1 ,c2))
                        (list 'And (nnf (list 'Not c1)) (nnf (list 'Not c2)))]
                       [`(Not (Exists ,(? symbol? r) ,c))
                        (list 'All r (nnf (list 'Not c)))]
                       [`(Not (All ,(? symbol? r) ,c))
                        (list 'Exists r (nnf (list 'Not c)))]
                       [`(Not (AtMost ,k ,(? symbol? r)))
                        (list 'AtLeast (add1 k) r)]
                       [`(Not (AtLeast ,k ,(? symbol? r)))
                        (if (positive? k)
                            (list 'AtMost (sub1 k) r)
                            (list 'Not 'Top))]
                       [`(And ,c1 ,c2)
                        (list 'And (nnf c1) (nnf c2))]
                       [`(Or ,c1 ,c2)
                        (list 'Or (nnf c1) (nnf c2))]
                       [`(Exists ,(? symbol? r) ,c)
                        (list 'Exists r (nnf c))]
                       [`(All ,(? symbol? r) ,c)
                        (list 'All r (nnf c))]
                       [concept concept]))))
           (nnf ',the-concept))))))

(record-bench 'eval/program 'staging 'nnf)
(defrel (nnfo concept nnf-concept)
  (time-staged
   (evalo-staged
    (nnf concept)
    nnf-concept)))

(define nnfo-10-results
  `((Not Top)
  ((Not (AtLeast z _.0))
    $$
    ,not-tags0
    (sym _.0))
  (Not (Not (Not Top)))
  ((Not (Not (Not (AtLeast z _.0))))
    $$
    ,not-tags0
    (sym _.0))
  (Not (Not (Not (Not (Not Top)))))
  ((Not (Not (Not (Not (Not (AtLeast z _.0))))))
    $$
    ,not-tags0
    (sym _.0))
  (Not (Not (Not (Not (Not (Not (Not Top)))))))
  ((Not (Not (Not (Not (Not (Not (Not (AtLeast z _.0))))))))
    $$
    ,not-tags0
    (sym _.0))
  (Not (Not (Not (Not (Not (Not (Not (Not (Not Top)))))))))
  ((Not (Not (Not (Not (Not (Not (Not (Not (Not (AtLeast z _.0))))))))))
   $$
   ,not-tags0
   (sym _.0))))

(test
 (length (run 10 (concept)
           (nnfo concept '(Not Top))))
 10)

(test
 (length
  (run 10 (concept)
    (evalo-unstaged
     (nnf concept)
     '(Not Top))))
 10)

;; Normalize something contradictory
(test
  ;; #:times 1000
  (run* (nnf-concept)
    (evalo-unstaged
     (nnf '(Not (AtLeast z hasChild)))
     nnf-concept))
  '((Not Top)))


(test
  ;; #:times 1000
  (run* (nnf-concept)
    (nnfo '(Not (AtLeast z hasChild)) nnf-concept))
  '((Not Top)))

(record-bench 'eval/program 'unstaged 'nnf #:description "Transformation to negation normal form~\\cite{szeredi_lukacsy_benko_nagy_2014} (x1000)")
(time-test
  #:times 1000
  (run* (nnf-concept)
    (evalo-unstaged
     (nnf '(Not (AtMost (s . z) hasChild)))
     nnf-concept))
  '((AtLeast (s s . z) hasChild)))


(record-bench 'eval/program 'staged 'nnf)
(time-test
  #:times 1000
  (run* (nnf-concept)
    (nnfo '(Not (AtMost (s . z) hasChild)) nnf-concept))
  '((AtLeast (s s . z) hasChild)))

(test
;;  #:times 1000
  (run* (nnf-concept)
    (evalo-unstaged
     (nnf '(Not (AtLeast (s s s . z) hasChild)))
     nnf-concept))
  '((AtMost (s s . z) hasChild)))

(test
;;  #:times 1000
  (run* (nnf-concept)
    (nnfo '(Not (AtLeast (s s s . z) hasChild)) nnf-concept))
  '((AtMost (s s . z) hasChild)))