Re: Variable declarations

[Andrzej Tarlecki <tarlecki@ipipan.waw.pl>]

Dear Peter,

You called for opinions on two topics (one long overdue). So, let me
just state my opinion, without much detailed justification at this
point.

1. Satisfaction of sentences:

Till proposed (a message time-stamped: Sat, 5 Oct 1996 16:06:28 +0200)
three possibilities differing in the view of variables (whether their
valuations are total or partial), suggesting a middle one --- partial
valuation of free variables, and total valuation of quantified
variables --- as the one to take.

I would rather stick to what we have: total valuations of all the
variables. Yes, we have to live then with a bit more complex
substitution rule, where it is necessary to explicitly state (and
hence check) definedness of the term which is being substituted for a
variable. But I view this more as an advantage than a disadvantage:
since we are working in a framework with partiality, definedness
checks have to happen somewhere, and we better make sure that the user
is aware of this. We have to teach the users who work with partial
functions to check definedness anyway, so we can as well do this as
explicitly as possible.

I would think that an apparent economy of proofs a different treatment
of free (than of quatified) variables might bring is less important
than a good understanding of the semantics of formulae, which such a
view may make more difficult to achieve.

Aha, this would be especially misleading if some form of implicit
(universal) closure of axioms was built into the language, as then a
confusion between free and quatified variables is quite likely.

2. Variable declarations and their importance for axioms etc:

In general I disagree with the idea that we should be able to "declare
variables once for all the axioms in a specification". From the most
fundamental point of view, universal quantification of variables is a
part of an axiom, as essential as anything else in the axiom for the
definition of its satisfaction. So, I would like to keep it where it
belongs.  [This view is in conflict with the majority of existing
specification languages, I believe.  --PDM]

Of course, in practice writing the same universal quantification over
and over again for a number of axioms is a pain, especially when the
type names a complex (not to say compound :-). But then again, if the
quantification really is common for a bunch of axioms, we can always
write a quantified conjunction as single axiom.  [...provided that the
axioms are not interspersed with declarations.  --PDM]

I do not think that it would be elegant to hide any subtleties (like
quantification over empty types) under the carpet by some more or less
tricky conventions like implicit quantification over those of the
declared variables that actually occur (free) in the axiom.  [Tricky?
The notion of the universal closure of a formula is surely rather
standard!  --PDM]

Perhaps as some kind of compromise we could consider declarations of
variables introducing only some information for the static semantics
about the intended types of the declared variables in axioms. Then a
variable would still have to be explicitly quantified over in axioms,
but its type could be omitted and deduced from its declaration?

Aha, I have some technical doubts that should be cleared out before we
adopt this proposal in any form: I am not sure how exactly a scope of
variable declarations would be determined in structured specs
(whatever the role of such declarations should be).
[My understanding is that it should be the enclosing BASIC-SPEC. --PDM]

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

And a final disclaimer: I do not feel too strongly about any of the
about issues --- just an opinion as many others...  [Thanks... and I
hope you don't mind me adding my reactions above! --PDM]

Best regards,

Andrzej