yxoc@sbsvax.cs.uni-sb.de (Ralf Treinen) (08/14/90)
Is the following a known problem? I would be very surprised if nobody
has worked on this problem, but I could not find anything in the literature.
Who can give useful references?
Briefly: Is it decidable whether a recursive program scheme is equivalent to
one of its finite appriximations?
In Detail:
----------
Consider recursive programs schemes in the sense of [Courcelle and Guessarian:
On Some Classes of Interpretations, JCSS vol. 17], that is
F1(x1,1 ... x1,l1) <= t1
...
Fn(xn,1 ... xn,ln) <= tn
The ti are first order terms, possibly containg the function signs F1 ... Fn
and some other base functions, and with their free variables among
xi,1 ... xi,li . We do not assume the existence of any predefined function
symbol with a fixed meaning, especially we do not assume the existence of
something like "if-then-else" or some means of testing equality.
We use the following class of interpretations: all algebras such that each
carrier set is a flat complete partial order (for instance natural numbers
plus bottom where bottom is less than each number but two numbers are
uncomparable) and all functions are monotonic. Functions may be non strict,
that is why we can avoid requiring something like "if-then-else".
Let Fi<m> denote the m-th approximation of Fi, that is the term that is obtained
by applying some computation rule m times to Fi(xi,1, ... xi,li) and then
substituting each term of the form Fj(...) by bottom. The computation rule
is some safe computation rule in the sense of Manna, for instance parallel
outermost or full substitution.
For example, for the program scheme F(x) <= f(x,F(h(x)))
the first iterations are:
F<1> = f(x,bottom)
F<2> = f(x,f(h(x),bottom))
F<3> = f(x,f(h(x),f(h(h(x)),bottom)))
Is the following question decidable:
For given recursive program scheme, is there an m such that for all
interpretations I and all assignements the following holds:
Fi(xi,1 ... xi,li) = Fi<m>
For example, the above program does not have this property. This can be shown
by constructing for each m some kind of term model such that indeed m
computation steps are needed for some input value.
On the other hand, the following program has the above property:
F(x) <= f(x,F(x))
Since from the properties of monotonic functions the following follows:
f(x,bottom) = f(x,f(x,bottom)), and so F is always equal to its first iteration.
These are of course simple examples, thing are more complicated if there are
more recursive functions with arity greater than 1 and nested function calls.
Neverthless I guess it IS a decidable property.
All references, ideas, guesses, etc. will be appreciated.
Thanks a lot, Ralf.
--
Ralf Treinen | Universitaet des Saarlandes
FB 14 - Informatik (Dept. of CS) | D-6600 Saarbruecken 11, West Germany
--------------------------------------+--------------------------------------
email: treinen@cs.uni-sb.de | phone: +49 681 302 2065