Next: Update Sets and
Up: Static Algebras and
Previous: Appropriate States and
As in first-order logic, the reduct of an ![[Upsilon]](upsilon.xbm)
-state S to a
smaller vocabulary ![[Upsilon^]](_2173_tex2html_wrap1358.xbm)
is the -state S' obtained from S by
``disinterpreting'' function names in
- ;
S is an expansion of S' to .
A carrier is a state whose vocabulary contains only static function
names. The carrier |S| of a state S is the reduct of S to
the static part of Fun(S).
A location over a carrier C is a pair
l = (f, ![[x]](xbar.xbm)
),
where
f is a function name outside of Fun(C)
and 
is a tuple of elements
of C whose length equals the arity of f ; location
l is relational if f is a relation symbol.
](_2173_tex2html_wrap914.xbm)
is the
collection of all locations over C with function names in . An
-state S with carrier C will sometimes be viewed as a function
from ](_2173_tex2html_wrap926.xbm)
to (the superuniverse of) C ; locations of S
are locations in ](_2173_tex2html_wrap932.xbm)
.
If a state S is appropriate for a ground term
= f(![[t]](tbar.xbm)
),
then the location of in S is the location
![(f, Val_S([t]))](_2173_tex2html_wrap942.xbm)
.
An update of a state S is a pair
![[alpha]](alpha.xbm)
= (l,y) , where l is
a location of S and
y 
|S|;
if
l is relational then
y is
Boolean. (More precisely, y belongs to the superuniverse of static
algebra |S|; the looser language is common in logic.) The location
l is the location Loc()
of
, and y is
the value Val()
of . To fire at S , put
y into
the location l ; that is, redefine S to map l to y . The
result is a new state S' such that
Fun(S') = Fun(S),
|S'| = |S|,
S'(l) = y
and
S'(l') = S(l')
for every location l'
of S different from l .