Re: [isabelle] What naming will cause potential errors?



On Sun, 7 Apr 2013, Gottfried Barrow wrote:

For theorem names, I name many theorems starting with uppercase, which seems to be contrary to the convention in the HOL sources.

I have good reason to do this, because I care more about following mathematical notation conventions than following Isabelle coding conventions.

In some sense the "coding" conventioned deviated by accident (or on purpose) from what you often see in informal "prose" text, but I would consider this an improvement. We are not writing for the New York Times here.

Isabelle sources are coming from certain free-world Unixoid background where lowercase is preferred. The ancient empire of IBM had enforced all-caps variable names, and the advent of proper lowercase in ASCII was a great relieve (together with the invention of the underscore as formal separator).


I did not invent these conventions, but I do think that lower-case is better for the mass of text. Incidently, Coq prefers capital names and keywords by default, and just last year some hard-core Coq users pointed this out as historical accident: it causes a lot of pain to press SHIFT so often, especially in Proof General. The proposed solution was then to use vi keyboard mapping for Emacs. (If this is madness, there is method in it.)

Note that I normally don't argue about the ease of *writing* the sources, since ease of *reading* has the prime priority. This is why the underscore is important to separate words, and lower-case helps the Western brain to gloss quickly over large bodies of text (this is why the scribes of Charlemagne invented the miniscules). Uppercase still has its role in situations of special emphasis, e.g. "max", "Max", "MAX", but it would loose that benefit if it were used by default.


However, if someone tells me that my naming scheme will potentially cause errors, rather than just annoy people

Annoyance only starts when people try to combine several independent theory libraries into bigger coherent applications.

Until recently, hardly anything was done in this respect, apart from the main libraries that are shipped with Isabelle (main HOL and HOL/Library). I am pleased to see that in recent years, some AFP articles have started to aggregate, and build up beginnings of modest dependency structures.


But I don't want to change my naming scheme without knowing what the rules are because there are lots of different objects, in particular, in addition to theorem names, there are locales, classes, and sublocales, which I see that I may need now.

As a general principle in Isabelle, "different objects" don't differ in the naming convention, but make them coincide as far as sensible, even with the actual names. Each category of a separate name space, so you normally you don't have a dog "foo_dog", cat "foo_cat", mouse "foo_mouse", but dog "foo", cat "foo", mouse "foo".

In practice, this could mean class "nat", type "nat", const "nat", theorem "nat". Fine points need to be observed when different categories appear in clusters: lets say some type "nat" and some const "nat" that both produce some theorem "nat.induct", which would then clash in the common theorem name space.


	Makarius




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.