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

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

Phil

Attachment: char_tuple_issue.sml.gz
Description: GNU Zip compressed data

Attachment: imp062.doc.patch.gz
Description: GNU Zip compressed data

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

Reply via email to