Re: Variable declarations

[Eelco Visser <visser@fwi.uva.nl>]

Remarks on variable declaration and quantification:


It seems to me that global vs. local declaration of variables is 
orthogonal to explicit vs. implicit universal quantification of axioms.


My preference would be to declare variables globally (also 
export variable declarations from modules) and have implicitly
quantified axioms, at least in the user language.

- It is a straightforward operation to transform implicitly quantified
axioms into explicitly quantified ones and axioms are much more readable
when variable declarations are omitted.

- Variable names are as much part of the language defined by a signature
as are its operations and sorts. It is usual to define certain ranges
of letters or names as variables for some sort and use these consistently.
Global declarations encourage this. Some kind of renaming mechanism can be 
used to resolve clashes.

regards,

        Eelco Visser

---
mail:visser@fwi.uva.nl
http://adam.fwi.uva.nl/~visser/