Delivery-Date: 
Sender: info-hol-request@leopard.cs.byu.edu
Errors-To: info-hol-request@leopard.cs.byu.edu
Precedence: bulk
From: Wishnu Prasetya <wishnu@cs.ruu.nl>
Message-Id: <199312211115.AA10365@relay.cs.ruu.nl>
Subject: Re: Help with DEPTH_CONV
To: Wai.Wong@cl.cam.ac.uk (Wai Wong)
Date: Tue, 21 Dec 1993 12:15:21 +0100 (MET)
Cc: info-hol@cs.uidaho.edu (hol mailing list)
In-Reply-To: <"swan.cl.cam.:108460:931221105953"@cl.cam.ac.uk> from "Wai Wong" at Dec 21, 93 10:59:39 am
Mime-Version: 1.0
Content-Type: text/plain; charset=US-ASCII
Content-Transfer-Encoding: 7bit
Content-Length: 1336

  > Wishnu,
  > 	The problem you have is not the size of the subterms, but
  > the conversion can be applied to the subterm REPEATEDLY. This means
  > the system drops in an infinite loop. As the manual page says:
  > 
  > DEPTH_CONV c tm repeatedly applies the conversion c to all the subterms of
  > the term tm, including the term tm itself.  The supplied conversion is
  > applied repeatedly (zero or more times, as is done by REPEATC) to each
  > subterm until it fails. 

I would say that applying c to ALL subterms of tm is a finite process.
This is the impression I got of what DEPTH_CONV do after reading the
manual.

It seems to me that the infinite loop is caused more because
DEPTH_CONV c tm also attemps to applies c to subterm of every term
generated by c itself. 

  > You should use ONCE_DEPTH_CONV instead of DEPTH_CONV in this case.

I also have problem in interpreting the manual here. Quoting from the
manual: "ONCE_DEPTH_CONV c t applies c once to the FIRST term on which
it suceeds in a top down traversal" I would say that

  ONCE_DEPTH_CONV SYM_CONV "((a:*)=b) /\ (b=a)"


will result |- ((b=a) /\ (b=a) as "b=a" is the first subterm onwhich
SYM_CONV will suceed. But instead it gives:

  |- (a = b) /\ (b = a) = (b = a) /\ (a = b)  

But then again, apparently I simply have misunderstood the manual.

-Wishnu-