Modern Deduction: Post 1

post1.rkt

;; Relational algebra
#lang racket

(define relation? symbol?)
(define atom? symbol?) ;; atomic lits are symbols

;; variables must be explicitly tagged, not 'x, but '(var x)
(define (var? x) (match x [`(var ,(? symbol? x)) #t] [_ #f]))
(define (var-or-atom? x) (or (atom? x) (var? x)))

;; tuples are untagged
(define (tuple? f)
  (match f
    [`((,(? atom?) ...)) #t]
    [_ #f]))

;; facts add a relation name (otherwise how would we know it)
(define (fact? f)
  (match f
    [`((,(? relation? r) ,(? atom?) ...)) #t]
    [_ #f]))

;; notice that ∧ is implicit in the body
(define (rule? r)
  (match r
    [`((,(? relation? head-rel) ,(? var-or-atom?) ...) <-- 
       (,(? relation? body-rels) ,(? var-or-atom?) ...) ...)
     #t]
    [_ #f]))

;; should all be true
(rule? '((p) <--))
(rule? '((r) <-- (q)))
(rule? '((path x y) <-- (edge x x)))
(rule? '((path x y) <-- (edge x y) (path y z)))

;; RA queries
(define (RA-query? q)
  (match q
    [`(literal-tuple ,(? atom? es) ...) #t]
    ;; scan a relation
    [`(scan ,(? relation? R)) #t]
    [`(select from ,(? RA-query?)
              where column ,(? nonnegative-integer?)
              equals ,(? atom?))
     #t]
    ;; natural join on the first N columns, values must be equal
    [`(,(? RA-query? q0) ⋈ ,(? RA-query? q1) on first ,(? nonnegative-integer? N)) #t]
    [`(,(? RA-query? q0) ∪ ,(? RA-query? q0)) #t]
    [`(,(? RA-query? q0) ∩ ,(? RA-query? q0)) #t]
    ;; reorder tuples
    [`(reorder ,(? RA-query? q) ,(? nonnegative-integer?) ...) #t]
    ;; project the first n elements of tuples
    [`(project ,(? RA-query? q) to first ,(? nonnegative-integer? n)) #t]
    ;; need closed-world assumption
    [`(- ,(? RA-query? q)) #t]
    [_ #f]))

;; q: query?
;; db: hashmap from relation name ↦ ℘(Tuple)
;; returns a set of tuples
(define (interpret-query q db)
  (match q
    [`(literal-tuple ,es ...) (set es)]
    [`(scan ,R) (hash-ref db R)]
    [`(select from ,q+ where column ,n equals ,k)
     (list->set (filter (lambda (x) (equal? (list-ref x n) k))
                        (set->list (interpret-query q+ db))))]
    [`(,q0 ∪ ,q1) (set-union (interpret-query q0 db)
                             (interpret-query q1 db))]
    [`(,q0 ∩ ,q1) (set-intersect (interpret-query q0 db)
                                 (interpret-query q1 db))]
    [`(reorder ,q ,order ...)
     (let ([ts (set->list (interpret-query q db))])
       (set->list
        (map (λ (t) (map (λ (i) (list-ref t i)) order))
             ts)))]
    [`(project ,q to first ,n)
     (list->set (map (λ (t) (take t n)) (set->list (interpret-query q db))))]
    [`(,q0 ⋈ ,q1 on first ,N)
     (list->set
      (foldl
       (λ (t0 tups)
         (foldl (λ (t1 tups)
                  (if (equal? (take t0 N) (take t1 N))
                      (set-add tups (append (take t0 N) (drop t0 N) (drop t1 N)))
                      tups))
                tups
                (set->list (interpret-query q1 db))))
       (set)
       (set->list (interpret-query q0 db))))]))

(define (RA-rule? r)
  (match r
    [`(,(? relation? R) ∪= ,(? RA-query? q)) #t]
    [_ #f]))

(define (interpret-rule r db)
  (match-define `(,R ∪= ,q) r)
  (hash-set db R (set-union (hash-ref db R (set)) (interpret-query q db))))

(define (interpret-program rules)
  (define (next-iteration db)
    (foldl (λ (r db) (interpret-rule r db)) db rules))
  (define (do-some-more db)
    (if (equal? db (next-iteration db))
        db
        (do-some-more (next-iteration db))))
  (do-some-more (hash)))

;; relations: hash from relation names to their associated arities
;; herbrand-base is a list of atoms 
(define (herbrand-universe relations herbrand-base)
  ;; generate a cartesian product of arity n with atoms from herbrand-base
  (define (h n)
    (if (= n 0)
        '(())
        (apply append (map (λ (lst) (map (λ (x) (cons x lst)) herbrand-base)) (h (- n 1))))))
  (foldl
   (λ (R acc) (hash-set acc R (h (hash-ref relations R))))
   (hash)
   (hash-keys relations)))

(interpret-query
 '(project (reorder ((reorder (scan edge) 1 0) ⋈ (scan path) on first 1) 1 2 0)
           to first 2)
 (hash 'edge (set '(a b) '(b c) '(c d) '(b e))
       'path (set '(a b) '(b c) '(c d) '(b e))))

(interpret-program
 '((edge ∪= (literal-tuple a b))
   (edge ∪= (literal-tuple b c))
   (edge ∪= (literal-tuple c d))
   (path ∪= (scan edge))
   (path ∪= (project (reorder ((reorder (scan edge) 1 0) ⋈ (scan path) on first 1) 1 2 0)
                     to first 2))))