🚀 go-pugleaf

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