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

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

William D Clinger wrote:
> I am posting this as an individual member of the Scheme
> community. I am not speaking for the R6RS editors, and
> this message should not be confused with the editors'
> eventual formal response.
>
> Thomas Lord wrote:
>
>> 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).
>>
>
> It most surely does not mean that. All previous reports
> have been axiomatic in character, not constructive,


Yet effective implementations are, by definition, constructive in
character. Nevermind that the traditional semantics can
arguably be formalized in a constructive framework, regardless,
they are meant to characterize a class of constructive theories
(the class of possible implementations). That is to say, they are
axioms intended to be *about* constructive systems, which is
all that is required for my line of argument.

Look, as an aside, even if I were to grant (which I don't but if I were to)
that the language as written reasonably supposes a CHAR=?
which describes an equivalence class among programmatically
distinguishable character values, even then you've got other
problems. For example, surely if the intent includes permitting
bucky-bitted characters then, at the very least, 5.92's CHAR->INTEGER
is poorly named (given the natural integer mapping of bucky-bitted
characters outside the range of scalar values).

But this foundational stuff is, I agree, getting to the heart of
the matter so let's continue to dig in.


>
>> The language of 5.92 describes a total order over a set, not a
>> total order over equivalence classes of a set.
>>
>
> The notion of a set is itself relative to some notion of
> equality. If you don't believe me, go look at ZF.
>
>


Believe you? Gee, I thought I was pointing that out.
(He's referring to "Zermelo Fraenkel" for anyone who
may be having fun wikipedia-ing or google-ing along
at home.)


>> 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.
>>
>
> No, the draft states axioms that all implementations must
> satisfy with respect to particular equality predicates.
> It neither states nor implies anything with respect to
> equality predicates that are neither mentioned nor implied
> by the draft.
>
>


If a programmatic equivalence predicate, relative to each particular
implementation, isn't implied by "the set of characters" then I don't
know what is.


"The horse died yesterday. I rode the horse to work today." You
see, I meant two different horses, get it, fooledyadiddni, haha?!?!

Now, the axiomatic concept of programmatic equivalence simply
can't be reified as an effective procedure, sure -- but don't we expect
EQV? to at least be consistent with that (never returning #t for
distinguishable
values)? For example, the syntax:

      (define-syntax noop-on-vars
         (syntax-rules ()
            ((noop-on-vars a b) (eqv? a b) (swap! a b))))

should, in fact, define a form that is a noop when applied to a
pair of mutable variables (for a suitable definition of swap)
(except, perhaps, in cases where invoking EQV? or the hypothesized
SWAP! results in some permitted divergence).


In that case, you can't have the 5.92 definition that insists EQV?
behaves like CHAR=? and simultaneously have the, let's call it
"liberal" reading you give the section on the CHAR type. I know,
you already mentioned the possibility of messing with EQV?
here, but, really? Is it that you don't want EQV? to be consistent
with proved programmatic equivalence or that you want to hork
all existing code that uses EQV? rather than EQUAL? in
contexts where it is applied to characters? Or what?

>> It is "lawyerly" in the worst possible sense of the word to argue,
>> retrospectively, that really two different notions of equality are
>> being used.
>>
>
> The draft itself refers to several different notions of
> equality, and is usually careful (though sometimes not as
> careful as it should be) to identify those predicates.
>
> That is common sense.
>
> For you to hold that the draft states or implies that
> char<=? is a total ordering with respect to arbitrary
> implementation-dependent predicates,

No, neither arbitrary nor implementation-dependent. It refers
to "the set of characters," presumably within a given implementation.
It asserts that the set is totally ordered. It effectively states axioms
that mean there exactly as many character values, in *any* implementation,
as there are Unicode scalar values. In the sense of dead horses, referred
to above, I don't see how you can reasonably expect a reader to look at
the definition of CHAR and think that bucky-bitted characters are a
permitted extension (nevermind any of the other plausible extensions that
have been mentioned).


> after I have written
> a concrete example to illustrate the absurdity of such a
> claim---well, that seems pretty disingenuous to me.
>

Well, I guess we're even then. ;-) (sorry, I implied a similar thing
about
you and that was equally rude :-( )



> There is no need for either of us to insult the lawyers.
>
>

Eh. There is no insult in pointing out flaws in an argument
or in attributing implausibly slippery readings of a text to
"the worst kind" of lawyerliness. Arguably, it's a compliment
to the profession.

-t



> Will
>
>
Received on Tue Mar 20 2007 - 17:58:38 UTC