On Friday 20 Apr 2012 13:36, Steve King wrote:
> For interest, my recollection is that the Standard's
> definition of variable scope was based on:
> - the idea of a *set* of a declarations: decl1; decl2
> should have 'the same effect' as decl2; decl1.
This is in "Understanding Z" though its not clear why this
is thought to be desirable (though of course, if you call it
a "set" of declarations you have already taken a step in
that direction).
It may be noted that this does not provide a basis for
chosing between the scope rules in the standard and those
adopted in ProofPower, since they both have this
characteristic.
> The other thing to remember is that the Standard does not
> include a logic: there was no agreement at the time (or
> now!). So effects of decision decisions on proof
> couldn't be easily seen.
This was something which I advocated at the very beginning
of the standardisation process (I attended the meetings for
a while, maybe a year, and then Rob Arthan took over
representing ICL on the panel).
I did this because we had already had a proof tool and
expected that any attempt to promulgate a standard logic
would be unlikely to fall in line with the ICL
implememtation.
And of course, the semantics suffices to determine which
deductive systems are sound, and that should be good enough.
If I'm not mistaken you were present at ICL Winnersh when I
gave my first presentation on the way in which proof in Z
would work in our tool, (using conversions which delivered
extensional characterisations of the various set denoting
expressions), and that you pointed out an error in my
presentation.
I'm guessing that Z standardisation had not yet started at
that point.
I also advocated a loose semantics for partiality since
Spivey had by then already firmly diverged from the prior
tradition (I believe) that Z should be understood in two-
valued first order logic, and this was in our opinion bad
news for proof (by allowing that terms sometimes failed to
have a value).
This is bad news for proof since it makes many
transformations which would otherwise be unconditional
conditional on whether the terms involved denote.
However, I don't recall discussions of scope rules, in which
had I been present I would also have advocated a loose
specfication (probably with less success).
I don't know to what extent these attempts to make the
standard "loose" could have rescued ProofPower Z from non-
compliance, since we would still have been able to prove
things which were not definitely true under the standard
semantics.
> The case where I really regret the scope rules is where
> you need to model a set-valued variable, together with a
> particular element of the set. Instead of saying
> xs: P X; x: xs, you have to say xs: P X; x: X | x \in xs
> More long-winded and harder to understand!
Yes this is an example of the benign uses of the variables
in the declaration of names in the signature which I
referred to.
Rob was rather definite in his rejection of my "prohibition"
interpretation (of Spivey) without saying why.
I think this is correct insofar as "Understanding Z" is
concerned. However, Spivey does not seem to me to have been
consistent between "Understanding Z" and the ZRM.
In my early analysis of the treatment of partiality in Z I
had a table with four columns in it "Blue book" "Red book",
"previous info" and "ICL HOL/Z", and various aspects of the
treatment of partiality on each row.
No two colums were the same.
As far as the scope issue is concerned it is probably more
accurate to say that it was clear to me that the mapping
into HOL would be simpler and the resulting proof more
straightforward if the scope includes the declaration.
In that case we have in effect that the occurrences of names
on the left of colon's are both binding occurrences and
bound occurrences (in the implicit predicate).
If the scope excludes the declaration neither of these
change but we then find that occurrences on the right are
free, so in the same textual context the same name may
appear as a binding occurrence, a bound occurrence and as
free variables.
The variable binding constructs were one of the special
challenges in devising a mapping from Z into HOL and
I would certainly not have been keen to make the problem
even more difficult for the sake of a scope rule which seemed
to me to be ill-advised.
By way of further mitigation I note that in the ZRM Spivey
is not as explicit about the consequences of this rule as he
perhaps should have been, and his slightly fudges the issue
leaving open the "prohibition" interpretation.
This option can be understood in terms of scope rules as
arising from making a large hole in the out scope than the
inner scope, and Spivey's words taken literally do indeed
have this effect, since he says:
"the whole of the inner quantification is a hole in the
scope of the variable x introduced by the outer
quantifier"
from which we may infer that occurrences of x in the
declaration are in neither the outer nor the inner scope.
If he really meant it then he had diverged from
"understanding Z", but I believe he did so on other points
(though I can't remember what they were).
For Phil, on the differences between the two editions of ZRM,
I have not noticed any material differences in this part
(section 2.3.1).
Roger Jones
_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
