On 11/07/11 13:37, Rob Arthan wrote:
Further to my earlier reply to Phil's suggestion (outlined below), I
have looked into implementing it and it all looks good to me.

That's good - I was poised to have a go myself!

There is
only one consequence that I can see that looks a little strange at
first, but makes sense when you think about it. This is the treatment of
conditionals in quotations. If you enter:

%SZT% if 1 = 2 then 3 else 4 %>%

it will fail, because the top level of a Z quotation is a predicate
context (but not an operand of a stub, so non-predicates are allowed).
To get this to work you have to force an expression context:

%SZT% (if 1 = 2 then 3 else 4) %bigcolon% %bbU %>%

Arguably we should have a separate quotation symbol to introduce a Z
expression. The justification for the quotation to default to predicate
is easy to see when you think about entering ordinary logical
expressions: it would be very painful if they defaulted to being treated
as schema expressions. I think the above slight complication (which is
specific to conditionals or user-defined things like them) is worth the
improved uniformity of the new approach.

I agree with your view. Although it may be necessary to force an expression for such terms, overall I think the behaviour is clearer because it's more uniform.

Whether to have a separate expression quotations is an interesting question. The need to force an expression is not that common so %bigcolon% %bbU% seems all right. It just takes getting used to. Expression quotations would be clearer and more intuitive though.




On 11 Jul 2011, at 09:45, Rob Arthan wrote:


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? ...

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 will look into implementing something along these lines.



Proofpower mailing list <>

Proofpower mailing list

Proofpower mailing list

Reply via email to