Return-Path: Delivery-Date: Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Tue, 21 Dec 1993 11:22:09 +0000 Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA03790; Tue, 21 Dec 1993 04:15:17 -0700 Sender: info-hol-request@leopard.cs.byu.edu Errors-To: info-hol-request@leopard.cs.byu.edu Precedence: bulk Received: from dworshak.cs.uidaho.edu by leopard.cs.byu.edu with SMTP (1.37.109.8/16.2) id AA03786; Tue, 21 Dec 1993 04:15:10 -0700 Received: from swan.cl.cam.ac.uk by dworshak.cs.uidaho.edu with SMTP (1.37.109.8/16.2) id AA16198; Tue, 21 Dec 1993 03:13:11 -0800 Received: from merganser.cl.cam.ac.uk (user rjb (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Tue, 21 Dec 1993 11:12:24 +0000 To: Wishnu Prasetya Cc: info-hol@cs.uidaho.edu (hol mailing list) Subject: Re: Help with DEPTH_CONV In-Reply-To: Your message of "Tue, 21 Dec 93 11:35:27 +0100." <199312211035.AA08606@relay.cs.ruu.nl> Date: Tue, 21 Dec 93 11:12:21 +0000 From: Richard Boulton Message-Id: <"swan.cl.cam.:113190:931221111227"@cl.cam.ac.uk> Wishnu Prasetya writes: > Can anyone kindly explain why is the following application of > DEPTH_CONV is wrong: > > #DEPTH_CONV CONTRAPOS_CONV "!x:*. P x ==> p" ;; > > Error: Frame stack overflow. > Fast links are on: do (use-fast-links nil) for debugging > Error signalled by %AP. > Backtrace: > funcall > lambda > %AP > evaluation failed lisp error DEPTH_CONV is repeatedly applying the conversion, building larger and larger terms each time. This can be seen by repeated application of ONCE_DEPTH_CONV, which you should use instead: #ONCE_DEPTH_CONV CONTRAPOS_CONV "!x:*. P x ==> p" ;; |- (!x. P x ==> p) = (!x. ~p ==> ~P x) #ONCE_DEPTH_CONV CONTRAPOS_CONV (rhs (concl it));; |- (!x. ~p ==> ~P x) = (!x. ~~P x ==> ~~p) #ONCE_DEPTH_CONV CONTRAPOS_CONV (rhs (concl it));; |- (!x. ~~P x ==> ~~p) = (!x. ~~~p ==> ~~~P x) Richard.