Phil,
On 6 Jul 2011, at 16:15, Phil Clayton wrote:
On 21/06/11 16:58, Phil Clayton wrote:
Is there any reason why a schema argument in a predicate stub (_?) isn't
implicitly converted to a predicate?
A Z specification taking a Standard-compatible approach to booleans may
have:
BOOL == P []
True == [| true]
False == [| false]
if True then X else Y
However, this produces a type error: we must explicitly say that True is
to be taken as a predicate, i.e.
if %Pi% True then X else Y
which seems unnecessary.
The parser and type checker are doing what the ProofPower-Z language
description says and no more: it talks about the stubs _? and _! in terms of
the syntactic context in which operands are parsed and says nothing about what
happens after that. And, in fact, they currently have no effect on
type-checking. You will find that the following actually works:
if True %and% False then X else Y
This is because the parser knows that the conjunction must be predicate
conjunction and passes that information on to the type-checker, which then does
the right thing and converts the operands of the conjunction into predicates. I
agree with you that it would be much better to have the type checker treat
contexts corresponding to _? stubs as contexts in which schema expressions are
converted into booleans.
I note that the built-in function %Pi% (that forces its argument to be taken
as a predicate) is defined using a predicate stub (_?) but _does_ convert
schemas to schemas as predicates. It is the special handling of %Pi% during
type-checking that achieves this conversion, not the predicate stub.
Yes. I agree it would be better if the type inference aspects of %Pi% came from
a general rule about predicate stubs. (%Pi% would still be treated specially,
in that it is removed from the final type-checked term).
It would certainly make sense for predicate stubs to be type-checked as
predicates. (I was about to modify the type-checker to do that, which looks
fairly simple.) Thus, given
function (op1 _?)
I would expect
%SZT% [ | op1 2] %%
to fail because 2 is not a predicate, irrespective of any definition op1 may
have. Is there any reason ProofPower-Z does not want this behaviour?
No. It is just a historical accident that things are as they are.
There is also the question of whether context stubs (_!) should be checked as
predicates when the context is a predicate. Given
function (op2 _!)
would we expect
%SZT% [ | op2 2] %%
to fail because 2 is not a predicate? (Irrespective of any definition op2
may have.) I think I would. (This looks more effort to implement.)
I would put it slightly differently: I can't imagine any useful definition of
op2 in which it would have a context stub for its operand and be capable of
delivering a truth value when its operand is a number. So I agree with your
suggestion that context stubs be type-checked as predicates in predicate
contexts. A little bit of experimentation with conditionals also supports this.
E.g., try the following:
(1) [|if 1 = 2 then True else True]
(2) [|if 1 = 2 then True %and% False else (False %and% True)]
(3) [|if 1 = 2 then True %and% False else True]
(1) and (2) work, but if you pick the terms apart you will find that the
conversion from schema to predicate has happened as late as possible in (1) and
as early as possible in (2). (3) fails because the else part is type-checked as
a schema and its type doesn't unify with the type %bbB% of the then part. If
the predicate context was passed into the type-checking all (3) would work and
the conversion of schemas to predicates would be treated uniformly.
I will look into implementing something along these lines.
Regards,
Rob.
___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
