Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.4) outside ac.uk; Sun, 14 Feb 1993 20:58:02 +0000 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA09755; Sun, 14 Feb 93 12:43:16 -0800 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA09749; Sun, 14 Feb 93 12:43:08 -0800 Received: from auk.cl.cam.ac.uk (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.4) to cl; Sun, 14 Feb 1993 20:42:41 +0000 To: info-hol@edu.uidaho.cs.ted Subject: Re: power of HOL In-Reply-To: Your message of Fri, 12 Feb 93 14:09:46 -0500. <9302121909.AA09659@spock> Date: Sun, 14 Feb 93 20:42:38 +0000 From: John Harrison Message-Id: <"swan.cl.ca.049:14.02.93.20.42.44"@cl.cam.ac.uk> "My" conjecture has met with general scepticism. David McAllester argues as follows (apologies for any misrepresentation and my general ignorance about recursion theory) The primitive recursive functions in HOL are recursively enumerable. Therefore one can define a recursive function by diagonalization, i.e. its value at n is 1 greater than that of the n'th HOL PR function. But this cannot correspond to any of the HOL PR functions. This would indeed appear to show that the HOL PR functions are not coextensive with the recursive functions (as it certainly does for first-order PR). I suppose it's true that any HOL PR function is recursive -- that's the only difference I can see? On reflection I am a little unsure as to what my question means. What forms of nonrecursive definition should one allow as constituting `higher-order primitive recursion'? At least one must presumably expand the forms of substitution/application over first order PR? If one allows any nonrecursive terms as a part of a PR definition, then it's intuitively plausible (and Tom Melham refers me to Thm 6401 of Peter Andrews' book) that one can define any recursive function. For example one can minimize a function f by: @n. (f(n) = 0) /\ (!m. m < n ==> ~(f(m) = 0)) Tom Melham has also pointed out to me something right at the end of the book by Barendregt on lambda-calculus (cf. pp 569-70, and the very last exercise) which might be relevant, but I'm not quite sure what it's saying. Toby Nipkow suggests Schwichtenberg as a good person to ask (I note Barendregt refers to a paper by him in the '73 Logic Colloquium about something similar). John. JRH .-~~~-__-~~~-. { } <--`. -----;'--<<< `. .' `. .' \/ HOL