  We consider the reachability problem for higher-order functional programs and
study the relationship between reachability games (i.e., the reachability
problem for programs with angelic and demonic nondeterminism) and
may-reachability (i.e., the reachability problem for programs with only angelic
nondeterminism). We show that reachability games for order-n programs can be
reduced to may-reachability for order-(n+1) programs, and vice versa. We
formalize the reductions by using higher-order fixpoint logic and prove their
correctness. We also discuss applications of the reductions to higher-order
program verification.
