Delivery-Date: 
Sender: info-hol-request@ted.cs.uidaho.edu
Errors-To: info-hol-request@ted.cs.uidaho.edu
Precedence: bulk
Message-Id: <199305101605.AA19810@panther.cs.uidaho.edu>
To: info-hol@ted.cs.uidaho.edu
Subject: Re: Can't solve recursion equation
In-Reply-To: Your message of Sun, 09 May 93 10:36:56 -0400. <9305091436.AA02600@sparta.oracorp.com>
Date: Mon, 10 May 93 09:05:26 -0700
From: Phil Windley <windley@panther.cs.uidaho.edu>


On Sun, 09 May 93 10:36:56 EDT, shb@oracorp.com wrote:
+------------
| 
| I'm defining several functions with new_recursive_definition, and the
| most difficult debugging comes after I get the
| 
|   Can't solve recursion equation
| 
| error message.  Every time so far, the problem has been that I've
| misspelled some constant's name.  Do people have any recommendations
| for a relatively painless way of finding such errors?  I'm using HOL90
| release 5 if that makes a difference in the answer.

Non-recursive definitions have a similar problem: its not uncommon on a
long definition to get a message about unbound vars in the definition.  I
once hacked the definition code to return a list of the free vars, but the
chanmges were lost in version changes.

When I have problems like this (whether with recursive definitions or
otherwise) the first thing I do is to apply the function _frees_ to the
term I'm trying to define and look at the list.  The free vars should be on
the lhs of the equality.

--phil--

Phillip J. Windley, Asst. Professor   |  windley@cs.uidaho.edu
Laboratory for Applied Logic	      |  windley@panther.cs.uidaho.edu
Department of Computer Science        |
University of Idaho                   |  Phone: 208.885.6501  
Moscow, ID    83843                   |  Fax:   208.885.6645