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 

> 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 
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 
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 

> 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                         

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

Reply via email to