Received: from scaup.cl.cam.ac.uk by Steve.CL.Cam.AC.UK with SMTP/TCP/IP over Ethernet id a022378; 29 May 89 11:12 BST Via: uk.ac.nsf; 29 May 89 11:10 BST (UK.AC.Cam.Cl.scaup) Received: from clover.ucdavis.edu by NSFnet-Relay.AC.UK via NSFnet with SMTP id aa04664; 29 May 89 10:51 BST Received: from ucdavis.ucdavis.edu by clover.ucdavis.edu (5.59/UCD.EECS.1.9) id AA27205; Mon, 29 May 89 02:50:38 PDT Received: by ucdavis.ucdavis.edu (5.51/UCD1.41) id AA09078; Mon, 29 May 89 02:39:51 PDT Received: from computer-lab.cambridge.ac.uk by NSFnet-Relay.AC.UK via Janet with NIFTP id aa04455; 29 May 89 10:20 BST Received: from steve.cl.cam.ac.uk by scaup.Cl.Cam.AC.UK id aa17667; 29 May 89 10:32 BST Date: Mon, 29 May 89 10:30:11 BST From: Jeffrey Joyce To: info-hol Message-Id: <8905291032.aa17667@scaup.Cl.Cam.AC.UK> Sender: jjj Status: R More on n-bit words =================== In regard to my earlier message about n-bit words, Tom Melham has pointed out that the basis case in Albert Camilleri's proof of the n-bit adder in Cambridge Tech. Report #91 is actually a "0+1" bit adder and not a 0-bit adder. I originally had my own version of this proof in mind, but referred to the published proof given by Albert without noticing this slight difference. The proof in TR91 uses a different definition of "Val" than the definition of "Valn" shown below. To clarify my earlier remarks, here is a part of my n-bit adder proof (specification and basis steps). % ===================================================================== % % First the n-bit adder specification: % % % % let Adder = new_prim_rec_definition ( % % `Adder`, % % "(Adder 0 a b cin cout sum = (cout = cin)) /\ % % (Adder (SUC n) a b cin cout sum = % % ?w. Add1 (a n,b n,w,cout,sum n) /\ Adder n a b cin w sum)");; % % % % A function for converting n-bit words to natural numbers: % % % % let Valn = new_prim_rec_definition ( % % `Valn`, % % "(Valn 0 b = 0) /\ % % (Valn (SUC n) b = % % ((2 EXP n) * ((b n) => 1 | 0)) + Valn n b)");; % % % % Top-Level Correctness Statement: % % % % set_goal ([], % % "!n a b cin cout sum. % % Adder n a b cin cout sum ==> % % ((((2 EXP n) * (Val cout)) + (Valn n sum)) = % % ((Valn n a) + (Valn n b) + (Val cin)))");; % % % % Use induction and then simplify the basis step. % % % % expandf (INDUCT_TAC);; % % expandf (REWRITE_TAC [Adder;Valn;EXP;MULT_CLAUSES;ADD_CLAUSES]);; % % % % The above REWRITE_TAC simplifies the basis step to: % % % % "!cin cout. (cout = cin) ==> (Val cout = Val cin)" % % % % This is easily solved by: % % % % expandf (REPEAT STRIP_TAC THEN ASM_REWRITE_TAC []);; % % ===================================================================== % In concrete terms, my point here is that correctness results for the 1-bit adder are not used in the basis step ... they get used exactly once in the entire proof and that's in the induction step. As for the "philosophical point", I didn't mean specifically that leaving 0-bit words out would be an imitation of engineering practice. I meant much more generally that the concept of a 0-bit device is a useful concept in our work - even though it is less likely to be a useful concept at the enginneering level. Finally, with regard to the "width-checking" problem mentioned in Tom's latest message, I wonder if there's any chance of solving this problem for a restricted set of relations between word widths (as opposed to the general case), eg., identity, "+ C" where C is a constant ? Jeff