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



On Sun, 7 Apr 2013, Gottfried Barrow wrote:

If possible, I'd like to know what naming conventions I "have to" follow to prevent future, potential errors due to naming.

There is nothing you "have to" follow. Naming conventions are a matter to keep things simple at very little cost -- they belong to "best practices".

Observing certain customs routinely saves a lot of energy to rethink and reconsider things over and over again. Sometimes this has to be done, nonethrless: e.g. for Isabelle/Scala I've re-used many Isabelle/ML conventions at the cost of violating other conventions on the Java Virtual Machine, and Scala itself tends towards very mixed ways of writing. I had to spend extra time to study history, manuals, websites to ensure that no bad consequences are coming from Graph.is_minimal in both Isabelle/ML and Isabelle/Scala, and not Graph.is_minimal here and Graph.isMinimal there (IAmNotGoingIntoDetailsWhyCamelCaseIsNotUsedInOurTradition).


Anyway, the mail thread you mention was initiated by the surprise that using a lower-case theory name in Isabelle/HOL makes the Haskell code generator fail due to resulting lower-case module name, which Haskell rejects.

Theory names in Isabelle have a long-standing naming tradition: capital words (usually in singular), separated by underscore.

Example (good): Vector_Space.

Counter-examples (bad): Vector_Spaces, VectorSpaces, vectorSpaces, vectorspace etc.

Many years ago, theory names were als very short, since users had to repeat typing use_thy invocations a lot on the TTY, but has changed a lot with the introduction of Proof General in 1998. Today there is nothing special saying outright what you mean with theory Boolean_Algebra, which former generations would have squeezed that towards 8 or 5 characters.


The majority of material within a theory body uses lower case names (also separate by underscore). Some special situation have capitalized or all-caps names, e.g. "max", "Max", "MAX" for certain families of operations.

Locale names are within a theory body, and thus lower-case.

Example:

  theory Vector_Space
  imports Main
  begin

  locale vector_space = ...
  begin

  definition "foo = ..."

  end

  end

This produces fully qualified names like

  Vector_Space.vector_space.foo

with name space accesses like

  Vector_Space.foo   -- "global access"
  vector_space.foo   -- "local access"

That is the basic observation from 1999, when locales were first introduced. Further complexity has piled up since then, but the basic advantage of having access to two important hierary levels is still there -- by convention, not by special machinery that would introduce extra complexity.

You do get overlaps in certain more complex cases nonetheless, but the convention is somewhat better off than doing it just arbitrarily.


	Makarius




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