[opentheory-users] type variable names

[Joe Hurd]

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.
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.

Cheers,

Joe