🚀 go-pugleaf

[ 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