Ensuring the quasi-termination of needed narrowing computations

We present a characterization of first-order functional programs which are quasi-terminating with respect to the symbolic execution mechanism of needed narrowing, i.e., computations in these programs consist of a sequence of finitely many different function calls (up to variable renaming). Quasi-terminating programs are particularly useful for program analysis and transformation, since in this context quasi-termination often amounts to full termination.