Variable declarations

[Till Mossakowski <till@informatik.uni-bremen.de>]

Dear Peter,

I want try to summarize the discussion about variable declarations:
There are two proposals:

1. Gianna's proposal to have global declarations of variables,
which are added as (either open or universally quantified, which
does not matter here) variables to each subsequent axiom. To cope
with the empty carrier problem, only those globally declared variables
should be added which actually occur free in the axiom (while it is always
possible to added non-occuring variables in a quantification local
to the axiom).

2. Bernd's proposal to let the abstract syntax as it stands, and
treat Gianna's problem of multiple axioms with (possibly different
subsets of) the same set of variables by writing a single universal
quantification of a conjunction of the list of axioms.
[This seems to assume that the axioms occur together, rather than
interspersed with declarations of sorts, functions, etc.?  --PDM]
To make this easy to use, the concrete syntax should be designed
to allow subsequent lines of texts occurring within a universal
quantification (i.e. within some indentation, using an off-side rule,
or indicated by brackets) to be interpreted as implicit conjuction.
This proposal has the following advantages:
a) The scope of the variables is delimited (by brackets, off-side rule),
so variable names may be used differently in different scopes,
while in 1., the scope is the whole BASIC-SPEC.
b) Variable declarations remain tightly bound to the axioms they
refer to, this makes transformation tools less complicated.
A disadvantage may be that the empty carrier problem remains here,
but this is not so severe since the scope of the declaration is limited,
so an axiom like is-empty(empty)=false can easily be placed outside
the scope of any variable.
[Perhaps one could provide both, so that everyone is happy?  --PDM]

Greetings,
Till