🚀 go-pugleaf

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