[sv-bc] naive questions about types

Hi Folks:

I have been mulling over the thought of removing the rewriting
algorithm from Annex F as defined in 1549 and 1667, as was mentioned
in today's SV-SC meeting.

I'm hesitant to do this simply out of fear that something is broken.

I would rather understand more clearly the issues and see if we can
keep it by setting the proper expectations of what it does and does
not define.

When one enters Annex F one leaves the world of concrete source code
and enters an abstracted world in which a number of things are
presumed known or are not dealt with, such as

- name resolution, including all issues of hierarchical 
  reference
- rules of expression evaluation (excepting, of course, sequence
  and property expressions)
- rules of type casting and coercion


I would like to know from those who understand well the rules of types
and expression evaluation whether the following conjectures, which are
intuitively reasonable to me, are false.  Simple counterexamples will
be appreciated.


CONJECTURE 1.  The relation of matching types defined in 6.22.1 is
an equivalence relation.

CONJECTURE 2.  The relation of equivalent types defined in 6.22.2 
is an equivalence relation.

CONJECTURE 3.  Let e be an expression that is evaluated in a
self-determined context.  Assume that type(e) is defined.  Then
replacing e by type(e)'(e) preserves the quality that type(e)'(e) is
evaluated in a self-determined context, and the result of the
evaluation is the same as the result of the original evaluation of e.

CONJECTURE 4.  Let e be an expression that is evaluated in a context
that is not self-determined.  Then there can be defined at least one 
casting type that is within the equivalence class of matching types 
that includes the contextually determined type for evaluation of e.

CONJECTURE 5.  Let e be an expression that is evaluated in a context 
that is not self-determined.  Assume that t is a casting type that 
is within the equiavalence class of matching types that includes the
contextually determined type for evaluation of e.  Then replacing e
by t'(e) preserves the quality that t'(e) is evaluated in a context
that is not self-determined, and the result of the evaluation is the 
same as the result of the original evaluation of e.


J.H.





-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.