Datalog docs
original commit: e8ef7dcaa5b9e6d93e801fa149214b73d2d80377
This commit is contained in:
parent
042a0a5dbb
commit
fbeb110aff
|
@ -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
|
||||
|
|
|
@ -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
|
||||
|
@ -588,6 +590,13 @@ This library provides facilities for evaluating Datalog. It can be required via:
|
|||
(open-input-string
|
||||
"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?))]{
|
||||
|
|
|
@ -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) ...)))))]))
|
||||
(clause #'#,stx (->literal head)
|
||||
(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))))]))
|
||||
|
||||
(define-syntax (= stx)
|
||||
(quasisyntax/loc stx
|
||||
(constant #'#,stx '=)))
|
||||
|
||||
(provide (rename-out [top #%top]
|
||||
[datum #%datum]
|
||||
#;[module-begin #%module-begin]
|
||||
#;[top-interaction #%top-interaction])
|
||||
|
||||
[datum #%datum])
|
||||
#%top-interaction
|
||||
#%module-begin
|
||||
! ~ ?
|
||||
:-
|
||||
:- =
|
||||
unquote)
|
Loading…
Reference in New Issue
Block a user