Poll: should Jeffrey Mark Siskind be drawn and quartered (three times)?

TO DEPEND UPON THE FIXED ORDER OF EVALUATION IS UNIVERSALLY
REGARDED AS EXTREMELY BAD STYLE; PERPETRATORS OF THIS STYLE
SHOULD BE DRAWN AND QUARTERED.

I don't have an opinion as to whether it is a good idea or a bad idea
to leave
evaluation order unspecified in a programming language. There are
valid
arguments for both design choices. Rather, the purpose of this email
is to
show it may not be so simple to say whether given code "depends on
evaluation
order".

Over the past few weeks, I've written the following the following
three code
fragments:

(define (alpha-convert e map)
(let alpha-convert ((e e) (map '()))
(cond ((variable-access-expression? e)
(mapping-new (find-if (lambda (mapping)
(eq? (mapping-old mapping)
(variable-access-expression-variable e)))
map)))
((application? e)
(make-application (alpha-convert (application-callee e) map)
(alpha-convert (application-argument e) map)))
((lambda-expression? e)
(let ((x (gensym)))
(make-lambda-expression
x
(alpha-convert (lambda-expression-body e)
(cons (make-mapping (lambda-expression-variable e) x)
map)))))
(else (fuck-up)))))

(define (to-a-normal-form e)
(cond
((variable-access-expression? e)
(let ((x (gensym))) (make-anf x (list (make-variable-binding x
e)))))
((application? e)
(let ((anf1 (to-a-normal-form (application-callee e)))
(anf2 (to-a-normal-form (application-argument e)))
(x (gensym)))
(make-anf
x
(append (anf-bindings anf1)
(anf-bindings anf2)
(list
(make-variable-binding
x
(make-application
(make-variable-access-expression (anf-variable anf1))
(make-variable-access-expression (anf-variable anf2)))))))))
((lambda-expression? e)
(let ((anf (to-a-normal-form (lambda-expression-body e))) (x
(gensym)))
(make-anf
x
(list
(make-variable-binding
x (make-let* (anf-bindings anf)
(make-variable-access-expression (anf-variable anf))))))))
(else (fuck-up))))

(define (call callee argument)
(cond ((primitive-procedure? callee)
((primitive-procedure-procedure callee) argument))
((closure? callee)
(evaluate (closure-body callee) argument (closure-values callee)))
(else (run-time-error "Target is not a procedure" callee))))

(define (evaluate e v vs)
(define (lookup-value i) (if (= i -1) v (vector-ref vs i)))
(cond ((variable-access-expression? e)
(lookup-value (variable-access-expression-index e)))
((application? e)
(call (evaluate (application-callee e) v vs)
(evaluate (application-argument e) v vs)))
((lambda-expression? e)
(make-closure
(map-vector lookup-value (lambda-expression-free-variable-indices
e))
(lambda-expression-body e)))
(else (fuck-up))))

These code fragments would be very familiar to anyone who works on
programming language semantics or implementation.

Question: do these code fragments depend on evaluation order?
Answer: it depends on what you mean by by "depend on evaluation
order".

One one hand, the above procedures are correct. They correctly
performs alpha
conversion, conversion to A-normal form, and applicative-order
evaluation of
the lambda calculus. They obey the properties that such processes are
designed
to obey. On the other hand, the alpha-converted code and the
A-normal form code can differ (in the name of the gensymed variables
and the order of the bindings)
depending on the evaluation order. And while the evaluator always
produces the
same result because all of the primitives are free of side effects, if
you
instrument the evaluator for debugging purposes, the order-of
evaluation
becomes visible.

So the correctness of alpha-convert and to-a-normal-form does not
depend of
evaluation order. But the results do. And even the results of call and
evaluate don't depend on evaluation order. But they do if you add
debugging
statements.

Now, to-a-normal-form can be made independent of evaluation order
simply by
changing:

(let ((anf1 (to-a-normal-form (application-callee e)))
(anf2 (to-a-normal-form (application-argument e)))
(x (gensym)))
...)

to:

(let* ((anf1 (to-a-normal-form (application-callee e)))
(anf2 (to-a-normal-form (application-argument e)))
(x (gensym)))
...)

Not so bad. But the other two require changing:

(make-application (alpha-convert (application-callee e) map)
(alpha-convert (application-argument e) map)))

to:

(let* ((callee (alpha-convert (application-callee e) map))
(argument (alpha-convert (application-argument e)
map)))
(make-application callee argument))

and:

(call (evaluate (application-callee e) v vs)
(evaluate (application-argument e) v vs)))

to:

(let* ((callee (evaluate (application-callee e) v vs))
(argument (evaluate (application-argument e) v vs)))
(call callee argument))

One can argue that such changes are undesirable. Because the
traditional way
of writing these processes in mathematical notation does not involve
such
transformation. Something like:

A(e1 e2, m) = A(e1, m) A(e2, m)
E(e1 e2, v, V) = E(e1, v, V)(E(e2, v, V))

And it is desirable for programs to transparently reflect the
underlying
mathematics.

