Re: [ProofPower] Instantiation of free variables according to some matching.
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. I was often finding that I wanted to backward-chain in Z so I wrote a simple version of z_bc_thm_tac as attached. It may not do everything that is required of such a tactic and doesn't have any proper error management but it has been sufficient for my purposes. Phil The information contained in this E-Mail and any subsequent correspondence is private and is intended solely for the intended recipient(s). The information in this communication may be confidential and/or legally privileged. Nothing in this e-mail is intended to conclude a contract on behalf of QinetiQ or make QinetiQ subject to any other legally binding commitments, unless the e-mail contains an express statement to the contrary or incorporates a formal Purchase Order. For those other than the recipient any disclosure, copying, distribution, or any action taken or omitted to be taken in reliance on such information is prohibited and may be unlawful. Emails and other electronic communication with QinetiQ may be monitored and recorded for business purposes including security, audit and archival purposes. Any response to this email indicates consent to this. Telephone calls to QinetiQ may be monitored or recorded for quality control, security and other business purposes. QinetiQ Limited Registered in England & Wales: Company Number:3796233 Registered office: 85 Buckingham Gate, London SW1E 6PD, United Kingdom Trading address: Cody Technology Park, Cody Building, Ively Road, Farnborough, Hampshire, GU14 0LX, United Kingdom http://www.qinetiq.com/home/notices/legal.html z_bc_thm_tac.doc.gz Description: GNU Zip compressed data ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] Instantiation of free variables according to some matching.
Hi Rob,
Many thanks for the reply and clarification.
All below makes sense. I can see how effectively excluding terms such as
|- n = 1 /\ n = {1}
would in any case impose a big overhead on run-time, requiring some
dynamic type-checking when rules are applied, etc. To exclude such cases
nonetheless I suppose it will be cheapest to do manual checks in one's
own code where this duplicity can arise, and maybe raise custom error
messages or carry out renaming if feasible.
> ... finding a good name for it seems the hardest problem just now :-)
Maybe something like "match_inst_rule" ?
> 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.
Okay, I see. This happens I suppose when the theorem "asms | ant => suc"
used for backward-chaining contains free variables in the antecedent
which do not occur anywhere else, i.e. the assumptions or conclusion of
the implication used for backward-chaining. As far as I can see the
internal bc_rule wraps such free variables into an existential
quantification after the theorem used for backward-chaining has been
matched and suitably instantiated. So, basically, one needs to
reimplement bc_rule as well to ensure that the subgoal generated
(existential quantifiers) remains in the Z language. I might have a
crack at it next week and send a personal email if any success ;-).
Cheers, Rob, for taking the suggestions below into considerations with
the next release of ProofPower, and thanks for the feedback in general,
Frank
Rob Arthan wrote:
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 behaviou
Re: [ProofPower] Instantiation of free variables according to some matching.
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
Re: [ProofPower] Instantiation of free variables according to some matching.
Dear Roger,
Many thanks for the reply.
> It looks like apply_matches_rule will tolerate universal
> quantifiers on the conclusions better than yours, so it
> will just work more often than yours.
> It also has a "caller" parameter to make error reports
> more intelligible, and is complicated by not using the
> asm_inst_ things (i.e. by incorporating that functionality).
I had a closer look at apply_matches_rule and the main difference, as
you explained, is that it will allow the conclusion to be universally
quantified; it eliminates such a quantifier while avoiding clashes with
the free variables of the term prior to performing the matching. Rather
than using asm_inst_term_rule it employs inst_term_rule and therefore
requires a bit more effort to introduce (and eliminate) assumptions into
(and from) the conclusion. As you mentioned, it also gives more
informative error messages mentioning the area of the caller.
Since I don't need this additional feature of removing outer universal
quantifiers in the conclusion of the theorem, I think there is no
genuine advantage in using it in the context of my application. The
additional feature of better error handling is easily supported with
another line of code handling possible exceptions. Maybe
apply_matches_rule could be a nice function to have in the general
interface, what about exposing it?
>> 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? 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} ?
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?
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 ;-).
Roger Bishop Jones wrote:
On Thursday 02 April 2009 18:30:48 Frank Zeyda wrote:
My question is whether
apply_matches_rule behaves differently (better, more powerful?) than the
version above.
I'm not the right person to answer this, but since no-one else
has I'll say what I can.
It looks like apply_matches_rule will tolerate universal
quantifiers on the conclusions better than yours, so it
will just work more often than yours.
It also has a "caller" parameter to make error reports
more intelligible, and is complicated by not using the
asm_inst_ things (i.e. by incorporating that functionality).
Were there any reasons for not exposing it?
The caller parameter would be one.
A second problem: assume that the sub-expression of thm I'm matching
against contains some free variable y (of variable type), and that y
will be associated with some sub-term t according to the matching.
Further, let t also have y free in it. Could there be a problem in this
case? Since y will be substituted anywhere in thm, I would think there
is no risks with substituting y for a term that contains y.
I don't see a problem, but if there was one it would fail
so you don't risk making an unsound inference.
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.
Re: [ProofPower] Instantiation of free variables according to some matching.
On Thursday 02 April 2009 18:30:48 Frank Zeyda wrote: >My question is whether >apply_matches_rule behaves differently (better, more powerful?) than the >version above. I'm not the right person to answer this, but since no-one else has I'll say what I can. It looks like apply_matches_rule will tolerate universal quantifiers on the conclusions better than yours, so it will just work more often than yours. It also has a "caller" parameter to make error reports more intelligible, and is complicated by not using the asm_inst_ things (i.e. by incorporating that functionality). >Were there any reasons for not exposing it? The caller parameter would be one. >A second problem: assume that the sub-expression of thm I'm matching >against contains some free variable y (of variable type), and that y >will be associated with some sub-term t according to the matching. >Further, let t also have y free in it. Could there be a problem in this >case? Since y will be substituted anywhere in thm, I would think there >is no risks with substituting y for a term that contains y. I don't see a problem, but if there was one it would fail so you don't risk making an unsound inference. >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. I think the main problem you will have is in matching against terms containing bound variables. Roger Jones ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
