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 2065bjornl@sics.se (Bj|rn Lisper) (08/20/90)
In article <5960@sbsvax.cs.uni-sb.de> yxoc@sbsvax.cs.uni-sb.de (Ralf Treinen) writes: %Is the following a known problem? .... %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 .... %Let Fi<m> denote the m-th approximation of Fi, .... .... %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> .... %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. I don't know the answer either, but I do have some comments. 1. Why do you guess the property is decidable? I guess it is not, in general. It is mostly just a gut feeling. In order to prove the property for a given scheme, I think the equalities Fi<m> = Fi<m+1> must be proved, for all i and a certain m. Equation solving is essentially unification, which is decidable in some algebras (pure term algebras, for instance) and undecidable in others. So maybe the decidability of the property is dependent on the underlying algebra of the first-order terms. Maybe somebody can provide a more stringent alternative to my handwaving above? 2. An interesting observation is that the m:th approximations correspond to fixed terms over the underlying first-order algebra. So if the property holds, then the defined functions can always be evaluated according to the terms rather than the recursive computation rule. The terms can be evaluated bottom-up rather than top-down, and the computation structure is fixed (since the terms are fixed). Thus, compilation time optimization techniques can be applied to find efficient execution patterns (iterative instead of recursive, parallelizing scheduling, ...). So if there is a decision procedure for the problem, AND a method to find the m:th approximations in question (i.e. not just knowing the existence), then we have the embryo of an interesting technique for compile-time optimizations of this class of recusively defined functions. 3. The property in question corresponds to what sometimes is loosely referred to as "static algorithms", "computation with a static structure" etc. Bjorn Lisper
yxoc@sbsvax.cs.uni-sb.de (Ralf Treinen) (08/21/90)
[ Sorry if you see this for the 2nd time. The first attempt apparently failed] From article <1990Aug20.083410.24135@sics.se>, by bjornl@sics.se (Bj|rn Lisper): > In article <5960@sbsvax.cs.uni-sb.de> yxoc@sbsvax.cs.uni-sb.de (Ralf > Treinen) writes: > > % F1(x1,1 ... x1,l1) <= t1 > % ... > % Fn(xn,1 ... xn,ln) <= tn > > %Let Fi<m> denote the m-th approximation of Fi, .... > %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> > > > 1. Why do you guess the property is decidable? I guess it is not, in > general. It is mostly just a gut feeling. In order to prove the property for > a given scheme, I think the equalities Fi<m> = Fi<m+1> must be proved, for > all i and a certain m. Equation solving is essentially unification, which is > decidable in some algebras (pure term algebras, for instance) and > undecidable in others. So maybe the decidability of the property is > dependent on the underlying algebra of the first-order terms. > I agree with you in so far as the decidability depends on the underlying class of interpretations. For instance, if you only consider interpretations containing "if-then-else" with its standard meaning, the question should be undecidable. In this case, all interesting questions about program schemes are undecidable. This has been shown by Luckham, Park and Paterson ("On formalized computer programs", JCSS 11 (1975), pp. 358-374). But I am interested the class of *all* discrete interpretations, that is I do not assume "if-then-else" or something like this. I do not see how to apply the proofs of the above paper to this case. The reason why I think the question is decidable is the following: 1.) Consider the set of subterms of the approximations that do not contain function variables. For the program F(x) <= f(x,F(h(x))) this set is {x, h(x), h(h(x)), h(h(h(x))), ... }. If the size of the terms in the set is unbounded, than the minimal fixpoint of the program is *not* equivalent to any of its approximations. This is easily proven by constructing for each n a model such that n computation steps are required for some input. 2.) On the other hand, if the size of the set is bounded, the recursion must be "trivial" is some sense, that is the situation is similar to the following program: F(x) <= f(x,F(x)). This is just a guess, and until now I could not prove this second part. 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