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.
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.
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?
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.)
Phil
_______________________________________________
Proofpower mailing list
[email protected]
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
