fs@rex.cs.tulane.edu (Frank Silbermann) (06/14/90)
In article <15548@dime.cs.umass.edu> yodaiken@freal.cs.umass.edu (victor yodaiken) writes: >>>> But doesn't Primitive Recursive arithmetic >>>> contain much too small a set of functions? >>> Too small for what? I do not understand why a programming language >>> would need to be able to expressive functions that are not feasible. > What's an example of a function that is of real interest > and that cannot be expressed cleanly as a p.r. function? Could you write an interpreter for Horn clause logic programming (which is semi-decidable) as a primitive recursive function? On the otherhand, if you view primitive recursive functions as adequate for general programming, you _could_ reply that a Prolog interpreter is not of real interest! :-) Frank Silbermann fs@rex.cs.tulane.edu
yodaiken@freal.cs.umass.edu (victor yodaiken) (06/15/90)
In article <3594@rex.cs.tulane.edu> fs@rex.cs.tulane.edu (Frank Silbermann) writes: >Could you write an interpreter for Horn clause logic programming >(which is semi-decidable) as a primitive recursive function? > >On the otherhand, if you view primitive recursive functions >as adequate for general programming, you _could_ reply that >a Prolog interpreter is not of real interest! :-) > > Frank Silbermann fs@rex.cs.tulane.edu 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. Note that "steps" is a flexible notion here, and could include quite non-trivial computation. Is there a reason why such a function is significantly less useful than a partial function?
jrk@sys.uea.ac.uk (Richard Kennaway) (06/15/90)
In article <15591@dime.cs.umass.edu> yodaiken@freal.cs.umass.edu (victor yodaiken) writes: >In article <3594@rex.cs.tulane.edu> fs@rex.cs.tulane.edu (Frank Silbermann) writes: >>Could you write an interpreter for Horn clause logic programming >>(which is semi-decidable) as a primitive recursive function? >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. Note that "steps" is a flexible notion here, and could include >quite non-trivial computation. Is there a reason why such a function is >significantly less useful than a partial function? 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. 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? -- Richard Kennaway SYS, University of East Anglia, Norwich, U.K. Internet: jrk@sys.uea.ac.uk uucp: ...mcvax!ukc!uea-sys!jrk
murthy@algron.cs.cornell.edu (Chet Murthy) (06/15/90)
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. There are almost certainly practical uses for such functions - all of Ramsey theory was not developed for mathematician's sexual sublimation. Neither was the theory of well-quasi-orders. Both of these areas are applicable to term-rewriting, etc, and both of these areas are rife with recursive functions with ordinal running times above epsilon_0. --chet-- murthy@cs.cornell.edu
news@usc.edu (06/16/90)
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?