notes.txt

			     Design Notes


The purpose of this document is to help people who want to understand
the implementation of the chase program navigate the sources.  Nearly
all module interfaces are documented using OCamldoc.  This
documentation is generated by typing "make" which will produce the
file index.html, and then viewing that file in a browser.  Interface
documentation is not the whole story--important parts of the program
can only be understood by reading module implementation source code.

The code for parsing and printing is straightforward and will be
ignored in this note.  The first module to study is Formula.  It
declares the data structures used to represent geometric formulas.
The motivation for most of the data structures is obvious with the
exception of term.  It contains both structure constants and function
application.  An application of a function symbol to the empty term
list is a formula constant.  When a formula is read, this is how a
constant in a formula is represented.  When a formula is being
instantiated with elements of a structure, the constructor for
structure constants is used.  The function Step.chase performs
instantiation.

The Flatten module should be studied next.  Its interface document
specifies the properties possessed by a formula after flattening.

The Match module makes use of flattened formulas.  It uses streams to
perform all required matches of a conjunction of atomic formulas with
a structure.  For this module, the interface documentation is
insufficient for understanding the code.

The Step module implements a chase step.  Given a structure and a
formula, the step function returns None if the structure satisfies the
formula.  Otherwise it returns a list of structures that have been
extended so as to satisfy the formula.  It makes extensive use of the
Match module.

The Normalize module creates a new structure in normal form from an
old structure augmented with a set of ground formulas and equalities.

The Solve module provides the top-level loop that implements breath
first search for models.

				 ***

[Universal quantifiers in the consequent of formulas has been
implemented.  The new syntax is X = X => p(X) instead of using @.
What follows a description of the design written before it was
implemented.]

Notes on adding the effect of universal quantifiers in the consequent
of formulas.

The proposal is it to add the special unary predicate symbol @ that
can only occur in the antecedent of a formula.  An @ atomic formula
is satisfied by every element in the universe of a structure.  To
write

    forall x, p(x).

a chase programmer would write

    @(X) => p(X).

The @ predicate is expensive.  It's important to implement it in a way
so there is no penalty when it does not occur.  Here is a proposed
design.

1. Add a case of atomic formula for @ atomic formulas.

2. To each structure, add a mutable field called univ that is
initially set to None.

3. When the matcher is asked to match an @ atomic formula, it looks at
the univ field.  If field is None, the domain constants in the extents
of all of the predicate and function symbols in the structure are
collected and formed into a unary trie.  The result is put into the
univ field to avoid recalculation using the Some constructor.  That
trie is returned for matching using the standard matching procedure
for predicate symbols.