Phil,

On 5 Jun 2011, at 12:10, Phil Clayton wrote:

> (Examples also included in attached file char_tuple_issue.sml)
> 
> After defining e.g.
> 
>  [T]
> 
>  S %def% [X : T]
> 
> the type inference issue with characteristic tuples can be seen when the term
> 
>  {S; S'}
> 
> occurs as a subterm.  For example, the following terms fail when they are 
> being constructed, due to an internal type mismatch:
> 
>  {{S; S'}}
>  {S; S'} = A
> 
> The type of {S; S'} should be the same as for {S; (S)'}, i.e.
> 
>  [X : T] %rel% [X : T]
> 
> However, type inference incorrectly computes the type of {S; S'} as
> 
>  [X : T] %rel% [X' : T]
> 
> - the type of the different term {S; (S ')}.  When terms are constructed 
> after type inference, construction of the characteristic tuple has the 
> correct type.  However, incorrect type annotations can be present elsewhere 
> in the term from type inference, causing the type mismatch when building 
> terms.
> 
> The problem is that type inference generates the characteristic tuple for the 
> schema text, e.g. S; S', before type checking the schema text. Consequently 
> S' has not been converted from a local variable to a decorated global 
> variable when the characteristic tuple is generated, so the characteristic 
> tuple (effectively) contains
> 
>  %theta% (S ')
> 
> rather than
> 
>  %theta% S '
> 
> I think this is fairly simple to fix - see attached patch.

Yes. Thanks.


>  Note that there is no problem with
> 
>  {S; (S)'}
> 
> because there is no local variable S' to cause the problem.  (This can be 
> used as a work-around.)
> 
> I suppose this is a good opportunity to raise item 219, i.e.
> 
> 1. Should the Spivey-Z schema decoration S' be supported in ProofPower-Z?  I 
> believe Standard-Z requires one of
> 
>  (S)'
>  S '
> 
> to decorate a schema reference S.  This avoids the question of what happens 
> when both S and S' are global variable names.
> 

Yes. Horrible isn't it. The space is barbaric by usual mathematical 
typographical standards and is an incompatibility with Spivey Z.

> 2. Should ProofPower-Z allow S ' to be interpreted as the name S', i.e. 
> ignoring space between the two tokens and taking them as one token?  I would 
> never expect e.g. abc def to be taken as the name abcdef.

Apart from the above comment about _mathematical_ typography rather than 
programming language practice, I really don't want to get into a debate about 
why it should or should not be as it is, since I went into this kind of 
question very carefully and at some length during the Z standardisation process 
(see the document Issues for Concrete Syntax at 
http://www.lemma-one.com/zstan_docs/zstan_docs.html). ProofPower-Z implements 
the scheme described there that is backwards compatible with Spivey in all but 
very obscure cases. This was a typical case where one existing tool implemented 
a thought-through approach which gave the desired new semantics using a syntax 
that was designed to be compatible with Spivey at least in typical cases, but, 
while no other tool supported either the desired semantics or the syntax, the 
standards committee chose a different and incompatible approach.

>  Note that when both S and S' are global variable names, S ' is a reference 
> to S' in ProofPower-Z, not the schema decoration of S.  Not only is this 
> surprising, it is different to Standard-Z.  (Section 7.3 in Z Standard.)

Of course, only the seriously crazed declare global variables with decoration 
on them.

Currently, my thinking is that a separate Standard-Z compatible parser would be 
a useful adjunct to ProofPower-Z, but I am still much interested in some level 
of backwards compatibility with Spivey Z, because all the significant specs I 
have come across in industry are in Spivey Z. So I have no plans to throw away 
the existing parser.

Regards,

Rob.

_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Reply via email to