Return-Path: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) id <29117-0@swan.cl.cam.ac.uk>; Thu, 14 May 1992 11:14:44 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA10164; Thu, 14 May 92 03:06:19 -0700 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA10160; Thu, 14 May 92 03:06:13 -0700 Received: from guillemot.cl.cam.ac.uk by swan.cl.cam.ac.uk with SMTP (PP-6.0) to cl id <28913-0@swan.cl.cam.ac.uk>; Thu, 14 May 1992 11:06:14 +0100 To: toal@edu.ucla.cs Cc: info-hol@edu.uidaho.cs.ted, Tom.Melham@uk.ac.cam.cl Subject: Re: Ackermann's function In-Reply-To: Your message of Wed, 13 May 92 17:08:42 -0700. <9205140008.AA15050@ewa.cs.ucla.edu> Date: Thu, 14 May 92 11:06:04 +0100 From: Tom Melham Message-Id: <"swan.cl.ca.916:14.04.92.10.06.17"@cl.cam.ac.uk> > The footnote on p. 180 of DESCRIPTION states that Ackermann's function > can be defined by primitive recursion in HOL. Just curious how. See the proof below. Tom % --------------------------------------------------------------------- % % Ackermann's function defined in HOL. T. Melham, May 1992. % % % % Proof taken from M.J.C. Gordon, Programming Language Theory and its % % Implementation (Prentice-Hall, 1988), pp. 96-97. % % --------------------------------------------------------------------- % new_theory `ack`;; let rec = new_prim_rec_definition (`rec`, "(rec 0 x y = (x:*)) /\ (rec (SUC n) x y = y(rec n x y))");; let lemma2 = PROVE ("?fn. (!n. fn(0,n) = n+1) /\ (!m. fn(m+1,0) = fn(m,1)) /\ (!m n. fn(m+1,n+1) = fn(m,fn(m+1,n)))", let fn = "\(m:num,n:num). rec m SUC (\f x. rec x (f 1) f) n" in EXISTS_TAC fn THEN CONV_TAC(DEPTH_CONV PAIRED_BETA_CONV) THEN CONV_TAC (ONCE_DEPTH_CONV num_CONV) THEN REWRITE_TAC [rec;ADD_CLAUSES] THEN CONV_TAC (DEPTH_CONV BETA_CONV) THEN REWRITE_TAC [rec]);; let ACK = new_specification `ACK` [`constant`,`ACK`] lemma2;; close_theory();;