[opentheory-users] WFREC

[Konrad Slind]

Yes, probably WFREC doesn't need to be there, just the final theorems.

Note that relationTheory is quite simple, in that it is just based on

   'a -> 'a -> bool

That means that there are lots of "wellfoundedness" operators
that probably shouldn't get transported to relationTheory. I'm thinking
of "measure" in particular, which has type

   ('a -> num) -> 'a -> 'a -> bool

and belongs in whatever basic theory of natural numbers you've got.

Konrad.


On Wed, Apr 4, 2012 at 11:19 PM, Joe Hurd <joe at gilith.com> wrote:
> [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
>>
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list