Next: Semantics
Up: Some Other Simple
Previous: Some Other Simple
In , guards were Boolean terms. Now we introduce a separate syntactic
category of guards. Intuitively, guards are first-order formulas with
bound variables. It is intended that bound variables range over finite
domains, though exceptions are possible. Here is a recursive definition:
-
If f is an r -ary relation name and
are terms, then
f() is a guard.
- Any Boolean combination of guards is a guard.
- If g is a guard and U a universe name, then
(
v
U) g
and
(
v
U) g
are guards.
Call a guard closed if it has no free variables. Extend the definition of
basic ealgebras by replacing the condition ``
are Boolean
terms'' with the condition `` are closed guards'' in the
definition of the conditional rule constructor.