yodaiken@freal.cs.umass.edu (victor yodaiken) (06/16/90)
Some interesting responses to my query on why we need non-p.r. constructs in a programming language. Maybe the discussion would be clarified if we distinguished between general mathematical languages, and programming languages. Programming languages are mathematical languages for describing operations that are to be performed by a computer. Obviously, non-p.r. functions are useful in many mathematical languages. Are they useful/essential in programming languages? I'm assuming that the computers we are talking about are devices constructed from physical discrete switching elements. As long as these elements are have a bounded number of states, usually on/off, and take up 3 dimensional space, we will be restricted to computers with finite state sets or be faced with a rather uninteresting metaphysical problem. Several responders made an argument to the effect that nothing is accomplished by using p.r. functions instead of more general functions. News@usc.edu (anonymous) writes: > In article <15591@dime.cs.umass.edu> yodaiken@freal.cs.umass.edu > (victor yodaiken) writes: > > How about a function F_k: HCLWFF -> {T,F, TimedOut} > where for horn clause wff P, F_k(P)= TimeOut if > the algorithm does not conclude within j**j**j**j ... > k exponentiations > steps, where j is the length of P and k is a parameter bounding > the length. For decent sized k, > F_k(P) = TimedOut means that P is not feasibly decidable using this > algorithm. > > heh! > > so I just make a set of cover functions for all the system calls that > plug in the largest representable numeric value for the termination > parameter. What's been accomplished? > jrk@sys.uea.ac.uk (Richard Kennaway) has a similar point: > >The question here is whether or not we need non-p.r. functions to > >write programs? > > That is one question, and several examples have been posted; another is, > why should even a p.r. function necessarily be programmed in p.r.? These arguments seem to miss the point. P.r. arithmetic is a very simple, clear, formalization of a large chunk of number theory. It seems at least possible that reasoning about such a well behaved class of functions will be easier than reasoning about, say lambda-calc. So the question I'm asking is "do we really need a more general class of functions?". If not, then it might be interesting to see what a p.r. functional programming language would look like. An assertion that nothing is accomplished by using p.r. functions does not answer my question. In murthy@algron.cs.cornell.edu (Chet Murthy) writes: > > The beef I have with just prim. rec. is not about nontermination. If > every algorithm had to have a bound, I'd be happy. But prim. rec. > does not encompass all recursive functions, or even all > computationally interesting recursive functions. > .... > But your bound might not be p.r. You bound might be some ordinal > ABOVE epsilon_0. Such a program would still be bounded, still be > terminating, still efficient for the average case, but not provably > p.r. To exclude such algorithms simply because they can't be coded > using primitive recursion seems a bit extreme. > --chet-- > murthy@cs.cornell.edu > I'm afraid I don't understand this argument. Clearly, computers, are finite state objects, a computer able to use space not bounded by an integer function is an interesting mathematical notion, but has no physical counterpart. Secondly, any algorithm can be expressed as a p.r. function that "cuts-off" when the computation takes too long. We can write a p.r. function F which corresponds to a non p.r. function F' so that F(x)=F'(x) when the computation requires less than say, a quintuple exponential iterations, and so that F(x)= ERROR when the computation requires more than a quintuple exponential number of iterations. Thus we do not have to "exclude" non-pr algorithms from a p.r. programming language, we merely have to admit that they may not complete. Finally, it appears to me that what computers do is manipulate symbols representing mathematical objects, thus, invoking the "downward" lowenhiem skolem theorem, it is hard to see a mathematical necessity for higher ordinals in a programming language. Chet Murphy goes on in another posting to say: > jrk@sys.uea.ac.uk (Richard Kennaway) writes: > > >Technical question: are there functions which are expressible in PRA > >but much more compactly expressible in (e.g.) Horn clauses (or some other > >programming language more powerful than PRA)? Are there any practically > >useful such functions? > > I would be quite certain of this one. The work of Friedman on long > proofs of small theorems is relevant here, I think. > I'd like to know more about this. Note, if we have a p.r. programming language, there is nothing which requires us to use p.r. techniques for proving properties of programs. ********************* steve@hubcap.clemson.edu ("Steve" Stevenson) writes: > yodaiken@freal.cs.umass.edu (victor yodaiken) writes: > > >t arguing that one can dispense with all but p.r. mathematics. I'm > >questioning the need for anything beyond p.r. functions in > >a *programming language*. > > If it's a while loop, then it's not p.r. Look for one program with a while > loop which cannot be a simple for loop. > Take an example of a loop that is not p.r. (or is not known to be p.r. in any case). F(x,y) = While( there are fewer than x primes z < y, return F(x,y+1)) If this function is a program, then its actual behavior will diverge quite a bit from its conventional mathematical semantics. For some x and y F(x,y) will either be undefined or will fail in some other way. The two alternative p.r. functions F_k(x,y) = while( there are fewer than x primes z < y if y < x**x**x**x**x**x ... then return F(x,y+1) else return 0 AND F(x,y) = while( there are fewer than x primes z < y if y < MachineDependentBound() then return F(x,y+1) else return 0 on the other hand have precise mathematical semantics that actually correspond to the behavior of the program on a computer. As verwer@ruuinf.cs.ruu.nl (Nico Verwer) writes: > This is, however, not a very practical way of programming your computer. > In most cases, one prefers to think of a digital computer as modelling a > turing machine, or a lambda-calculus reduction machine. This allows you > to express algorithms in a more or less concise way, and doesn't force > the algorithm designer to account for memory or time limitations. > > It is better to use implicit bounds because, even though a computer > memory is always finite, one may always buy a faster computer with more > memory, and change those bounds. > Thus, the formal semantics of the program KB'(p,q) is: > Choose non-deterministically between > - KB(p,q) > - an "out of memory" error > - the user gets frustrated from waiting and kills the process. > The outcome depends on your particular system, and your patience... > It's the best you can get, I'm afraid :-) . > This is quite sensible, but I'm unhappy with the semantics that we get. How can we hope to analyze a system composed of functions that are all non-deterministic? Is it really so inconvenient to include bounds? ******************** gb@cs.purdue.EDU (Gerald Baumgartner) writes: > > >>This Groebner basis algorithm has a similar structure as the > >>Knuth-Bendix algorithm (Knuth-Bendix can be simulated by Groebner > >>basis algorithm, probably vice versa). > The usual way to run this algorithm on more difficult examples is to > start it and see whether you get a useful result before the machine > crashes the next time. I've seen useful results after 1-2 weeks of CPU > time on a Microvax II. > > Sure you can use bounds on the running time (say 1 year). But with > algorithms whose running time is completely unpredictable (that's how > it appears to the user) why not use the natural bound of waiting until > the next downtime of the machine. > > I don't think your proposed PR constructs are a bad thing, but I'd like > to have non-PR constructs as well. > > Gerald > By using uninterpreted function symbols I can easily get the same effect. That is i can write a function iterate from i=0 to GodKnows() F(x) If we increase GodKnows() each iteration until the system crashes, we get the effect of an infinite loop. The compiler would hide the details of this trick, so that the function would look like a p.r. function, and be subject to analysis as if it were p.r. Finally: jrk@sys.uea.ac.uk (Richard Kennaway) writes that a p.r. version of knuth-bendix is unappetizing: > > Because it requires the program to explicitly include a computation bound, > and to check that it has not been reached yet. If I know that the > algorithm I want to program is feasible, it is superfluous to explicitly > include a time bound in the program; and if I do not know if it is > feasible, it is either superfluous (if I give it a time bound far longer > than any user is able to wait for an answer) or erroneous (if I give it a > shorter bound). > > While it may be of interest to know that some problem can be solved in > PRA, it does not follow that its solution should be expressed in PRA. Again, if I can conveniently write a wide range of program in a p.r. language, it may have benefits other then a feeling of virtuous frugality.
guttman@mitre.org (Joshua D. Guttman) (06/17/90)
In article <15693@dime.cs.umass.edu> yodaiken@freal.cs.umass.edu (victor yodaiken) writes:
* * * *
These arguments seem to miss the point. P.r. arithmetic is a very simple,
clear, formalization of a large chunk of number theory. It seems at least
possible that reasoning about such a well behaved class of functions will
be easier than reasoning about, say lambda-calc.
By at least one measure, it is just as hard to reason about the PR functions as
about the full set of general recursive functions.
Namely, consider (say) the Ritchie-Meyer LOOP language, which has just a
primitive recursive ("for") iteration construct. And select a decidable
assertion language, say Pressburger arithmetic or quantifier-free
Pressburger arithmetic or even the pure theory of equality. The validity
question for the Hoare triples of this system is still undecidable.
Mark Nadel and I wrote up a brief note proving this fact when we found that
many people were unaware of it (or even skeptical when told it). It basically
killed off my interest in PR programming, because it means that checking the
correctness of programs still can't be done by a (total) algorithm. So why put
up with the roundabout programming and artificial bounds that would be called
for?
Josh