<div dir="ltr">Hi Rob,<div><br></div><div>Following our recent discussion on this list</div><div><br></div><div><a href="http://www.gilith.com/opentheory/mailing-list/2013-December/000328.html">http://www.gilith.com/opentheory/mailing-list/2013-December/000328.html</a><br>
</div><div><br></div><div>I added the following note to the "varType" command in the article format<br></div><div><br></div><div><a href="http://www.gilith.com/research/opentheory/article.html#varTypeCommand" target="_blank">http://www.gilith.com/research/opentheory/article.html#varTypeCommand</a><br>

</div><br>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".<div>
<br></div><div>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.</div>
<div><br></div><div>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).</div>
<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><br></div><div>Cheers,</div><div><br></div><div>Joe</div><div><br></div></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Tue, Feb 18, 2014 at 8:46 AM, Rob Arthan <span dir="ltr"><<a href="mailto:rda@lemma-one.com" target="_blank">rda@lemma-one.com</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div style="word-wrap:break-word"><div>I have a problem with edge cases in the mappings of type variable</div><div>names. What currently happens is that I export them as they stand</div>
<div>and import them by prefixing them with a prime if they don't already</div><div>start with one. Ramana does something more complicated by also </div><div>converting a primed single letter to upper case on output and to</div>
<div>lower case on input. The upshot of this is 'a in ProofPower imports as 'a</div><div>in HOL4 which then imports back into ProofPower as 'A which imports</div><div>back into HOL4 as 'a and now we are in a loop. This is harmless</div>
<div>but a bit silly. So should I be adjusting the case like Ramana does?</div><div>And if so why?</div><div><br></div><div>Since a HOL4 or ProofPower theory with non-standard type variable</div><div>names looks a mess and since the Gilith OpenTheory Repo seems</div>
<div>to have standardised on what HOL4 and ProofPower consider</div><div>non-standard, these mappings are necessary. Unfortunately,</div><div>they also need to be one-to-one and this is not the case for</div><div>what I do when importing or what Ramana does when importing or</div>
<div>exporting without some assumptions. What assumptions can we</div><div>reasonably make?</div><div><br></div><div>Regards,</div><div><br></div><div>Rob.</div></div><br>_______________________________________________<br>

opentheory-users mailing list<br>
<a href="mailto:opentheory-users@gilith.com">opentheory-users@gilith.com</a><br>
<a href="http://www.gilith.com/opentheory/mailing-list" target="_blank">http://www.gilith.com/opentheory/mailing-list</a><br>
<br></blockquote></div><br></div>