[ProofPower] Some questions about ProofPower/Z

[Roger Bishop Jones]

On Monday 13 September 2004  2:49 pm, Thiago Carvalho de Sousa 
wrote:

> 1) I´d like to know if there is some .doc explaining
> the encoding of Z in ProofPower-HOL. I´l like to
> verify how deep is this enconding...

The encoding was first defined (by me) formally in Z in
two documents entitled "Proof support for Z via HOL (I)"
and "... (II)".  We then implemented a prototype, threw
it away and wrote the real thing, during which process
these documents were not maintained.
You can find up to date documentation for the mapping in
the detailed design documents which are in the distribution
but these do not include formal specifications.
(look in $PPINSTALLDIR/tex/fmu.bib and search for
"Detailed Design of the Z..." and "Detailed Design for the Z...",
and then seek the relevant documents in the src directory).

This stuff was done more than ten years ago, and my
memory is not good, but I believe that the distinction
between a shallow and a deep embedding was introduced
by me in a talk I gave to the Hardware Verification
Group at Cambridge to explain how we did Z in HOL
(in the early 90's).
Of the two kinds of embedding which I distinguished in
that talk, ProofPower employs the shallower, but when
I years later described the ProofPower embedding to
someone as shallow they got quite the wrong idea
about how shallow it was.  It is for example, not
so shallow as the lightweight support for Z later
developed for Cambridge HOL by Mike Gordon.

In terminology I then employed a deep embedding
would have been one in which a HOL type representing
the abstract syntax of Z had been introduced, together
with a formal semantics of Z in HOL.
This could not have been done in HOL without strengthening
HOL with a new axiom (since HOL and Z are equiconsistent
and such a definition of the semantics of Z in HOL would
have allowed a consistency proof for Z in HOL), and would
not have allowed the type systems of Z and HOL to correspond
as closely as they do in the ProofPower implementation.
In the "shallow" embedding we employ, there is for each
syntactic constructor in Z a corresponding constant
(or a family of constants where the type system makes it
necessary) defined in HOL.  Sometimes this is just one
of the existing constants (e.g. for the propositional
connectives), but mostly it is a constant or family
of constants defined to capture correctly the semantics
of the Z construct.
An expression in Z is then represented as a HOL TERM
in which the relevant constant is applied to the
representations of the subexpressions.

A key distinction between shallow and deep embeddings
in the senses used here is that a shallow embedding does
not formalise the semantics in the object language,
and cannot therefore be used directly for reasoning
about the semantics of the embedded language.
ProofPower's shallow embedding was not intended for
metatheory. It was intended to provide practical
support for reasoning in Z, not about Z.
Of course you could take the formal specification
I mentioned above and reason about that with ProofPower,
though in fact I don't believe it was ever prepared
using the necessary document preparation tools to put
it through ProofPower (they didn't exist when I wrote
it). I can't remember how we produced Z documents in
those days, its probably pretty awful, and it may
no longer be possible to print them.

> 2) In the "ProofPower Description Manual", I can read
> about an approximation to the Z language. I´d like to
> know if there is a a .doc explaining explicity the
> diference between the standard and the approximation.

I don't know of one.  Its a good approximation, considering
we did it before the standardisation work started!

> 3) I´ve not seen any explicity proof in the ProofPower
> documentation about the initialisation theorem. I
> think it could useful for newbies in ProofPower and Z.

I'm afraid I don't know what that is!

> 4) In the Z style states-operations, can I have two
> initial states or can an operation generate two or
> more states? I mean I´d like to know if the Z style is
> a deterministic automata or not..

Initial states are an informal naming convention.
ProofPower doesn't know anything about these things.
It won't let you introduce two different schemas with
the same name, but you could certainly have an initial
state schema which didn't uniquely determine the initial
state.  I would have thought that was quite common.

Z operations are relations.
They need not be functional.
As to what it means when they are not, i.e. whether this
is looseness or non-determinism, this used to be a bit of
a muddle.
I don't know whether the Z standard or any other work
clarified this at all.
Perhaps Rob or Steve might comment.

Roger Jones