Datalog docs

This commit is contained in:
Jay McCarthy 2010-06-25 17:07:53 -06:00
parent c1e7bf62f7
commit e8ef7dcaa5
12 changed files with 140 additions and 99 deletions

View File

@ -3,18 +3,21 @@
scribble/eval
scribble/basic
scribble/bnf
(for-label racket/base
racket/contract
"../main.rkt")
"utils.rkt")
@title[#:tag "top"]{@bold{Datalog}: Deductive database programming}
@author[(author+email "Jay McCarthy" "jay@racket-lang.org")]
This package contains a lightweight deductive database system. Queries and database updates are expressed
using @link["http://en.wikipedia.org/wiki/Datalog"]{Datalog}---a declarative logic language in which each
@link["http://en.wikipedia.org/wiki/Datalog"]{Datalog} is
@itemize[
@item{a declarative logic language in which each
formula is a function-free Horn clause, and every variable
in the head of a clause must appear in the body of the clause. The use of Datalog syntax and an implementation based
in the head of a clause must appear in the body of the clause.}
@item{a lightweight deductive database system where queries and database updates are expressed
in the logic language.}
]
The use of Datalog syntax and an implementation based
on tabling intermediate results ensures that all queries terminate.
@table-of-contents[]
@ -23,10 +26,6 @@ on tabling intermediate results ensures that all queries terminate.
@defmodulelang[datalog]
XXX Progress
@subsection{Datalog Syntax}
In Datalog input, whitespace characters are ignored except when they separate adjacent tokens or when they occur in strings.
Comments are also considered to be whitespace. The character @litchar["%"] introduces a comment, which extends to the next line break.
Comments do not occur inside strings.
@ -70,17 +69,7 @@ END
A program is a sequence of zero or more statements. A statement is an assertion, a retraction, or a query. An assertion is a clause followed by
a period, and it adds the clause to the database if it is safe. A retraction is a clause followed by a tilde, and it removes the clause from
the database. A query is a literal followed by a question mark. The effect of reading a Datalog program is to modify the database as directed
by its statements, and then to return the literal designated as the query. If no query is specified, a reader returns a literal know to have no
answers. The following is a program:
@verbatim[#:indent 4 #<<END
edge(a, b). edge(b, c). edge(c, d). edge(d, a).
path(X, Y) :- edge(X, Y).
path(X, Y) :- edge(X, Z), path(Z, Y).
path(X, Y)?
END
]
the database. A query is a literal followed by a question mark.
The following BNF describes the syntax of Datalog.
@ -122,38 +111,66 @@ The following BNF describes the syntax of Datalog.
(nonterm "STRING"))
]
The effect of running a Datalog program is to modify the database as directed
by its statements, and then to return the literals designated by the query.
The following is a program:
@verbatim[#:indent 4 #<<END
#lang datalog
edge(a, b). edge(b, c). edge(c, d). edge(d, a).
path(X, Y) :- edge(X, Y).
path(X, Y) :- edge(X, Z), path(Z, Y).
path(X, Y)?
END
]
Currently, REPL interaction is not supported.
@section{Parenthetical Datalog Module Language}
@(require (for-label datalog/sexp/lang))
@defmodulelang[datalog/sexp]
XXX Progress
The semantics of this language is the same as the normal Datalog language, except it uses a @secref["parenstx"].
@subsection{Parenthetical Datalog Syntax}
Literals are represented as S-expressions with identifiers for constant symbols, strings for constant strings, and @racket[,id] for variable symbols.
@racketgrammar*[
#:literals (:- ! ~ ? unquote)
[program (begin statement ...)]
[statement assertion
retraction
query]
[assertion (! clause)]
[retraction (~ clause)]
[query (? literal)]
[clause (:- literal literal ...)
literal]
[literal (datum term ...)]
[term variable
constant]
[variable ,symbol]
[constant datum]
[datum symbol
string]]
@racket[unquote], top-level identifiers, and strings are not otherwise allowed in the program.
The following is a program:
@racketmod[datalog/sexp
(! (edge a b))
(! (edge b c))
(! (edge c d))
(! (edge d a))
(! (:- (path ,X ,Y)
(edge ,X ,Y)))
(! (:- (path ,X ,Y)
(edge ,X ,Z)
(path ,Z ,Y)))
(? (path ,X ,Y))]
@subsection[#:tag "parenstx"]{Parenthetical Syntax}
@defmodule[datalog/sexp/lang]
@defform[(! clause)]{ Asserts the clause. }
@defform[(~ clause)]{ Retracts the literal. }
@defform[(? literal)]{ Queries the literal and prints the result literals. }
@defform[(:- literal literal ...)]{ A conditional clause. }
@defform[(= term term)]{ An equality literal. }
@defform[(unquote symbol)]{ A variable symbol. }
@include-section["racket.scrbl"]
@section{Acknowledgments}
This package is structurally based on Dave Herman's @racketmodname[(planet dherman/javascript)] library and
This package was once structurally based on Dave Herman's @racketmodname[(planet dherman/javascript)] library and
John Ramsdell's @link["http://www.ccs.neu.edu/home/ramsdell/tools/datalog/datalog.html"]{Datalog library}.
The package uses the tabled logic programming algorithm described in

View File

@ -12,6 +12,8 @@
@defmodule[datalog]
The Datalog database can be directly used by Racket programs through this API.
@examples[#:eval the-eval
(define example-program
#<<END
@ -589,6 +591,13 @@ This library provides facilities for evaluating Datalog. It can be required via:
"path(X, Y) :- edge(X, a).")))]
}
@defproc[(eval-top-level-statement [s statement/c])
void]{
Evaluates @racket[s] using @racket[(current-theory)] as the @tech{theory}, printing query answers if @racket[s] is a query.
This will raise a syntax error if given an @racket[assertion] of a @racket[clause] that is not a @racket[safe-clause?].
}
@defproc[(eval-statement [s statement/c])
(or/c void (listof literal?))]{
Evaluates @racket[s] using @racket[(current-theory)] as the @tech{theory}.

View File

@ -1,23 +1,31 @@
#lang racket
(require (for-syntax syntax/parse)
racket/stxparam
"../eval.rkt"
"../ast.rkt")
(define-syntax (top stx)
(define-syntax-parameter top
(λ (stx) (raise-syntax-error '#%top "undefined identifier" stx)))
(define-syntax-parameter unquote
(λ (stx) (raise-syntax-error 'unquote "only allowed inside literals" stx)))
(define-syntax-parameter datum
(λ (stx) (raise-syntax-error '#%datum "only allowed inside literals" stx)))
(define-syntax (literal-top stx)
(syntax-parse
stx
[(_ . sym:id)
(quasisyntax/loc stx
(constant #'#,stx 'sym))]))
(define-syntax (unquote stx)
(define-syntax (literal-unquote stx)
(syntax-parse
stx
[(_ sym:id)
(quasisyntax/loc stx
(variable #'#,stx 'sym))]))
(define-syntax (datum stx)
(define-syntax (literal-datum stx)
(syntax-parse
stx
[(_ . sym:str)
@ -32,10 +40,17 @@
(literal #'#,stx 'sym empty))]
[(_ (sym:id e ...))
(quasisyntax/loc stx
(literal #'#,stx 'sym (list e ...)))]))
(literal #'#,stx 'sym
(syntax-parameterize ([top (make-rename-transformer #'literal-top)]
[datum (make-rename-transformer #'literal-datum)]
[unquote (make-rename-transformer #'literal-unquote)])
(list e ...))))]))
(define-syntax (->simple-clause stx)
(syntax-case stx ()
(syntax-case stx (:-)
[(_ (:- . r))
(quasisyntax/loc stx
(:- . r))]
[(_ e)
(quasisyntax/loc stx
(clause #'#,stx (->literal e) empty))]))
@ -44,10 +59,8 @@
(syntax-case stx ()
[(_ head body ...)
(quasisyntax/loc stx
(eval-top-level-statement
(assertion #'#,stx
(clause #'#,stx (->literal head)
(list (->literal body) ...)))))]))
(list (->literal body) ...)))]))
(define-syntax-rule (define-paren-stx op struct)
(define-syntax (op stx)
@ -65,12 +78,14 @@
(quasisyntax/loc stx
(eval-top-level-statement (query #'#,stx (->literal c))))]))
(provide (rename-out [top #%top]
[datum #%datum]
#;[module-begin #%module-begin]
#;[top-interaction #%top-interaction])
(define-syntax (= stx)
(quasisyntax/loc stx
(constant #'#,stx '=)))
(provide (rename-out [top #%top]
[datum #%datum])
#%top-interaction
#%module-begin
! ~ ?
:-
:- =
unquote)

View File

@ -1,11 +1,11 @@
#lang datalog/sexp
; Equality test
(:- (ancestor ,A ,B)
(parent ,A ,B))
(:- (ancestor ,A ,B)
(! (:- (ancestor ,A ,B)
(parent ,A ,B)))
(! (:- (ancestor ,A ,B)
(parent ,A ,C)
(= D C) ; Unification required
(ancestor ,D ,B))
(ancestor ,D ,B)))
(! (parent john douglas))
(! (parent bob john))
(! (parent ebbon bob))

View File

@ -4,12 +4,12 @@
(! (edge b c))
(! (edge c d))
(! (edge d a))
(:- (path ,X ,Y)
(edge ,X ,Y))
(:- (path ,X ,Y)
(! (:- (path ,X ,Y)
(edge ,X ,Y)))
(! (:- (path ,X ,Y)
(edge ,X ,Z)
(path ,Z ,Y))
(:- (path ,X ,Y)
(path ,Z ,Y)))
(! (:- (path ,X ,Y)
(path ,X ,Z)
(edge ,Z ,Y))
(edge ,Z ,Y)))
(? (path ,X ,Y))

View File

@ -2,12 +2,12 @@
; Laps Test
(! (contains ca store rams_couch rams))
(! (contains rams fetch rams_couch will))
(:- (contains ca fetch ,Name ,Watcher)
(! (:- (contains ca fetch ,Name ,Watcher)
(contains ca store ,Name ,Owner)
(contains ,Owner fetch ,Name ,Watcher))
(contains ,Owner fetch ,Name ,Watcher)))
(! (trusted ca))
(:- (permit ,User ,Priv ,Name)
(! (:- (permit ,User ,Priv ,Name)
(contains ,Auth ,Priv ,Name ,User)
(trusted ,Auth))
(trusted ,Auth)))
(? (permit ,User ,Priv ,Name))

View File

@ -4,9 +4,9 @@
(! (edge b c))
(! (edge c d))
(! (edge d a))
(:- (path ,X ,Y)
(edge ,X ,Y))
(:- (path ,X ,Y)
(! (:- (path ,X ,Y)
(edge ,X ,Y)))
(! (:- (path ,X ,Y)
(edge ,X ,Z)
(path ,Z ,Y))
(path ,Z ,Y)))
(? (path ,X ,Y))

View File

@ -1,8 +1,8 @@
#lang datalog/sexp
; p q test from Chen & Warren
(:- (q ,X)
(p ,X))
(! (:- (q ,X)
(p ,X)))
(! (q a))
(:- (p ,X)
(q ,X))
(! (:- (p ,X)
(q ,X)))
(? (q ,X))

View File

@ -4,9 +4,9 @@
(! (edge b c))
(! (edge c d))
(! (edge d a))
(:- (path ,X ,Y)
(edge ,X ,Y))
(:- (path ,X ,Y)
(! (:- (path ,X ,Y)
(edge ,X ,Y)))
(! (:- (path ,X ,Y)
(path ,X ,Z)
(edge ,Z ,Y))
(edge ,Z ,Y)))
(? (path ,X ,Y))

View File

@ -1,7 +1,7 @@
#lang datalog/sexp
(! (tpme tpme1))
(! (ms m1 "TPME" tpme1 ek tp))
(:- (says ,TPME ,M)
(! (:- (says ,TPME ,M)
(tpme ,TPME)
(ms ,M "TPME" ,TPME ,A ,B))
(ms ,M "TPME" ,TPME ,A ,B)))
(? (says ,A ,B))

View File

@ -12,11 +12,11 @@
(? (parent ,A ,A))
(:- (ancestor ,A ,B)
(parent ,A ,B))
(:- (ancestor ,A ,B)
(! (:- (ancestor ,A ,B)
(parent ,A ,B)))
(! (:- (ancestor ,A ,B)
(parent ,A ,C)
(ancestor ,C ,B))
(ancestor ,C ,B)))
(? (ancestor ,A ,B))
(? (ancestor ,X john))