On 10 Apr 2013, at 11:04, Freek Wiedijk wrote:
>>
> What I just want is to have some story + infrastructure
> that allows me to -- at the very very end -- prove that
> the result that I have established is "meaningful", in the
> sense that it doesn't depend on/refer to what functions do
> outside their domain. But that apart from that _everything_
> is as it was before.
Because the Z type system takes power set and products as primitive rather than
function spaces, Z models functions as sets of pairs and so function
application is a partial operation in general Z. Dealing with undefined terms
is therefore even more of an issue than it is for HOL. The original semantics
for Z decreed that the primitive relations in Z (set membership and equality)
were false if either operand is undefined. Many people liked this and it can be
quite convenient in writing specifications, but it can also be highly
counter-intuitive (e.g, f(x) < f(y), f(x) = f(y) and f(x) > f(y) may all be
false), so many others deprecate it and avoid writing things that are sensitive
to the values of undefined terms. The ISO standard for Z endeavours to allow
tools some freedom about the treatment of undefined terms, but I am not sure
how successful this has really turned out to be.
My take has always been that mechanized proof is hard enough even with a
completely classical approach to undefined terms, so I advocate a separate
analysis to investigate the dependency of specifications and statements of
theorems on the semantics of undefinedness. Unfortunately, I have never had an
opportunity to do much work on this in ProofPower. The Z/EVES system had a
feature like this. Given a Z specification it could generate a set of proof
obligations called domain conditions. The idea was that if the domain
conditions were true, then the specification was insensitive to the
interpretation of undefined terms. This was quite popular because the domain
conditions were very often automatically provable, so even users who were only
interested in writing specifications got some value out of the proof tool. The
reference gives some information about this. I thought Mark Saaltink had
written a more detailed account, but possibly that was in a technical report
that isn't available any more.
It ought to be feasible to do something similar for HOL.
Regards,
Rob.
@inproceedings{DBLP
:conf/zum/Saaltink97,
author = {Mark Saaltink},
title = {The Z/EVES System},
booktitle = {ZUM},
year = {1997},
pages = {72-85},
ee = {http://dx.doi.org/10.1007/BFb0027284},
crossref = {DBLP:conf/zum/1997},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP
:conf/zum/1997,
editor = {Jonathan P. Bowen and
Michael G. Hinchey and
David Till},
title = {ZUM '97: The Z Formal Specification Notation, 10th International
Conference of Z Users, Reading, UK, April 3-4, 1997,
Proceedings},
booktitle = {ZUM},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {1212},
year = {1997},
isbn = {3-540-62717-0},
bibsource = {DBLP, http://dblp.uni-trier.de}
}------------------------------------------------------------------------------
Precog is a next-generation analytics platform capable of advanced
analytics on semi-structured data. The platform includes APIs for building
apps and a phenomenal toolset for data science. Developers can use
our toolset for easy data analysis & visualization. Get a free account!
http://www2.precog.com/precogplatform/slashdotnewsletter
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
