Next: Decidability of Freeness of Up: User-Defined procedures and Functions Previous: User-Defined procedures and Functions
For now, suppose we have no recursion. We add procedures and/or functions. We have to decide what linear means. If it means that we are only allowed one call to each procedure then the problem is trivial and uninteresting. If we are allowed more than one call then things get interesting, so let's assume we are allowed to have more than one call. Let's call that "procedural linear", just for now.
Does this just make our schemas non-linear. After all, for any non linear schema, s, I can probably construct a "procedural linear" schema that identical to s after unfolding procedures. Well, what about if we start to add scope. In the absence of recursion, the primary semantic issue with procedures is one of scope (I think). Suppose that a procedure is not allowed to have global variables (only local ones). This raises the issue of how a procedure communicates its results. What if we are allowed a function call that can only take parameters and return a result and can only be used in an assignment at the top level. This is about as easy as I think it can get before it is trivial.
that is, suppose we can only write
x := UD(a,b,c);
Does this only differ from the existing situation with function-free linear schemas in that we can have repeated applications of UD? (this might then offer a "use" for Mike's predicate linear result).
Not quite, because we have access to the body of UD, so we can see whether all of a,b and c really affect the outcome. Nonetheless, this has the feel of something that could be tamed. It is probably trivial to handle this tiny augmentation, isn't it? Mike?
Suppose we allow the use of UD functions in all the places where they could occur on the RHS of an assignment,
Se we could write
x:= UD(UD(x,a,c),b,c) does that make things harder?
I presume things get a lot harder if we allow UD functions into predicates, but if the predicates themselves are still uninterpreted functions, then the results should still hold, shouldn't they? or not? Mike?
What about procedures, as opposed to functions. Here we have to decide how they communicate their result if they are not allowed to assign to globals. It seems to me that if they are allowed to assign to globals then we can "simulate" a non-linear schema using a set of procedure calls and so I presume we would lose all the advantages that linearity conveys. If I got that right,m then we have to abandon ever hoping to have procedures with globals. However, this need not be a deal breaker for linear schemas of itself, because apart from aliasing issues, programs can be converted into version that do not make use of globals.