Logic Programming for Racket
The logic-programming library provides a prolog-like language that can be used within
racket programs. Both queries and knowledgebases are s-expressions that can be manipulated programmatically,
rather than having a single knowledgebase. The library is intended for racket programs that just need to do a bit
of logic, rather than for writing full programs in the provided language. See also the Parenlog package,
which puts less focus on programmatic modification of knowledgebases.
1 Example of Use
Take the ‘hello world’ of formal logic:
1. Socrates is a man
2. Men are mortal
3. Therefore, Socrates is mortal
We can express 1 and 2 as a knowledgebase like so:
|> (define knowledgebase|
| '((man socrates)|
| (:- (mortal X)|
| (man X))))|
Note that we can’t capitalise Socrates’ name because that would make him a variable. :- might be read "if".
Now we can make queries about that information, asking questions such as "is Socrates mortal?":
|> (query '(mortal socrates) knowledgebase)|
The result is a set of requirements for the query to be true, so an empty set means that it’s unconditionally true.
If instead we ask "is Plato mortal?":
|> (query '(mortal plato) knowledgebase)|
we get #f
- indicating not of course that Plato is provably immortal, but that given the information in
knowledgebase he can’t be proven to be mortal. The distinction between provably false and unprovable is very
important in logic programming, don’t forget that the question answered by query
is ’is this provable?’.
We can also ask other questions, like "who is mortal?":
|> (query '(mortal X) knowledgebase)|
(set (ec '(X) 'socrates))
and "what is Socrates?" (note the use of query-all
because there’s more than one answer):
|> (query-all '(X socrates) knowledgebase)|
(list (set (ec '(X) 'man)) (set (ec '(X) 'mortal)))
2 Racket Reference
This section details the bindings provided by the library. The details of the logic language are in the section below.
Returns #t if v is a symbol whose first character is an uppercase letter, #f otherwise.
Like prolog, variables are represented as such symbols.
Returns the necessary values that variable?
s must take to render all the p
s equivalent, in
the form of a set
s, or #f
if no variable binding could achieve that, given
that the bindings in vars
are already fixed. Note that vars
is the sort of thing
that both unify
etc return, and that each of the p
s is a predicate
in the logic language.
Returns the necessary variable?
bindings to make q
provable given kb
if it can’t be done. See below for the semantics of q
. If trace?
is true, it will print debugging information in the form "TRACE: calling <subgoal>, [<current variable bindings>]"
for each subgoal. Note that since the logic language is turing-complete, it can’t be guaranteed that
Some queries have more than one possible solution. query-gen
works like query
except that it returns a generator which takes no arguments and yields each solution in turn. Once
it runs out, it yields #f
Works like query-gen
, except that instead of returning a generator it returns a list containing
every possible solution at once, in the order they would be returned by query-gen
. Note that
it’s possible for a query to have infinitely many solutions, and in that case query-all
| #:extra-constructor-name make-ec)|
| vars : (listof? variable?)|
| val : any/c|
Stands for Equivalence Class. Semantically, it represents a claim that all the members of vars
are equivalent to one another and that if val
is not #f
then they’re also equivalent to
is stored separately because it’s not possible for two different nonvariable
values to be equivalent. set
s of ec
s are returned by functions like query
represent the necessary equivalences to make a statement true.
3 Language Reference
The logic language provided by this library is very similar to prolog. Since it’s unlikely someone
interested in using it won’t have some prolog experience, it’ll be easiest to describe the differences.
For use, see Example of Use.
An s-expression syntax is used. Facts and Queries are written '(predicate-name arg1 ... argn), and
Rules are written '(:- (predicate-name arg1 ... argn) body), where body is a Fact (using ‘,’
and ‘;’ for ‘and’ and ‘or’ is not possible, a Rule might look like '(:- (p X) (and (q X) (r X)))).
Don’t forget to quote literal sections of this code before using it, there’s no binding provided for
:- or anything.
3.2 defined predicates
There are only five defined predicates (or six if you count :-):
and: '(and p q) is like p,q in prolog
or: '(or p q) is like p;q in prolog
unprovable: equivalent to prolog’s not.
WARNING: if you’re not familiar with it, prolog’s not can be fairly unintuitive. Hopefully unprovable better expresses what’s meant by it.
\\=: equivalent to prolog’s \=. The double slash is because racket allows backslash escapes in symbols, so without it it’d be the same as =
=: equivalent to prolog’s =. If it weren’t defined by default, it could be produced by adding '(= X X) to a knowledgebase.
Note especially that ! is missing from this list, no cut is provided.