🚀 go-pugleaf

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