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; Tue, 16 Feb 1993 20:18:07 +0000 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA19797; Tue, 16 Feb 93 11:21:07 -0800 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from ben.uknet.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA19792; Tue, 16 Feb 93 11:20:47 -0800 Received: from eros.uknet.ac.uk by ben.uknet.ac.uk via UKIP with SMTP (PP) id ; Tue, 16 Feb 1993 18:52:42 +0000 Received: from puffin.doc.ic.ac.uk by eros.uknet.ac.uk via UKIP with SMTP (PP) id <12956-3@eros.uknet.ac.uk>; Tue, 16 Feb 1993 18:25:31 +0000 Received: from ist.co.uk by puffin.doc.ic.ac.uk id <22808-0@puffin.doc.ic.ac.uk>; Tue, 16 Feb 1993 18:18:30 +0000 Received: from isohel by Istvax.Ist.co.uk via UUCP id aa06369; 16 Feb 93 16:57 WET Received: from isotropy.istcamb by upper.ist.co.uk (4.1/SMI-4.1) id AA21733; Tue, 16 Feb 93 16:56:06 GMT Date: Tue, 16 Feb 93 16:56:06 GMT From: Will Harwood Message-Id: <9302161656.AA21733@upper.ist.co.uk> To: John.Harrison@uk.ac.cam.cl, info-hol@edu.uidaho.cs.ted Subject: Re: power of HOL It appears from reading Girards "Proofs and Types" that the recursive functions expressable in HOL by higher order primitive recursion are the provably terminating functions. This seems to follow from the fact that this is true of Girards second order lambda calculus, system F, which is simple type theory plus abstraction on types (essentailly polymorphism). Hope this is helpful to someone. regards will ---------------------------------------------- Will Harwood Imperial Software Technology -----------------------------------------------