<html><head></head><body 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">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),</div></div></blockquote><div><br></div><div>I think you will find that this is John Harrison's convention rather than HOL Light's - those As and Bs come from explicit type casts in the HOL Light source. So you'd have to ask John what to do if he wanted more than 26 type variables :-). For the record the ProofPower parser carries on with "'27", "'28" and the HOL4 parser uses "'a0", "'a1". When the HOL Light parser invents type variables they come out as ?N where N is a number that is never the same twice. I have no idea why John implemented it like this - it has the bizarre effect that `x` == `x` returns false in HOL Light.</div><br><blockquote type="cite"><div dir="ltr"><div> 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></blockquote><div><br></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>Regards,</div><div><br></div><div>Rob.</div><br><blockquote type="cite"><div dir="ltr">
<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>
_______________________________________________<br>opentheory-users mailing list<br><a href="mailto:opentheory-users@gilith.com">opentheory-users@gilith.com</a><br>http://www.gilith.com/opentheory/mailing-list<br></blockquote></div><br></div></body></html>