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; Fri, 12 Feb 1993 11:33:31 +0000 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA28131; Fri, 12 Feb 93 03:14:57 -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 AA28126; Fri, 12 Feb 93 03:14:47 -0800 Received: from auk.cl.cam.ac.uk (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.4) to cl; Fri, 12 Feb 1993 11:01:39 +0000 To: info-hol@edu.uidaho.cs.ted Subject: Re: power of HOL In-Reply-To: Your message of Fri, 12 Feb 93 09:18:35 +0000. <"2259*/I=RB/S=Jones/OU=win0109/O=icl/PRMD=icl/ADMD=gold 400/C=GB/"@MHS> Date: Fri, 12 Feb 93 11:01:35 +0000 From: John Harrison Message-Id: <"swan.cl.ca.415:12.02.93.11.01.42"@cl.cam.ac.uk> Roger Jones writes: > Computationally HOL is Turing Complete. This isn't saying much. > The logical (proof theoretic) strength of HOL is a logical matter, > I would not have thought it a problem in "advanced computation", > and the answer is well known. The following assertion about the HOL logic has a computational flavour: Every total recursive function is higher-order primitive recursive (i.e. can be defined using only primitive recursive definitions in HOL). Certainly the Ackermann function, the classic example of a total recursive function which isn't first-order PR, was done as an example recently (see info-hol passim). But is the above assertion universally true? John.