In addition to terms, we will define various other syntactic objects, e.g., update instructions and transition rules. We call a state S appropriate for a syntactic object s if Fun(S) includes the collection of function names that occur in s . By default (that is, unless explicitly defined differently), that collection will be denoted Fun(s).
In an appropriate state S, a ground term t = f()
evaluates
to an element
.
If
is a tuple
(
)
of terms,
define
.
An expression may be a Boolean term or a metalanguage statement.
Often it does not matter which it is. One can use two different equality
signs or just try to be careful; we choose the second alternative.