[opentheory-users] Type variables

[Joe Leslie-Hurd]

Hi Rob,

It might perhaps be a nice feature if the "axiom" command didn't just match
alpha-equivalent theorems, but was able to rename/instantiate type and free
term variables too. However, that seems like a lot to ask of an article
reader, and in any case it wouldn't solve the problem of processing type
variables when reading articles exported from another theorem prover with
different conventions.

There was some discussion on the list a while back about standardizing
names for type variables:

http://www.gilith.com/opentheory/mailing-list/2011-September/000114.html

The best solution seems to be for the OpenTheory standard theory library to
adopt one convention (currently capital letters, like HOL Light), and for
other theorem provers to convert them to their local convention as part of
reading/writing articles (e.g., HOL4 would map A to 'a, B to 'b, etc.)

I have added a note about this to the documentation for the varType command
in the article format:

http://www.gilith.com/research/opentheory/article.html#varTypeCommand

Cheers,

Joe



On Fri, Nov 29, 2013 at 3:23 PM, Rob Arthan <rda at lemma-one.com> wrote:

> The OpenTheory "thm" command  allows for an alpha-conversion to get the
> variable names in a theorem exactly right. The description doesn't say
> anything about type instantiation, so presumably type variable names have
> to be right already. Perhaps it should allow type variable renaming too,
> because the choice of type variable names in definitions of existing
> constants (like the quantifiers) is going to be implementation-dependent.
> Unfortunately, this is a little tricky to specify and implement because
> "thm" also allows the inferred theorem to have fewer assumptions than the
> target theorem.
>
> On this topic, the Gilith OpenTheory Repo seems to use HOL Light type
> variable names (A, B, C etc.) that can't be parsed in HOL4 or ProofPower.
> In any case, if "thm" doesn't allow for type variable renaming, then the
> documentation needs to say what type variables have been used.
>
> Regards,
>
> Rob.
>
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20131202/d50e5a4b/attachment.html>