[opentheory-users] Type variable names

[Rob Arthan]

On 19 Feb 2014, at 11:25, Rob Arthan <rda at lemma-one.com> wrote:

> Joe,
> 
> On 18 Feb 2014, at 18:22, Joe Leslie-Hurd wrote:
> 
>> 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.
> 
And I replied:
> Well. I will see what it takes to amend Ramana's mapping so that it is guaranteed to be one-to-one.
> 


Note that HOL4, HOL Light and ProofPower all allow mk_vartype to be called with an arbitrary string.
So to handle pathological cases, we can’t make any assumptions about the strings. At first I thought we
would need an input-dependent mapping, but I think the following fixed mapping works.

ProofPower to OpenTheory:

Case 1: type variable name comprises a prime followed by 1 or more alphanumerics or underscores:
remove the prime and switch case of alphabetic characters.
E.g. “‘a” maps to “A”, “‘1_aZ” maps to “1_Az”.

Case 2: type variable name comprises 1 or more alphanumerics or underscores:
prefix with a prime  and switch case of alphabetic characters.
E.g., “Xyz” maps to “‘xYZ”.

Case 3: anything else: switch case of alphabetic characters..
E.g. “‘“ maps to “‘“. “A b” maps to “a B”.

OpenTheory to ProofPower:

Case 1: type variable name comprises 1 or more alphanumerics or underscores:
prefix with a prime and switch case of alphabetic characters.
E.g.,  “Z” maps to “‘z”, “1_aZ” maps to “1_zA”.

Case 2: type variable name comprises a prime followed by 1 or more alphanumerics or underscores:
remove the prime and switch case of alphabetic characters.
E.g., “'Xyz” maps to “xYZ”.

Case 3: anything else: switch case of alphabetic characters..
E.g. “‘“ maps to “‘“. “A b” maps to “a B”.

I wasn’t certain about the pros and cons of switching case in cases 2 and 3,
but it seemed more consistent always to switch case.

Any comments welcome.

Maybe Ramana might like to consider switching to the same scheme in the HOL4 OpenTheory implementation.
(Apart from the fact that HOL4 warns that some type variable names are non-standard, I think it’s syntax rules
and the conventions most users adopt agree with ProofPower.)

Regards,

Rob.




-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20140331/de09c3c4/attachment.html>