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

From: Thomas Lord <lord>
Date: Tue Mar 20 16:07:42 2007

William D Clinger wrote:
>> Characters are objects that represent Unicode scalar values [...].
>> [....]
>> Given a character, char->integer returns its Unicode scalar value as
>> an exact integer.
>> [....]
>> These procedures impose a total ordering on the set of characters
>> according to their Unicode scalar values.
>>
>> All three but especially the last statement are particularly damning.
>> A total ordering according to scalar values clearly implies that the
>> CHAR type contains no more values than there are scalar value
>> integers.
>>
>
> Whether a binary relation is a total ordering depends upon
> some notion of equality. If you take char=? (or eqv?) to
> be that notion of equality, then char<=? does indeed define
> a total ordering on the set of characters.
>

I think you are being too slippery (or, to borrow your word,
"incoherent") with equality.

5.92 in referring to a "set of characters", in the context of a
programming language, surely means that set to be constructively
defined in all implementations and to include a primal equality
relation (let's leave aside for a moment whether or which of
EQ?, EQV?, or EQUAL? reflect that equality relation).

If another relation induces a total order on that set, using ordinary
english, we would expect that total order to refer to the same
equality relation we use when speaking of, for example,
coextensionality of subsets.

For example, we would reasonably expect to be able to make
practical use of the theorem that any subset of a totally ordered
finite set has has a unique minimum and maximum. That theorem
is applicable to programs and assurance that it is true for the CHAR
type seems to follow from the plain language of 5.92. Yet in
your imagined 5.92+extended-chars, that theorem would not hold.

You are saying that, no, the equality that matters for
coextensionality of sets of characters is not the same equality
of total orders. Hrrm. In that case, 5.93 should more
properly say that that CHAR<=? family of predicates define
a total ordering among *equivalence classes of* CHAR values,
where the equivalence classes are given by CHAR=?, which
incidentally should not be mistaken for a predicate that
reliably computes character equivalence.




> If you take klepto:char=? (or eq?) to be the notion of
> equality, then char<=? may not define a total ordering on
> the set of characters. So what?
>
>

The language of 5.92 describes a total order over a set, not a
total order over equivalence classes of a set.



> One last example shows why it is unreasonable to interpret
> the language of the draft R6RS to mean that char<=? defines
> a total ordering with respect to all possible equivalence
> predicates:
>
> (define (klepto:char-equiv? c1 c2)
> (let ((i1 (char->integer c1))
> (i2 (char->integer c2)))
> (or (and (< i1 256) (< i2 256))
> (and (>= i1 256) (>= i2 256)))))
>
> That is an equivalence predicate, and it is definable in
> R5.92 Scheme, but char<=? does not define a total ordering
> with respect to that predicate.
>

No, but 5.92 refers to a constructive set with a reasonable equality
predicate and also goes on to describe that set as totally ordered.
It is "lawyerly" in the worst possible sense of the word to argue,
retrospectively, that really two different notions of equality are
being used.


-t
Received on Tue Mar 20 2007 - 16:17:18 UTC