[opentheory-users] WFREC

[Joe Hurd]

[While I'm finally catching up on my email] one thing I might add to
this discussion is that constants and type operators that are specific
to the infrastructure of a single theorem prover don't necessarily
have to be part of the OpenTheory standard theory library. The
constants you list don't appear in the final theorems returned by the
recursive function definition package, but are simply used to prove
that the desired recursive functions exist. The relevant theory
infrastructure could be "statically linked" in theories exported from
HOL4.

However, I'm not saying that such constants should never appear in
OpenTheory. It may well be the case that, say, RESTRICT is a perfectly
general operator for restricting the domain of relations that could be
useful in a variety of contexts, and if that was the case then it
would be a good addition to the Relation namespace.

Cheers,

Joe

On Thu, Feb 2, 2012 at 5:06 PM, Michael Norrish
<Michael.Norrish at nicta.com.au> wrote:
> 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
>
>
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>