The Analytic Hierarchy 261
x := ∀
: y := ∀
if ¬(y<x) then accept
x := y
goto
Any property that is expressed as a least fixpoint of a monotone map
defined by a positive first-order formula can be computed by an IND pro-
gram. Here is what we mean by this. Let ϕ(
x, R) be a first-order formula
with free individual variables
x = x
1
,... ,x
n
and free n-ary relation vari-
able R. Assume further that all occurrences of R in ϕ are positive ;thatis,
occur under an even number of negation symbols ¬. For any n-ary relation
B, define
τ(B)
def
= {a | ϕ(a, B)}.
That is, we think of ϕ as a set operator τ mapping a set of n-tuples B
to another set of n-tuples {
a | ϕ(a, B)}. One can show that the positivity
assumption implies that the set operator τ is monotone, therefore by Theo-
rem A.9 has a least fixpoint F
ϕ
,whichisann-ary relation. The traditional
treatment defines a first-order inductive relation as a projection of such a
fixpoint; that is, a relation of the form
{(a
1
,... ,a
m
) | F
ϕ
(a
1
,... ,a
m
,b
m+1
,... ,b
n
)},
where b
m+1
,... ,b
n
are fixed elements of the structure. Given the formula ϕ
and the elements b
m+1
,... ,b
n
, one can construct an IND program that as-
signs b
m+1
,... ,b
n
to the variables x
m+1
,... ,x
n
, then checks whether the
values of x
1
,... ,x
n
satisfy F
ϕ
by decomposing the formula top-down, exe-
cuting existential assignments at existential quantifiers, executing universal
assignments at universal quantifiers, using control flow for the propositional
connectives, using conditional tests for the atomic formulas, and looping
back to the top of the program at occurrences of the inductive variable
R. The examples above involving reflexive transitive closure, games, and
well-foundedness illustrate this process.
Conversely, any relation computed by an IND program is inductive in
the traditional sense, essentially because the definition of acceptance for
IND programs involves the least fixpoint of an inductively defined set of
labelings of the computation tree.
Inductive and Hyperelementary Relations
Many of the sample IND programs of the previous section make sense when
interpreted over any structure, not just N. We define the inductive relations
of any structure A to be those relations computable by IND programs over