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
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Reply via email to