```
))}
@index[hashtable (representation)]@t[hashtable]@\A binary relation stored in a hashtable
in which the domain of the relation serves as the index for accessing a list of values.
@*@t{:representation (hashtable @i(
``````
))}
@index[array (representation)]@t[array]@\A relation stored as
an array whose dimensions are one less than the arity of the relation.
Such a relation relates array indices to a list
of values stored in the array at those indices.
@*@inlineprogramexample{:representation (array @i(
``````
))}
@end(description)
Analogous representations (called @t[globalvar-single], @t[defstruct-single] and so forth)
are supplied for cases where at most one value is to be stored.
@Begin(ProgramExample)
(defvar *dictionary* (make-hash-table))
(DefRelation dictionary-entry
:types (symbol string)
:representation (hashtable-single *dictionary*))
(++ dictionary-entry
'arity "the number of objects in each tuple of a relation")
@End(ProgramExample)
@comment[Examples***]
@SECTION(Notational shortcuts)
@label(shortcuts)
AP5 provides a syntax in which variables (introduced by quantifiers or
descriptions) can be restricted to values of a particular type. The
character @index[# (within a variable name)]@indexsecondary[primary="wff syntax",secondary="#"]"#" is reserved to express this
restriction. Variables of the form @i[type#name] translate as a
variable named @i[name] restricted to values of type @i[type]. The name
may also be omitted in which case @i[type] will also be
used as the variable name, thus @i[type#] translates as a variable named
@i[type] of type @i[type]. This way of introducing a type restriction is equivalent to supplying
the type restriction explicitly.
@begin(programexample)
((x) s.t. (person x)) @math[@eqv] ((person#x) s.t. TRUE)
((x y) s.t. (and (hourly-employee x)(office x y)))
@math[@eqv] ((hourly-employee#x y) s.t. (office x y))
(?? E (x) (and (hourly-employee x)(office-mate 'Jim x)))
@math[@eqv] (?? E (hourly-employee#x)(office-mate 'Jim x))
@end(programexample)
For certain generator macros, @t[any], @t[theonly] and @t[listof], and the @t[set-listof] macro,
a relation name can be substituted as a shorthand for the corresponding spliced-in description.
@Begin(ProgramExample)
(any (p) s.t. (person p)) @math[@eqv] (any person)
(listof (p n) s.t. (office p n)) @math[@eqv] (listof office)
(set-listof (x y) s.t. (forward-phone x y) '((333 123)(123 542)(405 239)))
@math[@eqv] (set-listof forward-phone '((333 123)(123 542)(405 239)))
@End(ProgramExample)
Within a wff, the symbol @index[$ (within a wff)]@indexsecondary[primary="wff syntax",secondary="$"]"$" can be used as a shorthand to introduce additional
existentially quantified variables. Multiple usages of "$" need not
refer to the same value.
@Begin(ProgramExample)
((x) s.t. (E (y) (extension x y))) @math[@eqv] ((x) s.t. (extension x $))
@End(ProgramExample)
@SubHeading(Wff macros)
The syntax of wffs can be extended by macros. In contexts where a wff is
expected, a list whose initial symbol is not a known relation name or
piece of wff syntax will be macroexpanded and the result treated as a wff.
Predefined wff macros include:
@Begin(Description, leftmargin 20, indent -20)
@indexsecondary[primary="wff syntax",secondary="Implies"]@index[implies (wff macro)]
(@t[Implies] @i(wff1 wff2))@\@math[@eqv] (OR (NOT @i(wff1)) @i(wff2))
@indexsecondary[primary="wff syntax",secondary="Equiv"]@index[equiv (wff macro)]
(@t[Equiv] @i(wff1 wff2))@\@math[@eqv] (AND (implies @i(wff1) @i(wff2))
(implies @i(wff2) @i(wff1)))
@indexsecondary[primary="wff syntax",secondary="Xor"]@index[xor (wff macro)]
(@t[Xor] @i(wff1 wff2))@\@math[@eqv] (NOT (equiv @i(wff1) @i(wff2)))
@indexsecondary[primary="wff syntax",secondary="If-Then-Else"]@index[If-Then-Else (wff macro)]
(@t[If-Then-Else] @i(wff1 wff2 wff3))@\@math[@eqv] (OR (AND @i(wff1) @i(wff2))
(AND (NOT @i(wff1))(@i(wff3))))
@indexsecondary[primary="wff syntax",secondary="Exists"]@index[exists (wff macro)]
(Exists @i(vars wff))@\@math[@eqv] (E @i(vars wff))
@indexsecondary[primary="wff syntax",secondary="All"]@index[all (wff macro)]
(All @i(vars wff))@\@math[@eqv] (A @i(vars wff))
@End(Description)
@indexsecondary[primary="wff syntax",secondary="Funcall"]@index[funcall (wff macro)]
@indexsecondary[primary="wff syntax",secondary="Apply"]@index[apply (wff macro)]
In addition, the wff macros @t[funcall] and @t[apply] are defined in a manner analogous to
their Lisp counterparts. In contexts where a wff is
expected, a list whose car is the symbol @t[funcall] is translated by
evaluating the second element and treating the result as a relation to be applied to
the values of the remaining arguments comprising the list. Similarly, a list whose car is the symbol
@t[apply] is translated by evaluating the second element and treating the result as a
relation to be applied to the argument list that results when a list of the values of all
but the last of the remaining arguments is appended to the value
of the last remaining argument.
@SECTION(The AP5 Computation Model)
The following brief description of the @index[AP5 computation model]AP5
computation model is intended to supplement the earlier discussion of
database updates, atomic transitions, and rules. The computation model
used by AP5 layers a coarse-grained cycle over the fine-grained cycle of
computations defined by Common Lisp. This cycle, shown in Figure
@ref(Computation-Model-Figure), begins when an application proposes one
or more updates to the database (an atomic transition) and ends
when either the transition is aborted or the updates are transacted,
resulting in the next consistent state of the database and the execution
of any computations specified by automation rules that have been
triggered.
@begin(figure)
@blankspace(5 inches)
@caption(The AP5 Computation Model)
@tag(Computation-Model-Figure)
@end(figure)
The initial set of proposed changes to the database consists of
assertions or deletions of facts, i.e., primitive wffs involving transition
relations, where updates of derived relations have been translated into updates
of transition relations.
A @i[consistency manager] examines the proposed changes, aborts if there
are contradictory updates (assertion and deletion of the same fact) and
otherwise executes one or more consistency cycles. Within a consistency
cycle, the changes to the database are simulated resulting in a
potential state of the database, which is accessible only to the
consistency manager. The consistency manager then determines if any
constraints would be violated by this potential state transition.
If not, the consistency cycle is finished, the database is updated
(but not yet made accessible to other processes) and
control is passed to the automation manager.
If there are consistency violations, any associated repair procedures
are collected and executed in the context of the potential state
transition. These repair procedures cannot alter the proposed set of updates
except by supplying additional proposed updates (or aborting) and may
access the current or proposed database states. Unless contradictory updates
have been introduced, the consistency manager then executes another
consistency cycle with the modified set of proposed changes. This cycling
will continue until the transition succeeds (there are no more
violations of consistency rules) or aborts (a rule explicitly aborts or there are contradictory
updates or there are consistency violations but the set of proposed changes
is unchanged from the previous cycle) or some set limit
of cycles is exceeded.
An @i[automation manager] carries out the final steps of the computation
cycle. It examines the successful state transition, finds any
automation rules triggered by the transition and gathers a set of
pending automation procedures. Automation rules specify procedures to
be enqueued. The new database state is now made
accessible to all processes and the enqueued automation procedures are
executed. When the queue is empty, the application that initiated the
transition is allowed to resume.
@appendix(Defining, saving and restoring @index(worlds)Worlds)
@label(worldssection)
@comment[see pet-food:>Worlds>documentation>version5.mss]
Worlds is an augmentation
of AP5 that provides for the persistance and sharing of subsets of
a database. Briefly, Worlds allows a user to specify
the subset of interest (called a worldspec). This worldspec is then
instantiated as a structure, called a world, that can be populated with facts comprising
the specified subset. A world can be named and associated with a creator.
A particular state of a world
can be saved to disk or restored. More details are
available in the Worlds Manual @cite(Worldsmanual).
Some relevant functions are:
@multi{name=createworldspec, args="name comment exporttypes importtypes spec",
keys=" :creator", type=Function}
@linkedtext{@t[Createworldspec] defines and saves a specification for a world.}
@multi{name=createworld, args="name comment worldspec", keys=" :creator :seedset :savepath",
type=Function}
@linkedtext{@t[Createworld] actually creates and saves a world according to a worldspec.
When specified, the @t[:seedset] is a unary description which identifies objects that
serve to seed the world in that their associated relations with other objects constitute the
world.}
@t[populate @i[world] &key :in :out]@>[@i(Function)]
@linkedtext{@t[Populate] puts objects into an existing world.}
@t[save @i[world] &key :batch :comment]@>[@i(Function)]
@linkedtext{@t[Save] saves the current state of a world.}
@t[commit @i[world] &key :batch :comment]@>[@i(Function)]
@linkedtext{@t[Commit] puts objects into an existing seeded world and saves that world.}
@t[restore] @i[world] &key :targetstate :frombatch]@>[@i(Function)]
@linkedtext{@t[Restore] restores the state of a world previously saved.}
@t[loadworld @i[name] &key :creator]@>[@i(Function)]
@linkedtext{@t[Loadworld] loads a previously created world (but unlike @t[restore] the world is unpopulated).}
@t[loadworldspec @i[name] &key :creator]@>[@i(Function)]
@linkedtext{@t[Loadworldspec] loads previously defined worldspecs.}
@comment[ In(world entity) internal or exported
Relations and basetypes
name (dbobject string-or-symbol)
creator (world-or-worldspec string)
name and creator are strings that are used as identifiers]
@Begin(Group)
Here are some of the transition relations we have defined in the examples:
@begin(programexample)
(DefRelation person
:types (symbol)
:documentation "(Person x) an object representing a person.")
(DefRelation office-number
:types (integer)
:definition ((x) s.t. (integer-in-range x 1 99))
:documentation "(Office-number i) an integer from 1 to 99 inclusive")
(DefRelation office
:types (person office-number)
:count ((person output) :countspec :optional))
:documentation "(Office person number) associates a person with
that person's office number.")
(DefRelation office-phone
:types (office-number ((i) s.t. (integer-in-range i 100 999)))
:count ((output integer) :countspec :optional))
:documentation "The office-phone relation associates an office (actually
an office number) with a number that is the
office's phone number.")
(DefRelation forward-phone
:arity 2
:documentation "Forward-phone models the association between phone
numbers when a phone is forwarded.")
(set-listof (p) s.t. (person p)
'(John Amy Jane Dave Fred Mary Jim Mark))
(set-listof (o n) s.t. (office o n)
'((John 18) (Amy 24) (Jane 16) (Dave 10)
(Fred 18) (Mary 24) (Jim 12) (Mark 14)))
(set-listof (x y) s.t. (office-phone x y)
'((10 123) (12 333) (14 542) (16 234)
(18 562) (20 405) (22 239) (24 342)))
(set-listof (x y) s.t. (forward-phone x y)
'((333 123) (123 542) (405 239)))
@End(ProgramExample)
@End(Group)
@Begin(Group)
The following is an example of the use of WORLDS to save and restore the
data in the above relations. First we define a specification for the world:
@Begin(ProgramExample)
(setq testworldspec
(createworldspec
"test"
"Worldspec used as a example in the training manual"
nil
nil
'((:internal
(person
(office @@ $))
(phone-number
(office-phone @@ $)
(forward-phone @@ $))))
:creator "user"))
@End(ProgramExample)
@End(Group)
Then we create an instance of the world and populate it:
@Begin(ProgramExample)
(setq testworld
(createworld
"testworld"
"World used as an example in the training manual"
testworldspec
:creator "user"))
(populate testworld :in (listof (o) s.t. (E (n) (office o n))))
@End(ProgramExample)
We can now save this state of the world:
@Begin(ProgramExample)
(save testworld :batch t :comment "Initial testworld")
@end(programexample)
Change the data of these relations:
@Begin(ProgramExample)
(set-listof (p) s.t. (person p)
'(John Amy Fred Mary Wanda Bill))
(set-listof (o n) s.t. (office o n)
'((John 10) (Amy 12) (Fred 12)
(Mary 16) (Wanda 20) (Bill 24)))
(listof (p) s.t. (office p '12)) => (Fred Amy)
@End(ProgramExample)
Save the new state of the world:
@Begin(ProgramExample)
(save testworld :batch t :comment "Second testworld")
@end(programexample)
And now restore the former state of the world:
@Begin(ProgramExample)
(setq target (any (s) s.t. (and (state testworld s)
(comment s "Initial testworld"))))
(wor::restore (loadworld "testworld" :creator "user" :targetstate target))
(listof (p) s.t. (office p '12))
=> '(MARK)
@end(programexample)
@Appendix(Glossary)
@begin(description, font smallbodyfont, leftmargin +20, indent -20, spread .5)
@i(annotation)@\optional declarations in a specification that address representation
and efficiency concerns rather than functionality
@i(arity)@\the number of objects in each tuple of a relation
@i(atomic transition)@\change to a database in which one or more data updates are treated as a single step
@i(automation rule)@\rule that invokes some computation in response to a database transition that matches a
specified pattern
@i(compound-wff)@\wff containing a quantifier, connective or temporal operator
@i(computed relation)@\unchanging relation defined in terms of arbitrary Lisp computations
@i(consistency rule)@\rule that enforces conditions on the database by
signaling an error or attempting to carry out a repair procedure
@i[count constraint]@\idiomatic consistency rule that restricts the cardinality of certain projections of
the tuples of a relation
@i(defined relation)@\derived relation specified by a ground description
@i(derivation idiom)@\predefined syntax for methods which derive or compute relations
from other relations and Lisp computations
@i(derived relation)@\potentially changing relation defined in terms of other relations that are
either transition relations or less derived relations
@i(description)@\list of the form @t[(@i(vars) s.t. @i(wff))] that can serve as a relation
@i(generator)@\procedure that iterates through the tuples of a relation or description
@i(ground description)@\description having the property that all of the
operands of its constituent primitive wffs are constants, quantified
variables, or variables from from the variable list of the description
@i(n-tuple)@\sequence of n objects
@i(object)@\any value that can be stored in a variable
@i(primitive-wff)@\wff whose car is a relation name and whose cdr is list whose length is equal to the arity of the relation
@i(relation)@\(possibly infinite) set of tuples that are all the same length
@i(representation)@\data structure for a transition relation
@i(rule)@\mechanism that reacts to changes or proposed changes to the database
@i(specification)@\detailed functional description of a system
@i(transition relation)@\relation whose contents are defined by database updates
@i(tuple)@\sequence of objects
@i(type)@\relation whose arity is 1
@i[type constraint]@\idiomatic consistency rule that restricts the types of the operands of a relation
@i(well-formed formula)@\expression in first order logic
@Comment<@i(wff)@\well-formed formula>
@end(description)
@COMMENT[Queries that contain vars translate into generators
(?? e (x) (= x 5)) translates to (forany (x) s.t. (= x 5) T ifnone NIL)
]
```