[opentheory-users] WFREC

[Michael Norrish]

On 26/01/12 00:42, Ramana Kumar wrote:
> I'm thinking about the appropriate namespace for a recursion operator for wellfounded relations.
> In HOL4 it is called WFREC and is in relationTheory.
> In fact there is a small suite of related definitions there: RESTRICT, approx, and the_fun.
> I'm wondering if the list has any ideas about an appropriate way to package these things up (i.e. under what name, or with what other stuff).
> I realize I may need to give more background about what they actually do... (don't have that on me at the moment!)

These are operators used to define functions that recurse in well-founded ways.  I can see that they are not necessarily automatic fits for the relation theory, though they're obviously pretty tightly dependent on the WF notion from relation theory. 

How about a new theory called something like recursive functions?  (Of course, the problem with this is the possible confusion with the computable functions...)  Failing that, just put them into relation!

Michael


-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 554 bytes
Desc: OpenPGP digital signature
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20120203/00a11cdb/attachment.pgp>