[opentheory-users] type variable names

[Ramana Kumar]

On Mon, Sep 5, 2011 at 11:09 PM, Joe Hurd <joe at gilith.com> wrote:
> Hi Ramana,
>
> On Sun, Sep 4, 2011 at 7:55 AM, Ramana Kumar <ramana.kumar at gmail.com> wrote:
>> Unfortunately, type variables cannot be bound, so their names matter.
>
> My initial reaction to this is that I regard type variables being
> implicitly bound at the theorem level, like so:
>
> (forall-type A)  { <assumptions using type variable A> } |- <conclusion using A>
>
> This gives them the same status as free term variables in theorems,
> and both can be instantiated (or renamed) using the same primitive
> inference (subst).
>
> For me the larger issue is that OpenTheory allows any UTF-8 string as
> a type or term variable name, but different theorem prover
> implementations have different opinions on what constitutes a valid or
> standard variable name.
>
>> Is the convention for their names in OpenTheory specified somewhere?
>
> Notwithstanding the above, I agree that a convention for OpenTheory
> variable names would be beneficial, if only to avoid quite so many
> calls to subst to compose theories uploaded from different theorem
> prover implementations.
>
>> Looking at the base package, for example, one might guess that type
>> variables are named by uppercase letters starting from "A".
>
> By historical accident many conventions in the current set of
> OpenTheory theories have been inherited from HOL Light - including
> numerals, which you started discussing in a separate thread
>
> http://www.gilith.com/opentheory/mailing-list/2011-September/000106.html
>
> I'm currently writing a theory exporter to generate Haskell packages,
> and I've encountered the same difficulties because Haskell type
> variables must begin with a lower case letter.
>
> I haven't given much thought to good variable name conventions in
> OpenTheory, and would be very happy to hear people's opinions on this.

Well there is one convention that is very good for term variables:
bind them all, whatever they are. (Including exotic characters is a
separate issue.) This way theorems with different names are actually
equal as stack machine objects and don't need a rule to convert
between. My point was that the same trick doesn't work for type
variables. (By the way, at risk of hijacking this thread, the
convention seems to be violated in the theorems generated by
defineTypeOp, specifically the "r" and "a" variables are free: is
there a good reason for that?)

> One thing that's nice about the current scheme for type variables
> inherited from HOL Light is that you can see at a glance what's a
> variable and what's an operator, because of the convention that type
> operator names start with a lower case letter:
>
> (A * B) option list
>
> Haskell opts for the exact opposite set of conventions:
>
> List (Maybe (a,b))
>
> HOL4 uses an apostrophe to call out the variables
>
> ('a # 'b) option list
>
> but introduces a possible confusion as to whether or not the
> apostrophe is part of the name.
>
>> If this convention ought to be relied on, then it would make sense for
>> article readers and writers for HOL4, for example, which has a
>> different convention, to translate between "A" and "'a" automatically
>
> I agree that translating between OpenTheory conventions and theorem
> prover conventions in this way would be a nice feature of an interface
> layer.

I will put that translation in the HOL4 article reader/writer then :)

>
> Cheers,
>
> Joe
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>