Formalizing non-termination of recursive programs
In applicative theories the recursion theorem provides a term rec which solves recursive equations. However, it is not provable that a solution obtained by rec is minimal. In the present paper we introduce an applicative theory in which it is possible to define a least fixed point operator. Still, our theory has a standard recursion theoretic interpretation. (C) 2001 Elsevier Science Inc. All rights reserved.
non-termination applicative theories least fixed point operator