Logic Programming for Racket

8.0

top ← prev up next →

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)
(set)

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)
#f

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

(require logic-programming)

package: logic-programming

This section details the bindings provided by the library. The details of the logic language are in the section below.

procedure
(variable? v) → boolean?
v : any/c

Returns #t if v is a symbol whose first character is an uppercase letter, #f otherwise. Like prolog, variables are represented as such symbols.

procedure
(unify vars p ...) → (or/c (setof? ec?) #f)
vars : (setof? ec?)
p : (not/c #f)

Returns the necessary values that variable?s must take to render all the ps equivalent, in the form of a set of ecs, 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 and query etc return, and that each of the ps is a predicate in the logic language.

procedure
(query q kb [trace?]) → (setof? ec?)
  q : (not/c #f)
  kb : (listof? (not/c #f))
  trace? : boolean? = #f

Returns the necessary variable? bindings to make q provable given kb, or #f if it can’t be done. See below for the semantics of q and kb. 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 query will halt.

procedure
(query-gen q kb [trace?]) → generator?
  q : (not/c #f)
  kb : (listof? (not/c #f))
  trace? : boolean? = #f

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.

procedure
(query-all q kb [trace?]) → (listof? (setof? ec?))
  q : (not/c #f)
  kb : (listof? (not/c #f))
  trace? : boolean? = #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 won’t halt.

struct
(struct ec (vars val)
    #: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 val. val is stored separately because it’s not possible for two different nonvariable values to be equivalent. sets of ecs are returned by functions like query to 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.

3.1 syntax

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.

top ← prev up next →