[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: transitivity does not imply type-checking

Matthias wrote:
> Take for example the following definition of =:
> (define (= x y . rest)
>   (and (number? x) (number? y)
>        (prim= x y)
>        (or (null? rest) (apply my= y rest))))
> I claim that this meets the transitivity requirement of R5RS,

> assuming prim= is transitive, yet it only type-checks used args.

Actually, when SRFI 67 got made we tried to find out what the
authors of R5RS actually meant by saying (R5RS, Section 6.2.5.):

<quote>These predicates are required to be transitive.

Note: The traditional implementations of these predicates in
Lisp-like languages are not transitive.</quote>

Unfortunately, it is not clear what the authors of R5RS mean
by requiring a 'predicate' to be 'transitive.' There are (at
least) two possible interpretations:

   #1 The order (or equivalence) relation R represented by <=
(or =) is transitive, in the usual (mathematical) sense you
described, i.e. for all x, y, z from the set of possible
argument values:
   (<= x y) => #t   and   (<= y z) => #t   implies   (<= x z) => #t.
The set of possible argument values are represented by
(REAL? x) => #t for <, <=, >, >=, and by (NUMBER? x) => #t for ="">
unless the implementation chooses to extend it.

   #2 The predicate procedure tests if the argument values form
a chain, i.e. (<= 1 2 3) => #t, and (<= 2 1 3) => #f.

As you pointed out, the choice of interpretation has subtle
implications on semantics---and I do not find either of them
the clear 'this is what is meant' winner. Let me explain
this in greater detail.

Although #1 seems the obvious choice, it does not really make a
lot of sense because = is already defined to be equality, which
by definition is transitive. My doubts got stronger by the claim
that other Lisp-like languages manage to define non-transitive
'equality.' Miracles and wonders! What does that refer to? Maybe
(= nan nan) => #f, as IEEE 754 wants it?

Now #2 is not very compelling either because it gives a rather
unfamiliar meaning to the word 'transitive,' but it could be
that transitivity was the word that came to mind at the time.

Anyway, in #2 you have a very nice property: After evaluating
the test (<= x y z), you have (and (real? x) (real? y) (real? z))
as a post-condition. In #1, the order of testing is unspecified,
so (<= x y z) could be implemented as (and (<= x y) (<= y z)) but
also as (and (<= y z) (<= x y)). In the first case, (<= 2 1 'a)
does not raise an error, in the second case it does. In #1 the
only thing you can say about the arguments after the test is
that at least two of them satisfy real?.

For clarification, I was seeking advice from one or more of the
authors of R5RS to find out what they meant when they required
<= etc. to be 'transitive.' Unfortunately, neither me nor our
editor got any clarifying response. (But we also did not make
it our purpose in life---just a few emails.)

At this point, we cut the theory, ran our favourite Scheme
systems, typed in (<= 2 1 'a), and looked what happened: PLT
and Scheme48 both complain about the type mismatch, i.e. they
type check all arguments whether needed for the result or not.

So, since we wanted (chain<=? compare-real x1 x2 x3 ...) to be
exactly backward compatible with (<= x1 x2 x3 ...), we decided
to require the type checking---and of course to be consistent
this must then be done everywhere. Frankly, I am quite happy
with this choice because it contributes to robustness, more
than it hurts performance---unless you use chain<=? on very
long lists, in which case I would recommend not using APPLY
on an argument lists but rather another 4-line-program:

(define (vector-chain<=? compare vec)
  (every?-ec (:range i 1 (vector-length vec))
             (<=? compare (vector-ref vec (- i 1))
                          (vector-ref vec i))))