Frank,
On 7 Apr 2009, at 14:39, Frank Zeyda wrote:
Dear Roger,
Many thanks for the reply.
....
The additional feature of better error handling is easily supported
with another line of code handling possible exceptions.
The idea behind the caller parameter in many of these internal
functions was to make the reporting of the function that was the real
detector of the error more precise. In this case, apply_matches_rule
isn't doing anything very subtle so you are right that the calling
function could do it with a simple handler.
Maybe apply_matches_rule could be a nice function to have in the
general interface, what about exposing it?
In many instances in the original development of ProofPower, there
were instances of general purpose functions like this that were
nearly general enough and useful enough to "productise" but not quite
(e.g., because of the effort involved in getting the error handling
completely general or in documenting exactly what the function does,
or even just thinking up the right name for the function). I will
certainly consider exposing apply_matches_rule - finding a good name
for it seems the hardest problem just now :-)
>> A second case is when y occurs free in both thm and term,
>> is not substituted but nonetheless introduced through the
substitution.
>> I presume this is okay
>> as long as the types of y are identical in thm and term.
>
> Its still OK if the types are not the same, they will be
> logically distinct variables and its a confusing situation
> you shold seek to avoid.
This sounds a little bit curious, is there a document that explains
more about this situation?
There are at least two accounts of the semantics of HOL and they agree
on this point as do the classical references on type theory and on
many-sorted first-order logic. For HOL, I have in mind the account by
Andy Pitts in the Cambridge HOL documentation and my account in HOL in
spc00{1,2,3,4}.doc supplied with ProofPower. It isn't really curious
if you think about it the other way round: how could the semantics
possibly consider two variables with different types to be the same?
In Church's simple type theory and its polymorphic variant HOL, the
types are disjoint.
So although the variables have the same name they are actually
treated as logical distinct by the fact that they have different
types? So instantiation would have be sensitive to variable types
(not just names) and might result in one variables n to be
substitution, while another n is left unaffected e.g. if it has a
different type?
For example, assume we have a theorem thm
n = 1 |- n = {1}
Then (asm_inst_term_rule [(2, n)] thm) would yield
2 = 1 |- n = {1} ?
Absolutely! Instantiation works just like that (it even has to rename
bound variables if the instantiation would cause a capture problem).
But this is a tiny price to pay: the alternative approaches are very
unattractive: e.g., the abstract data type of terms could ban terms
that used the same variable name with different types but that would
impose a big runtime overhead on the constructors for applications and
lambda-abstraction.
Thanks for pointing this out, it clarified one or two behaviours of
ProofPower for me which I could not explain before.
> I think the main problem you will have is in matching against terms
> containing bound variables.
I haven't given considerations to this, but as far as I can see such
a situation may not arise in the particular application. Thanks for
pointing this out!
Cheers once more,
Frank
PS: What about a function that supports backward-chaining with Z
theorems, something like z_bc_tac and z_bc_thm_tac? I suppose this
could be quite useful too. Is there anything more that needs to be
done other than rewriting the Z universal quantifier into a HOL one,
and using the HOL backward-chaining tactics?
Yes. I have been meaning to get round to this for a long time. It
isn't quite as simple as you might think because the Z tactics are
designed to keep in Z, but the back-chaining tactics often need to
produce an existentially quantified goal and that would need to be
converted from HOL back into Z.
PPS: A final comment. To implement some custom error handling I
noticed that there was no functions that could be used to infer the
id of an error message (of type MESSAGE). Since the MESSAGE datatype
is not exposed, we cannot take the message apart; the only solution
seems to be to dissect the string of the error message. If I'm
overlooking something please let me know, otherwise it would be
beneficial to have some function get_id in the general interface of
BasicError to extract the id of an error message ;-).
You aren't overlooking anything. I have thought that a function like
you get_id would be useful in some circumstances. I think I will add a
function that will just let you take the MESSAGE type apart, but with
a warning that it should be used with caution since ti makes your code
very sensitive to changes in the code you are calling.
By the way, it is very good to see that you are boxing very clever
with ProofPower just now!
Regards,
Rob.
_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
