Re: comments on 0.93: variable declarations

[pdmosses@brics.dk]

[Thanks for the prompt reactions to the proposal concerning variable
declarations as basic items!  --PDM]


From: Jim Horning <horning@intertrust.com>

[Referring to the proposal from Gianna Regggio:]

Our experience with LSL strongly supports this, for exactly the reasons   
given.

[Referring to the comments by Chris George:]

This is exactly why LSL rejects all models with empty carriers.  We never   
found a use for such models, either.

Jim H.


From: cerioli@disi.unige.it (Maura Cerioli)

>[So perhaps one could interpret variable declarations as
>quantifying only over the variables *used* in each axiom?
>Or just leave the axioms open??  --PDM]
Gianna is currently examining some poor students, but I'm sure that this is
what she had in mind with her proposal.
That is, open formulae are intended as their universal closures, where the
sort of variables is deduced from the environment built by the VAR-DECL
part
Best regards
Maura


From: pdmosses@brics.dk (Peter D. Mosses)

In Section 1.3 of the Language Design Summary v0.93, it should
be clarified where the X in "Sigma(X)-terms" comes from.

Independently of the decision about whether open formulae used as
axioms should be implicitly universally closed, one could say that X
is determined by the valid variable declarations for the enclosing
basic specification, supplemented (and perhaps overridden) by those in
enclosing explicit quantifications.

Or is there a neater way of explaining this?

Peter