<html><head><meta http-equiv="Content-Type" content="text/html charset=windows-1252"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;"><br><div><div>On 19 Feb 2014, at 11:25, Rob Arthan <<a href="mailto:rda@lemma-one.com">rda@lemma-one.com</a>> wrote:</div><br class="Apple-interchange-newline"><blockquote type="cite"><div style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; ">Joe,<div><br><div><div>On 18 Feb 2014, at 18:22, Joe Leslie-Hurd wrote:</div><br class="Apple-interchange-newline"><blockquote type="cite"><div dir="ltr">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).</div></blockquote><blockquote type="cite"><div dir="ltr">
<div><br></div><div>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.</div></div></blockquote><div><br></div></div></div></div></blockquote>And I replied:<br><blockquote type="cite"><div style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; "><div><div><div>Well. I will see what it takes to amend Ramana's mapping so that it is guaranteed to be one-to-one.</div><div><br></div></div></div></div></blockquote></div><div><br></div><div>Note that HOL4, HOL Light and ProofPower all allow mk_vartype to be called with an arbitrary string.</div><div>So to handle pathological cases, we cant make any assumptions about the strings. At first I thought we</div><div>would need an input-dependent mapping, but I think the following fixed mapping works.</div><div><br></div><div>ProofPower to OpenTheory:</div><div><br></div><div>Case 1: type variable name comprises a prime followed by 1 or more alphanumerics or underscores:</div><div>remove the prime and switch case of alphabetic characters.</div><div>E.g. a maps to A, 1_aZ maps to 1_Az.</div><div><br></div><div>Case 2: type variable name comprises 1 or more alphanumerics or underscores:</div><div>prefix with a prime and switch case of alphabetic characters.</div><div>E.g., Xyz maps to xYZ.</div><div><br></div><div>Case 3: anything else: switch case of alphabetic characters..</div><div>E.g. maps to . A b maps to a B.</div><div><br></div><div>OpenTheory to ProofPower:</div><div><br></div><div>Case 1: type variable name comprises 1 or more alphanumerics or underscores:</div><div>prefix with a prime and switch case of alphabetic characters.</div><div>E.g., Z maps to z, 1_aZ maps to 1_zA.</div><div><br></div><div>Case 2: type variable name comprises a prime followed by 1 or more alphanumerics or underscores:</div><div>remove the prime and switch case of alphabetic characters.</div><div><div>E.g., 'Xyz maps to xYZ.</div></div><div><br></div><div><div>Case 3: anything else: switch case of alphabetic characters..</div><div>E.g. maps to . A b maps to a B.</div></div><div><br></div><div>I wasnt certain about the pros and cons of switching case in cases 2 and 3,</div><div>but it seemed more consistent always to switch case.</div><div><br></div><div>Any comments welcome.</div><div><br></div><div>Maybe Ramana might like to consider switching to the same scheme in the HOL4 OpenTheory implementation.</div><div>(Apart from the fact that HOL4 warns that some type variable names are non-standard, I think its syntax rules</div><div>and the conventions most users adopt agree with ProofPower.)</div><div><br></div><div>Regards,</div><div><br></div><div>Rob.</div><div><br></div><div><br></div><div><br></div><div><br></div></body></html>