[r6rs-discuss] Re: [Formal] formal comment (ports, characters, strings, Unicode)

From: Thomas Lord <lord>
Date: Tue Mar 20 19:49:05 2007

William D Clinger wrote:
>
> =Meanwhile, you pull the concept of "programmatic equivalence"
> out of thin air and use it as foundation of your argument.
> What you mean, I think, is "observable equivalence",

It is quite fair criticism that "programmatic equivalence" needs
some clarification and, /maybe/ a better name. Lemme try to clear that
up and I'll also leave your message marked to possibly respond to the
other points (but this one is good one to start with).

(1) My topic is two-fold: the universally deterministic behavior of portable
programs and the deterministic behavior of portable programs under
individual
implementations which may have extensions that satisfy the intentions
of conforming extensions. By "universally deterministic behavior" I mean
what you can prove about the I/O behavior of a portable program without
making any assumptions about an implementation other than it conforms.
By "deterministic [...] under individual implementations" I mean what you
can prove about a portable program's I/O behavior, leaving some
implementation-dependent terms in your conclusions that depend on nothing
other than conformance of extensions.

(2) It's a theorem, basically, that if we (define eq? eqv?), that the
universally deterministic behavior of portable programs is unaffected.

(3) I think it also a theorem, and intention, that the universally
deterministic behavior of portable programs is unchanged by any
substitution of EQV values.

I hope that you find (2) and (3) uncontroversial.

Where I think we are talking about parting ways (thought I still hope
you'll change your mind) is regarding an extension of (3) to cover what
we can say about the deterministic behavior of a portable program
within a single implementation, given an environment in that implementation
where (define eq? eqv?).

I expect the definition of Scheme to require that, in any conforming
implementation, if we are running with (define eq? eqv?), then
the observational effect of a portable program is invariant even under
various reasonable ways of substituting EQV values for one another
at run-time. I gather that you are suggesting otherwise.

Another way to say that is that I think the only clear reading of
original intent in the EQ/EQV distinction is such that, once we identify
EQ with EQV, values which are EQV are indistinguishable for any
observable purpose, regardless of what conforming extensions are present.

(Similar substitutability requirements apply to EQ values but
the present discussion is simplified if we focus on EQV. Briefly,
EQ is the least approximation of programmatic equivalence that
portable programs can rely on while EQV is the strongest approximation.)

So, under this reading, if two characters are distinguishable in
any way, even by conforming but non-standard extensions, then they
must not be EQV. That doesn't add up, though, given 5.92's language
about the CHAR type, CHAR=, EQV, and "the set of characters".

If you have some more principled explanation of EQV as an alternative,
I'd like to hear it. That, in your view, a lot of people don't understand
it isn't, in my view, a particularly good reason to mess it up.

-t
Received on Tue Mar 20 2007 - 19:58:46 UTC