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

Reply via email to