Re: [Axiom-developer] Re: rep, per, Rep in SPAD/Aldor

[Gabriel Dos Reis]

Ralf Hemmecke <address@hidden> writes:

| Gaby,
| 
| just a short reply. As I said, I agree that Rep is an important
| issue. It would actually be good to hear what Stephen Watt has to say
| about that issue. I'd like to learn about the original intentions.
| 
| > Secondly, what we want to convey with `rep' is not that one can take
| > object foo, restrict its interpretation at type T and then do an `on
| > faith interpretation of its sequence of bytes representation as an
| > object at type U'.   Rather, what we want to say is that object foo
| > at type T is the result of a (hopefully injective) mapping from U
| > and we are interested in its pre-image.
| 
| I don't know that I understand that paragraph. If I understand that
| correctly, then (U = Rep, T = %)
| 
| per: Rep -> %     injective map
|    In general we have card(Rep)>=card(%). (If this would not always be
|    true then I don't know.)
| 
| rep: % -> Rep     the "inverse" of per
|    If x is from % then rep(x) should be an element from Rep such that
|    per(rep x) = x. Since there might be several such elements, rep should
|    choose one, and since we want rep to be a function, it should always
|    choose the same element from the preimage of per.
| 
| Gaby, what you were saying is that Rep and % (in an abstract setting)
| need not be represented by the same string of bytes in memory. 

You understand me correctly.

| That is
| my interpretation of your paragraph. Abstractly seen, this seems to be
| OK, but from an efficiency point of view, it is probably always good
| if rep and per actually do nothing than changing the view on the same
| string of bytes in memory.

Depending on the application, yes.

| But, I agree, that decision should be left to the compiler.

-- gaby