Re: Variable declarations

[Didier Bert <Didier.Bert@imag.fr>]

Comments about the declarations of variables : I would want to give
arguments for keeping the variables inside the axioms and against a
global declaration of a list of variables common to a list of axioms.

1- This is consistent with the definition of logic formulae, where the
quantification of the variables is a part of the formula
(cf. Andrzej). Many model-oriented specification languages adopt this
point of view, although not chosen in many algebraic specification
languages.

2- As quoted by Till (1st nov), tools must deal with variables when
they use axioms. In the case where variables are local to each axiom,
there is no problem to translate an axiom by a signature morphism in
another specification (no name conflict) or more generally, for any
operation on formulae.

3- If we adopt a solution where the user declares the variables
globally, but where the meaning is that the variables are bounded
locally, there is no direct correspondence between an external
specification and its internal representation and that can cause
problems, for example if we want to visualise (to flatten) a
specification built by operators.

4- We must be aware that the heavy declaration of variables is a
consequence of the ``many-sorted'' framework. So, we have to accept
(``assumer'' in french) this fundamental choice.

5- The problem of emptyness of carriers can be considered
independently of the declaration of variables in the axioms. We can
have the global assumption that the carriers are not empty. This can
be checked when a new data type is declared and this can be assumed as
hypotheses for formal sort parameters (as it is done in the B language
for formal sets).  Obviously, for subsorts, dependent types, etc.,
non-emptyness must be checked by suitable mechanism (proof, etc.).

6- A last point: in the LPG language, declarations of variables are
global in a specification ! The work carried out for the
implementation of the language and for the implementation of the tools
like the solver of goals, etc. convinced me that it is better to have
variables locally declared for each axiom.

==================================

Again: ``And a final disclaimer: I do not feel too strongly about any
of the about issues --- just an opinion as many others... ''
(Andrzej on Mon Nov  4,  9:01am).

Best regards,
Didier

-- 
==============================================================================
Didier Bert			   http://www-lsr.imag.fr/users/Didier.Bert/
IMAG-LSR			   Tel: 04 76 82 72 16	    +33 476 82 72 16
BP 53 				   Fax: 04 76 82 72 87	    +33 476 82 72 87
F-38041 Grenoble Cedex 9
==============================================================================