On the detection of some loops in recursive computations

Abstract

In the present paper recursive computations are treated as a certain deterministic kind of term processing. The terms are built up in the usual way from atoms by means of function symbols. The atoms are intuitively viewed as constants. Simple non-atomic terms are those ones constructed by supplying some function symbol with arguments which are atoms. A recursion rule is supposed to be given, considered s a mapping of the set of the simple non-atomic terms into the set of all terms. A recursive computation is a process of constructing terms by starting with some given term and , while possible, replacing the leftmost occurrence of a simple non-atomic term in the current term by the corresponding term according to the given recursion rule. A Brent-Van Gelder's style method is proposed for detection of the case when some simple non-atomic term repreduces itself again in a leftmost position after a positive number of steps in a recursive computation.