[opentheory-users] Type variable names

[Joe Leslie-Hurd]

Hi Rob,

Following our recent discussion on this list

http://www.gilith.com/opentheory/mailing-list/2013-December/000328.html

I added the following note to the "varType" command in the article format

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

Note: The OpenTheory standard theory library adopts the HOL Light
convention of naming type variables with capital letters, and theorem
provers are expected to map them to local conventions as part of processing
articles. For example, in HOL4 it would be natural to map an OpenTheory
type variable with name "A" to a local type variable with name "'a".

I worked very hard to make the article format agnostic of the choice of
symbol names (constants & type operators can be renamed, most commands are
blind to alpha-equivalent terms), but unfortunately the names chosen by
theorem provers for type variables persist inside OpenTheory proofs.

When technical solutions fail, political solutions must take up the slack.
In this case, the policy is for type variables in OpenTheory format to be
named according to HOL Light conventions (single capital letter, start
naming from A, I've no idea what happens if a term requires more than 26),
and for other theorem provers to rename on import and export between
OpenTheory standard names and native names (just like what already happens
with constant and type operator names).

So applying the policy to your loopy scenario, I'm afraid it is the
ProofPower importer and exporter that is in violation, and I suggest you
implement Ramana's HOL4 procedure for importing and exporting type variable
names. Then HOL4 and ProofPower should be able to play nicely with each
other, and as a bonus with HOL Light too.

Cheers,

Joe



On Tue, Feb 18, 2014 at 8:46 AM, Rob Arthan <rda at lemma-one.com> wrote:

> I have a problem with edge cases in the mappings of type variable
> names. What currently happens is that I export them as they stand
> and import them by prefixing them with a prime if they don't already
> start with one. Ramana does something more complicated by also
> converting a primed single letter to upper case on output and to
> lower case on input. The upshot of this is 'a in ProofPower imports as 'a
> in HOL4 which then imports back into ProofPower as 'A which imports
> back into HOL4 as 'a and now we are in a loop. This is harmless
> but a bit silly. So should I be adjusting the case like Ramana does?
> And if so why?
>
> Since a HOL4 or ProofPower theory with non-standard type variable
> names looks a mess and since the Gilith OpenTheory Repo seems
> to have standardised on what HOL4 and ProofPower consider
> non-standard, these mappings are necessary. Unfortunately,
> they also need to be one-to-one and this is not the case for
> what I do when importing or what Ramana does when importing or
> exporting without some assumptions. What assumptions can we
> reasonably make?
>
> 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/20140218/a85ebea8/attachment.html>