Jeffrey Mark Siskind wrote:
> One can argue that such changes are undesirable. Because the
> traditional way of writing these processes in mathematical notation
> does not involve such transformation. Something like:
>
> A(e1 e2, m) = A(e1, m) A(e2, m)
> E(e1 e2, v, V) = E(e1, v, V)(E(e2, v, V))
>
> And it is desirable for programs to transparently reflect the
> underlying mathematics.

Hmm. I say let's fix the underlying mathematics. Non-computational
mathematics doesn't tend to pay attention to computational issues, of
course. If computational mathematics has inherited that characteristic,
that would seem like a bug.

However, in this case, it seems that the use of order-dependent side effects
in implementing this mathematics leads to a dependency on evaluation order,
which then has to be dealt with. This is not so much a question of whether
the mathematics can be implemented transparently, as which tools are chosen
to do that. Gensym seems like one of the weak points here. (Clearly, the
solution is to use a monadic gensym...

Re the clumsier notation that can arise when evaluation order needs to be
specified: it certainly seems as though a special form or two could address
that, and once again, such cases are the exceptional ones. Would it really
make sense to fix a useful evaluation order throughout all of e.g. Stalin's
30K+ lines of source code, just to make a few otherwise exceptional cases
like these indistinguishable from all the rest of the code? Do you really
want such cases to be indistinguishable in that way?

Anton

qobi@purdue.edu (Jeffrey Mark Siskind) wrote in message news:<a520654a.0410070839.74d25c49@posting.google. com>...
> One can argue that such changes are undesirable. Because the
> traditional way
> of writing these processes in mathematical notation does not involve
> such
> transformation.

No, the mathematical notations of stateful processes _do_ tend to use
explicit state passing.

> Something like:
>
> A(e1 e2, m) = A(e1, m) A(e2, m)
> E(e1 e2, v, V) = E(e1, v, V)(E(e2, v, V))
>
> And it is desirable for programs to transparently reflect the
> underlying
> mathematics.

Correct. If the mathematical transformation is not a stateful process
(e.g., whose state is that of GENSYM), neither should the code use such
state explicitly; on the other hand, mathematical operations that _do_
involve stateful processes tend to have the state explicitly written
out, and the code should reflect this explicit ordering.

If I understood Siskind's example correctly, it uses allocation
effects rather than mutation effects. Here is a simpler example
of the interaction between allocation effects and the order of
evaluation:

(list (cons 1 '()) (cons 2 '()))

The locations that are allocated to represent the results of the
two calls to cons depend upon the order of evaluation. We don't
usually think about those allocation effects, because they are
invisible in Scheme, but they are visible to programmers who use
low-level debuggers.

For this discussion, the main difference between cons and gensym
is that the allocation effects of gensym are visible to the Scheme
programmer. There is no harm in that, so long as the rest of the
program is as oblivious to alpha-conversion of gensyms as it is to
alpha-conversion of the locations allocated by cons.

As that is presumably the case in Siskind's program, I don't think
his program depends upon the order of evaluation. It was a good
example, though, showing that the meaning of "depends upon" is a
subtle thing that is difficult to state correctly.

Will

qobi@purdue.edu (Jeffrey Mark Siskind) wrote in message
news:<a520654a.0410070839.74d25c49@posting.google. com>...

Jeff, I've just got 2 cents to add to Will's excellent reply:

And it is desirable for programs to transparently reflect the
underlying mathematics.

Sure, but I don't think you gave a good example here. I bother to
complain, as I thought you posted a great point on 2003-07-23, that we
should use some/every as Scheme predicates, to reflect underlying
Math, where we constantly use the quantifiers \forall & \exists.

OK, but I don't see the underlying mathematics here. Now I apologize
for not reading your code carefully. But you described it as:

They correctly performs alpha conversion, conversion to A-normal
form, and applicative-order evaluation of the lambda calculus.

That sounds like what we were arguing about in PLAI: to beta-reduce

((\x. M) P) ---> M[x <- P]

we must alpha convert M so that no free variables of P are captured in
M. The simplest way to do that is just rename all the bound variables
of M to be distinct from all the free variables of P. Then we can
just replace each free (not bound!) occurrence of x in M with P.

Am I getting this right? If so, I don't see the Math connection,
because the new names of these new bound variable means nothing
mathematically, nor what order we perform the alpha-conversions in.
And the sensible way to handle this is with deBruijn trees, as I do in
my LC_v code on web page. There's a powerful mathematical principle
here, as you know well: if you're doing "random" Math, try to redo it
so that the "random" Math (the new bound variable names) gets removed.

So I'd say Scheme does reflect the underlying mathematics here: what
doesn't mean anything mathematically is done "randomly" in Scheme.

Would you agree? Can you give a better example? Back to the top:

TO DEPEND UPON THE FIXED ORDER OF EVALUATION IS UNIVERSALLY
REGARDED AS EXTREMELY BAD STYLE;

I don't think this is true anymore. On plt-scheme, Shriram posted
that he thought that depending on the MzScheme left->right eval order
was perfectly good style. I don't see any problem with that. I'm
sure nobody wants to start up that flame-war again, right guys?

PERPETRATORS OF THIS STYLE SHOULD BE DRAWN AND QUARTERED.

Ah, the thread-name! Duh. So maybe you don't believe it's EXTREMELY
BAD STYLE yourself.