"The lambda calculus is inconsistent without typing."
Daniel Ortmann
Questions:
1) Is the statement true?
2) Is it true with respect to Scheme?
3) Any enlightening comments?
Thanks!
--
Daniel Ortmann, IBM Circuit Technology, Rochester, MN 55901-7829
ort...@vnet.ibm.com or ort...@us.ibm.com and 507.253.6795 (external)
ort...@rchland.ibm.com and tieline 8.553.6795 (internal)
ort...@isl.net and 507.288.7732 (home)
"The answers are so simple, and we all know where to look,
but it's easier just to avoid the question." -- Kansas
ol...@pobox.com
which sequences of tokens make "well-formed" terms. Its semantics
consists of rewriting rules, which tell how one term may be rewritten
into another. Such a rewriting system can be called inconsistent if a
term A can be rewritten into two "distinct" terms B and C. One can
define terms B and C distinct iff they cannot be rewritten into each
other (not inter-convertible). OTH, one can define two terms
equivalent if they can be re-written (or _reduced_) to a common
term. Fortunately, Church-Rosser Theorems show that the
lambda-calculus is consistent: no term can be converted to two
distinct terms (this is actually a corollary from the Theorem).
Church-Rosser Theorem II proves even a stronger, _constructive_
result. It tells how to find in practice if two terms are equivalent:
one should apply a normal-order reduction to both terms until no
further reduction is possible, and then compare the results.
pp. 364-366 of an excellent survey
Conception, Evolution, and Application of Functional
Programming Languages
Paul Hudak
ACM Computing Surveys, Vol. 21, No.3, Sept 1989
talks about lambda-calculus and consistency in some detail.
Note, some terms in Lambda-calculus do not have a normal
form. Furthermore, if one uses an applicative-order reduction, one can
fail to find a normal form, even if it exists. This gives rise to a
certain inconsistency. For example, consider a term
(\x.\y.z) u ((\x.x x) (\x.x x))
I can re-write in into
(\x.y) ((\x.x x) (\x.x x))
and
y
Are these terms equivalent? If I use a normal-order reduction, I can
show that they are. If I use an applicative-order reduction, then I
will never find the answer. From the constructivist point of view,
the failure to _construct_ a (applicative-order) reduction chain means
terms are not equivalent; hence inconsistency.
Scheme uses an applicative-order evaluation (that is, the
innermost application is evaluated first). This opens up a possibility
of a "constructive" inconsistency:
(define (bottom) (bottom))
(define (foo x) 5)
Let's consider an expression (foo (bottom)). A smart optimizing
compiler may notice that 'foo' and 'bottom' are pure functions, and
foo does not need the result of its argument. The compiler can
therefore compile "(foo (bottom))" to a value 5. A less-smart compiler
(or interpreter) may try to deal with expression head-on, and,
obviously, will never finish. This shows that the same expression,
processed by two different compilers, can yield different
results. Well, if one takes a less-constructivist point of view, he
may declare a non-terminating computation to be equivalent to any
result -- and thus regain consistency. I'm afraid not many
practioners will agree with this interpretation.
Actually, in Scheme even stronger inconsistencies are
possible. Consider
(define x 0)
(+ (begin (set! x 2) x) x)
The latter term can be rewritten either to 4 or 2, depending on the
order an interpreter chooses to evaluate argument expressions. Similar
inconsistencies exist in other languages, for example, i++ + i++
etc. Note how mutations may make life difficult.
Every programming language has semantics, which specifies the
meaning, or interpretation of syntactically-correct terms
(expressions). This semantics can be thought of a set of reduction
rules, which take one expression and re-write it into another -- until
no other reduction rule applies. It may happen that the end result is
a value -- this signifies the success of the computation. The end
result may still be an application of a non-constructor (or a
composite form). For example,
(+ 1 2)
can be reduced further, while (/ 1 0) cannot (as there is no reduction
rule that takes /, a number and zero). Nor can (+ 1 "aaa") be reduced.
This signifies an error -- the computation got stuck and failed to
produce a value. There is the third possibility -- the reduction
process never finishes. One can interpret this result as he wishes.
BTW, the following code
http://pobox.com/~oleg/ftp/c++-digest/lambda-interp.cc
http://pobox.com/~oleg/ftp/Computation/ultimately-static-
typing.txt
gives a simple example of the reductionist semantics. It spells out
rewriting rules that give meaning to arithmetic expressions. The
reduction rules are expressed as C++ templates (with C++ _compiler_
acting as a reduction engine).
Sent via Deja.com http://www.deja.com/
Before you buy.
Simon Helsen
> Scheme uses an applicative-order evaluation (that is, the
>innermost application is evaluated first). This opens up a possibility
>of a "constructive" inconsistency:
>
> (define (bottom) (bottom))
> (define (foo x) 5)
>
>Let's consider an expression (foo (bottom)). A smart optimizing
>compiler may notice that 'foo' and 'bottom' are pure functions, and
>foo does not need the result of its argument. The compiler can
>therefore compile "(foo (bottom))" to a value 5. A less-smart compiler
>(or interpreter) may try to deal with expression head-on, and,
>obviously, will never finish. This shows that the same expression,
>processed by two different compilers, can yield different
>results. Well, if one takes a less-constructivist point of view, he
>may declare a non-terminating computation to be equivalent to any
>result -- and thus regain consistency. I'm afraid not many
>practioners will agree with this interpretation.
But practioners will *expect* the above program not to terminate! An
optimizing compiler is not allowed to change the semantics of a
program. And the semantics of Scheme says that the above
program is not terminating. Non-termination is some kind of side-effect in
applicative order reduction, hence, you cannot eliminate the argument.
regards,
Simon
Joe Marshall
> On Tue, 11 Apr 2000 ol...@pobox.com wrote:
>
> > Scheme uses an applicative-order evaluation (that is, the
> >innermost application is evaluated first). This opens up a possibility
> >of a "constructive" inconsistency:
> >
> > (define (bottom) (bottom))
> > (define (foo x) 5)
> >
> >Let's consider an expression (foo (bottom)). A smart optimizing
> >compiler may notice that 'foo' and 'bottom' are pure functions, and
> >foo does not need the result of its argument. The compiler can
> >therefore compile "(foo (bottom))" to a value 5. A less-smart compiler
> >(or interpreter) may try to deal with expression head-on, and,
> >obviously, will never finish. This shows that the same expression,
> >processed by two different compilers, can yield different
> >results. Well, if one takes a less-constructivist point of view, he
> >may declare a non-terminating computation to be equivalent to any
> >result -- and thus regain consistency. I'm afraid not many
> >practioners will agree with this interpretation.
>
> But practioners will *expect* the above program not to terminate!
They shouldn't.
> An optimizing compiler is not allowed to change the semantics of a
> program.
An optimizing compiler is not allowed to change the semantics of a
*correct* program. It can do what it likes with incorrect ones.
> And the semantics of Scheme says that the above program is
> not terminating. Non-termination is some kind of side-effect in
> applicative order reduction, hence, you cannot eliminate the
> argument.
Compilers don't have to preserve the non-terminating behavior of code
any more than they have to preserve the running time of the code.
They *only* have to preserve the `answer' and the effect on the
`store'. Since the call to (foo (bottom)) has no effect on the store,
and the compiler can prove that the answer cannot be anything but 5,
code that simply returns a 5 is legit.
MIT Scheme, for example, (with the right declarations) will toss out
calls to pure functions if the result is not used, so it will in fact
compile (foo (bottom)) to a value of 5.
They take the view that the compiler object code must terminate with
the same answer as the compiler source code *if the source code in
fact terminates*. If I remember correctly, the compiler is also
allowed to assume that the code terminates with erroneous input.
Suppose we defined bottom as such:
(define (bottom x) (car x) (bottom x))
Foo is defined as before, and bar is defined as
(define (bar) (foo (bottom 42)))
Although the interpreter will get an error trying to take the car of a
number, the compiler can notice that CAR is pure functional, BOTTOM is
pure functional, the results are not used, so it can prove this
statement:
`The function BAR cannot correctly produce an answer other than 5.'
And so it generates the code that returns a 5. If I recall correctly,
the MIT Scheme implementors actually went out of their way to ensure
that this would happen.
However, I don't think it takes the less-constructivist point of view
that a non-terminating computation may be equivalent to *any* result.
For instance, (display (bottom)) will not print anything nor will it
terminate.
--
~jrm
Matthias Blume
> Simon Helsen <hel...@informatik.uni-freiburg.de> writes:
>
> > On Tue, 11 Apr 2000 ol...@pobox.com wrote:
> >
> > > Scheme uses an applicative-order evaluation (that is, the
> > >innermost application is evaluated first). This opens up a possibility
> > >of a "constructive" inconsistency:
> > >
> > > (define (bottom) (bottom))
> > > (define (foo x) 5)
> > >
> > >Let's consider an expression (foo (bottom)). A smart optimizing
> > >compiler may notice that 'foo' and 'bottom' are pure functions, and
> > >foo does not need the result of its argument. The compiler can
> > >therefore compile "(foo (bottom))" to a value 5. A less-smart compiler
> > >(or interpreter) may try to deal with expression head-on, and,
> > >obviously, will never finish. This shows that the same expression,
> > >processed by two different compilers, can yield different
> > >results. Well, if one takes a less-constructivist point of view, he
> > >may declare a non-terminating computation to be equivalent to any
> > >result -- and thus regain consistency. I'm afraid not many
> > >practioners will agree with this interpretation.
> >
> > But practioners will *expect* the above program not to terminate!
>
> They shouldn't.
As far as "should" and "shouldn't" goes, the language definition
_should_ be explicit as to which programs terminate and which don't.
The "practitioner" then _should_ rely on the definition.
> > An optimizing compiler is not allowed to change the semantics of a
> > program.
>
> An optimizing compiler is not allowed to change the semantics of a
> *correct* program. It can do what it likes with incorrect ones.
Actually, a compiler, optimizing or not, should reject incorrect
programs. And indeed, for correct programs it should not change the
semantics.
As far as I know, the above program is correct Scheme, so a compiler
that turns the "bottom" loop into something that terminates has
changed the semantics of a correct program.
> Compilers don't have to preserve the non-terminating behavior of code
> any more than they have to preserve the running time of the code.
Says who?
> MIT Scheme, for example, (with the right declarations) will toss out
> calls to pure functions if the result is not used, so it will in fact
> compile (foo (bottom)) to a value of 5.
But "bottom" is not pure as it does not return at all. Or at least it
shouldn't.
> They take the view that the compiler object code must terminate with
> the same answer as the compiler source code *if the source code in
> fact terminates*. If I remember correctly, the compiler is also
> allowed to assume that the code terminates with erroneous input.
> Suppose we defined bottom as such:
> (define (bottom x) (car x) (bottom x))
> Foo is defined as before, and bar is defined as
> (define (bar) (foo (bottom 42)))
>
> Although the interpreter will get an error trying to take the car of a
> number, the compiler can notice that CAR is pure functional, BOTTOM is
> pure functional, the results are not used, so it can prove this
> statement:
>
> `The function BAR cannot correctly produce an answer other than 5.'
>
> And so it generates the code that returns a 5. If I recall correctly,
> the MIT Scheme implementors actually went out of their way to ensure
> that this would happen.
Someone obviously had too much time on their hands -- time that could
have better be spent on some nice little flamewar in c.l.s. :)
Matthias
--
Matthias Blume <blume@k_u_r_i_m_s.k_y_o_t_o-u.a_c.j_p>
Kyoto University, Research Institute for Mathematical Sciences
(remove underscores in mail address; they are there to fight spam)
Joe Marshall
> As far as "should" and "shouldn't" goes, the language definition
> _should_ be explicit as to which programs terminate and which don't.
> The "practitioner" then _should_ rely on the definition.
How could it be? If the language definition were explicit about which
programs terminate and which don't, wouldn't it require a means to
decide whether a particular program was terminating or not?
> > > An optimizing compiler is not allowed to change the semantics of a
> > > program.
> >
> > An optimizing compiler is not allowed to change the semantics of a
> > *correct* program. It can do what it likes with incorrect ones.
>
> Actually, a compiler, optimizing or not, should reject incorrect
> programs.
You have to qualify this. Compilers can discriminate between three
kinds of programs: ones provably correct, ones provably incorrect, and
ones for which correctness or incorrectness is statically
undecideable. I *hate* compilers that reject all code not in the
first category, and even in the case of provably incorrect programs, I
might want to compile it *anyway* so I can debug parts of the program.
> And indeed, for correct programs it should not change the semantics.
> As far as I know, the above program is correct Scheme, so a compiler
> that turns the "bottom" loop into something that terminates has
> changed the semantics of a correct program.
I think we're arguing about angels and pinheads, so to speak.
We might want the compiler to be such that the object code behaves in
all observable ways exactly like the source code.
We might want the compiler to be such that the object code behaves in
all observable ways exactly like the source code with the exception of
speed and space utilization.
We might want the compiler to be such that the object code ultimately
has the exact same effect on the `store' and produces the same
`answer' as the source code on all input.
We might want the compiler to be such that the object code ultimately
has no different effect on the `store' and produces no different
`answer' as the source code on all valid input.
Non-optimizing compilers tend to be toward the front of the list,
`aggressively optimizing' compilers tend to be toward the end. Some
compilers have `switches' that let you select.
> > Compilers don't have to preserve the non-terminating behavior of code
> > any more than they have to preserve the running time of the code.
>
> Says who?
Says me. But I like to compile my code with aggressive optimizations.
> Someone obviously had too much time on their hands -- time that could
> have better be spent on some nice little flamewar in c.l.s. :)
Glad to see that that I am investing my time wisely, then!
--
~jrm
David Rush
> Joe Marshall <jmar...@alum.mit.edu> writes:
> > Simon Helsen <hel...@informatik.uni-freiburg.de> writes:
> > > On Tue, 11 Apr 2000 ol...@pobox.com wrote:
> > >
> > > >innermost application is evaluated first). This opens up a possibility
> > > >of a "constructive" inconsistency:
> > > >
> > > > (define (bottom) (bottom))
> > > > (define (foo x) 5)
> > > >
> > They shouldn't.
...
> > > An optimizing compiler is not allowed to change the semantics of a
> > > program.
> >
> > An optimizing compiler is not allowed to change the semantics of a
> > *correct* program. It can do what it likes with incorrect ones.
>
> Actually, a compiler, optimizing or not, should reject incorrect
> programs. And indeed, for correct programs it should not change the
> semantics.
>
> As far as I know, the above program is correct Scheme, so a compiler
> that turns the "bottom" loop into something that terminates has
> changed the semantics of a correct program.
>
> > Compilers don't have to preserve the non-terminating behavior of code
> > any more than they have to preserve the running time of the code.
>
> Says who?
To quote my betters, 'Oh boy' ;)
david rush
--
I begin to understand the Balkanization of Scheme...
...and why the rnrs author's list is dead
...
ol...@pobox.com
of an expression/term, which, according to language's semantics, _may_
be reduced to two distinct terms or values. The previous article
gave an example:
(define x 0)
(+ (begin (set! x 2) x) x)
Unfortunately, in addition to mutations and non-termination, hell has
other gates. Consider:
(call-with-current-continuation (lambda (k) (+ (k 1) (k 2))))
This _mutation-free_ term can be reduced to either 1 or 2, as the
order of evaluating function arguments is unspecified. Similar
problem appears in other languages as well:
#include <stdio.h>
static int foo(const int x);
static int add(const int x, const int y);
static int bar(void)
{ try {
return add(foo(1),foo(2)); }
catch(int x)
{
return x; }
}
static int foo(const int x) { throw x; return 0; }
static int add(const int x, const int y) { return x + y; }
int main(void)
{
printf("\nThe result is: %d\n", bar()); return 0;
}
This "pure functional" C++ code, when compiled with egcs-2.91.66 on
i686/Linux and run, prints "2". If you move the implementation of
function add() above the function bar() and compile with an -O4 flag,
the result will be "1". Remove the optimization, and the result is "2"
again. Isn't it wonderful?
I guess the same will apply to Java as well. I'm curious if ML
specifies the result of the term like
1+ (raise 1) + (raise 2) handle x => x;
unambiguously?
To generalize, every language that has a function 'rand', or permits
some kind of indeterminism is inconsistent in the above
sense. Likewise every language that involves interaction with an
external environment is most likely inconsistent, as it is generally
very difficult or impractical to explicitly specify all the external
state (including the possibility of a file system filling up, a hacker
breaking in, or bugs in the kernel).
There appears to be a close relationship between inconsistency
and referential transparency: an ambiguous term is obviously
referentially opaque. On the other hand, a term that has only one
normal form and can be reduced to it is referentially transparent:
every instance of this term in a program can be replaced by the
reduced form without changing program's semantics.
Fergus Henderson
>Simon Helsen <hel...@informatik.uni-freiburg.de> writes:
>
>> On Tue, 11 Apr 2000 ol...@pobox.com wrote:
>>
>> > Scheme uses an applicative-order evaluation (that is, the
>> >innermost application is evaluated first). This opens up a possibility
>> >of a "constructive" inconsistency:
>> >
>> > (define (bottom) (bottom))
>> > (define (foo x) 5)
>> >
>> >Let's consider an expression (foo (bottom)). A smart optimizing
>> >compiler may notice that 'foo' and 'bottom' are pure functions, and
>> >foo does not need the result of its argument. The compiler can
>> >therefore compile "(foo (bottom))" to a value 5.
...
>> But practioners will *expect* the above program not to terminate!
>
>They shouldn't.
That depends on the language. I don't know Scheme well enough to know whether
valid Scheme compilers are allowed to perform such optimizations. If you
intended your comments to apply only to Scheme in particular, and you want us
to believe them, then you should cite some relevent passage from the Scheme
standard (be it an ISO standard or merely some de facto standard) to support
them.
Some languages are not sufficiently well specified for us to even say whether
such optimizations are valid or not.
>> An optimizing compiler is not allowed to change the semantics of a
>> program.
>
>An optimizing compiler is not allowed to change the semantics of a
>*correct* program. It can do what it likes with incorrect ones.
Well, again that depends on the language. For many languages, for many
incorrect programs the compiler is required to report an error message and/or
to reject the program.
In any case, I don't like your terminology. An optimizing compiler
can change the _behaviour_ of the program, but the _semantics_ of
the program should in general be defined by the language specification
(perhaps with some parts of that semantics being implementation-defined,
i.e. determined by the compiler). For programs for which the language
specification does not impose any requirements, the semantics is the universal
set of all possible behaviours.
>> And the semantics of Scheme says that the above program is
>> not terminating. Non-termination is some kind of side-effect in
>> applicative order reduction, hence, you cannot eliminate the
>> argument.
>
>Compilers don't have to preserve the non-terminating behavior of code
>any more than they have to preserve the running time of the code.
This is again dependent on the language. For some languages it is true, for
other languages it is false, and for at least one language (Mercury) the
implementation is required to provide the user with a mode in which it is
false but may also provide alternative modes of operation in which is true.
Note that there are probably some languages, designed for supporting real-time
systems, that do place requirements on the compiler to not worsen the running
time of the code. (I don't know of any off-hand, though. Perhaps someone
reading this can give us an example?)
--
Fergus Henderson <f...@cs.mu.oz.au> | "I have always known that the pursuit
WWW: <http://www.cs.mu.oz.au/~fjh> | of excellence is a lethal habit"
PGP: finger f...@128.250.37.3 | -- the last words of T. S. Garp.
Eijiro Sumii
> ... or actual non-termination, in the case the internet, and
> (hopefully) your operating system and window manager and mobile
> phone networks and nuclear power plant control systems.
Moreover, in some systems such as embedded ones, non-termination is
the only way to termination. I myself have an experience where our
group developed such a system and implemented Scheme on top of it. In
such systems, what happens if a program like below is "optimised" to
(bomb)?
(define (halt) (halt))
(define (bomb) (system "rm -fr /")) ; or whatever bad
(let ([x (halt)]) (bomb))
> Although I guess these are not functional programs and so might be
> outside the scope of this newsgroup.
http://www.erlang.se/erlang/sure/main/applications/
// Eijiro Sumii <su...@saul.cis.upenn.edu>
//
// currently visiting: Department of Computer and Information Science,
// School of Engineering and Applied Science, University of Pennsylvania
Markus Mottl
>> An optimizing compiler is not allowed to change the semantics of a
>> program.
> An optimizing compiler is not allowed to change the semantics of a
> *correct* program. It can do what it likes with incorrect ones.
It seems that you think that non-termination is something "incorrect" - but
this is not necessarily true: there are indeed useful programs that can only
be implemented by using potential (!) non-termination.
E.g. consider the following "map"-function on lazy streams (streams are
either empty or contain integers - but you can't "ask" them whether they
are "empty"; it's rather like "blocking" I/O):
Its type:
map : (int -> int) -> stream -> stream
Its specification ("e" is the empty stream, juxtaposition is like the
"cons"-operation on lists, e.g: "ma" means "m" is prefixed to stream "a";
`m' means that m is a value of the lifted domain of integers (i.e. the
domain has a bottom-element).
(* mapping over the empty stream yields the empty stream *)
[|map|](f)(e) = e
(* if the first element of the stream (an integer expression) can be
evaluated, we apply the function to it (and recurse), otherwise
the stream is empty from there on *)
[|map|](f)(ma) = { e if f(`m') = _|_ (bottom)
{ nb otherwise, where f(`m') = `n', and
{ [|map|](f)(a) = b
A Haskell (or Clean or Miranda) programmer would probably think that
the implementation looked similar to this:
map := rec map. \f. \s. f (hd s) :: map f (tl s)
However, this "straightforward" solution is plain wrong! If you pass a
function "f" that does not need to look at its argument to yield a result,
then it will generate an infinite stream of expressions, even if the input
stream was empty!
E.g.:
map (\x. 42) e
generates the following stream instead of the empty one (try normal order
reduction to verify this):
42 :: 42 :: 42 :: ...
The solution to this problem can only be achieved by "forcing" evaluation of
the first element - if it does not converge, you get the right output
behaviour: namely nothing = the empty stream:
map :=
rec map. \f. \s.
(lazylet h <- hd s in
if h = h then f h else 42) :: map f (tl s)
Here you have "h = h" so considering your argumentation, one could "optimize"
this program and rewrite the "if"-construct to just "f h" - but this would
change semantics in an unwanted way, namely to the previous (wrong)
implementation! The "else"-part is irrelevant, of course - you may put any
type correct (integer) expression into it.
Here a more practical example if you are familiar with Unix-pipes (they are
pretty similar to "streams" as above):
Say, you have a program "all2ones" that reads from stdin and converts each
read byte to "1" and a program "diverge" that prints nothing. If I allowed
your "semantic tricks", writing something like:
diverge | all2ones
will print "ones" although "diverge" did not produce any output! Do you really
want output *filters* on pipes to work this way?
> Compilers don't have to preserve the non-terminating behavior of code
> any more than they have to preserve the running time of the code.
I hope that the above examples clearly show that non-termination might be
required to fill the specification. Note, that there is no way to implement
the map-example correctly without something similar to "h = h"! So if you want
to be sure about the behaviour of your code as an implementor, you'd really
want compilers *not* to "optimize" code parts whose only purpose might be
non-termination (= a side effect). Optimization is only sound if the compiler
has a proof that the termination behaviour will be uneffected.
> `The function BAR cannot correctly produce an answer other than 5.'
It can produce "nothing", which is also a (possibly correct!) answer...
Regards,
Markus Mottl
--
Markus Mottl, mo...@miss.wu-wien.ac.at, http://miss.wu-wien.ac.at/~mottl
L.J. Wischik
>It seems that you think that non-termination is something "incorrect" - but
>this is not necessarily true: there are indeed useful programs that can only
>be implemented by using potential (!) non-termination.
... or actual non-termination, in the case the internet, and (hopefully)
your operating system and window manager and mobile phone networks and
nuclear power plant control systems. Although I guess these are not
functional programs and so might be outside the scope of this newsgroup.
--
Lucian Wischik, Queens' College, Cambridge CB3 9ET. www.wischik.com/lu
Matthias Blume
> To quote my betters, 'Oh boy' ;)
I somehow have the feeling that this instance of "Oh boy" has a
different macro expansion than the previous one. Could you elaborate?
Matthias
Matthias Blume
> Matthias Blume <s...@my.sig> writes:
>
> > As far as "should" and "shouldn't" goes, the language definition
> > _should_ be explicit as to which programs terminate and which don't.
> > The "practitioner" then _should_ rely on the definition.
>
> How could it be? If the language definition were explicit about which
> programs terminate and which don't, wouldn't it require a means to
> decide whether a particular program was terminating or not?
No. The definition does not have to be decidable. In fact, as you
observed, it _cannot_ be decidable for languages that are
Turing-complete (as most programming languages are).
Still, the definition can be given in such a way that _preservation_
of termination (or non-termination) is provable for specific program
transformations.
> > Actually, a compiler, optimizing or not, should reject incorrect
> > programs.
>
> You have to qualify this. Compilers can discriminate between three
> kinds of programs: ones provably correct, ones provably incorrect, and
> ones for which correctness or incorrectness is statically
> undecideable. I *hate* compilers that reject all code not in the
> first category, and even in the case of provably incorrect programs, I
> might want to compile it *anyway* so I can debug parts of the program.
Before we have any misunderstandings, let me say that in this case by
"correct" I mean some notion of correctness that is part of the
language definition. (I.e., it is _not_ the notion of "the program
does what I want it to do".)
For this, the definition should clearly specify a decidable predicate
Correct(P) (for programs P), and if Correct(P), then the language
should assign a unique meaning Meaning(P) to that program.
With this, if Correct(P), then a compiler should accept the program
and produce an "executable" with the same meaning as Meaning(P). If,
on the other hand, Correct(P) does not hold, the compiler should
produce a diagnostic.
*I* hate compilers that do not do this. And I have come to immensely
dislike language definitions that do not provide such a decidable
predicate "Correct" in the first place.
As for whether or not a compiler should actually _refuse_ to compile
incorrect programs, this is a different topic. In a
development/debugging environment, a compiler might still go ahead
(after issuing the mandatory diagnostic) and try to produce an
executable for an "incorrect" program anyway.
> > And indeed, for correct programs it should not change the semantics.
> > As far as I know, the above program is correct Scheme, so a compiler
> > that turns the "bottom" loop into something that terminates has
> > changed the semantics of a correct program.
>
> I think we're arguing about angels and pinheads, so to speak.
>
> We might want the compiler to be such that the object code behaves in
> all observable ways exactly like the source code.
>
> We might want the compiler to be such that the object code behaves in
> all observable ways exactly like the source code with the exception of
> speed and space utilization.
>
> We might want the compiler to be such that the object code ultimately
> has the exact same effect on the `store' and produces the same
> `answer' as the source code on all input.
>
> We might want the compiler to be such that the object code ultimately
> has no different effect on the `store' and produces no different
> `answer' as the source code on all valid input.
No. You are already too specific. Notions like "answer", "store",
and various resource utilization measures pertain to specific
semantics. What I am demanding here is more abstract: I simply want
the language definition to _say_ what these semantic aspects are, and
how valid programs relate to them. Once we have this, I want a
compiler to stick to the definition. Nothing more.
If you want to blur the line between non-terminating and terminating
programs (and have the compiler optimize away provably non-terminating
programs), then I want you to have the language definition specify
precisely for which programs this will happen.
On the other hand, I would find such a so-defined language rather
strange, and the blurring of non-termination aspects rather
questionable. But this is a different issue. (To me, personally, the
difference between "happens soon" and "happens later" is qualitatively
different from the difference between "happens" and "never happens".
But let's not quibble about this further, because _that_ discussion
is, indeed, heading for the "angels and pinheads" category.)
Peter Hancock
> ... or actual non-termination, in the case the internet, and (hopefully)
> your operating system and window manager and mobile phone networks and
> nuclear power plant control systems. Although I guess these are not
> functional programs and so might be outside the scope of this newsgroup.
I think they DO terminate -- over and over again, till the end of
time. What terminates is evaluation of the next I/O command. They
RUN forever just because this evaluation always terminates. And they
can very well (and sometimes are) implemented by functional programs.
The only case I can think of where one does not want evaluation to
terminate is an idle process.
--
Peter Hancock, Edinburgh LFCS
Matthias Blume
> > ... or actual non-termination, in the case the internet, and (hopefully)
> > your operating system and window manager and mobile phone networks and
> > nuclear power plant control systems. Although I guess these are not
> > functional programs and so might be outside the scope of this newsgroup.
>
> I think they DO terminate -- over and over again, till the end of
> time. What terminates is evaluation of the next I/O command. They
> RUN forever just because this evaluation always terminates. And they
> can very well (and sometimes are) implemented by functional programs.
Ok, so you take the outer loop (the one that never terminates) out of
the picture and treat it as some sort of "meta" construct.
Well, if you want to do that, why not go further and do it for all
potentially non-terminating programs? It is actually possible,
because from basic computability theory we know that every computable
function can be expressed as minimization of some primitive recursive
function. In this form (Kleene-NF), the only part of the program that
could potentially lead to non-termination is the outermost
minimization "loop".
(Not that I am seriously suggesting this approach, though. :)
Guy McCusker
> There appears to be a close relationship between inconsistency
> and referential transparency: an ambiguous term is obviously
> referentially opaque.
Why so? It's perfectly possible to add a nondeterministic choice
operator to a pure functional language without breaking any of the
usual equations. You do need to be aware of when and how the
nondeterminism is resolved, though: a call-time-choice (the equivalent
of call-by-value) strategy will break the beta rule for example, but
the same can be said of any kind of side-effect. To recover beta, you
need what I think is called run-time-choice, in which case
(lambda n. n + n) ( 1 or 2) // here "or" is the erratic choice
// operator
can evaluate to 2, 3 or 4 and is equivalent to
(1 or 2) + (1 or 2)
by beta.
Guy.
Nick Williams
Peter Hancock <p...@dcs.ed.ac.uk> wrote:
> > ... or actual non-termination, in the case the internet, and (hopefully)
> > your operating system and window manager and mobile phone networks and
> > nuclear power plant control systems. Although I guess these are not
> > functional programs and so might be outside the scope of this newsgroup.
>I think they DO terminate -- over and over again, till the end of
>time. What terminates is evaluation of the next I/O command. They
>RUN forever just because this evaluation always terminates. And they
>can very well (and sometimes are) implemented by functional programs.
I think it might be fair to say that when the system is desired
to run forever, calling upon the language of axiomatic
semantics, partial correctness is acceptable of the outer-loop,
whereas any inner-loops should be totally correct.
Cheers,
Nick.
--
[ Nick Williams ]
[ MSc Computation Mobile - 07957-138179 ]
[ New College, Oxford http://www.new.ox.ac.uk/~nick/ ]
Joe Marshall
> Let's define inconsistency of a programming language as existence
> of an expression/term, which, according to language's semantics, _may_
> be reduced to two distinct terms or values.
>
> [Examples snipped]
>
> To generalize, every language that has a function 'rand', or permits
> some kind of indeterminism is inconsistent in the above
> sense. Likewise every language that involves interaction with an
> external environment is most likely inconsistent, as it is generally
> very difficult or impractical to explicitly specify all the external
> state (including the possibility of a file system filling up, a hacker
> breaking in, or bugs in the kernel).
I would suggest that your definition of inconsistency could use some
re-working then. It seems reasonable to me that a `rand' procedure (I
hesitate to say function for rand) could exist in a language and
produce different values each time it is called, without bringing the
entire language into doubt.
~jrm
Joe Marshall
> Still, the definition can be given in such a way that _preservation_
> of termination (or non-termination) is provable for specific program
> transformations.
That's where I thought this was going, so I was thinking about this
this morning.
You are making an assertion about program transformations. If a
transformation preserves the termination characteristics of a program,
then you are saying that for any source program S and object program O
under transformation T, that O halts iff S halts.
Now you'll have to help me out with this reasoning here: if the
semantics of a program do not involve taking a fixed-point, then the
program is guaranteed to halt, right? But if the semantics do involve
taking a fixed-point, then halting is undecidable, right?
If I remember correctly, what in particular is undecideable is whether
the fixed point is or is not bottom. If it isn't, you have a program
that halts, if not, it runs forever.
So if your transformation T operates on a program, it must preserve
the identity of the fixed points (to preserve the termination
characteristics). But since the identity of the fixed point is
undecideable, how do you prove that the transformation preserves it?
What I'm questioning is whether you can in fact prove that a
particular transformation preserves the termination characteristics of
all programs it is presented with.
> > > Actually, a compiler, optimizing or not, should reject incorrect
> > > programs.
> >
> > You have to qualify this. Compilers can discriminate between three
> > kinds of programs: ones provably correct, ones provably incorrect, and
> > ones for which correctness or incorrectness is statically
> > undecideable. I *hate* compilers that reject all code not in the
> > first category, and even in the case of provably incorrect programs, I
> > might want to compile it *anyway* so I can debug parts of the program.
>
> Before we have any misunderstandings, let me say that in this case by
> "correct" I mean some notion of correctness that is part of the
> language definition. (I.e., it is _not_ the notion of "the program
> does what I want it to do".)
>
> For this, the definition should clearly specify a decidable predicate
> Correct(P) (for programs P), and if Correct(P), then the language
> should assign a unique meaning Meaning(P) to that program.
>
> With this, if Correct(P), then a compiler should accept the program
> and produce an "executable" with the same meaning as Meaning(P). If,
> on the other hand, Correct(P) does not hold, the compiler should
> produce a diagnostic.
>
> *I* hate compilers that do not do this. And I have come to immensely
> dislike language definitions that do not provide such a decidable
> predicate "Correct" in the first place.
Since I've read some of your posts in the past, I don't want to get
into too much of a flame war here. I don't mind hacking on code where
the Correct(P) is not statically decidable, so I don't want the
compiler to reject programs it can't prove Correct.
> > > And indeed, for correct programs it should not change the semantics.
> > > As far as I know, the above program is correct Scheme, so a compiler
> > > that turns the "bottom" loop into something that terminates has
> > > changed the semantics of a correct program.
> >
> > I think we're arguing about angels and pinheads, so to speak.
> >
> > We might want the compiler to be such that the object code behaves in
> > all observable ways exactly like the source code.
> >
> > We might want the compiler to be such that the object code behaves in
> > all observable ways exactly like the source code with the exception of
> > speed and space utilization.
> >
> > We might want the compiler to be such that the object code ultimately
> > has the exact same effect on the `store' and produces the same
> > `answer' as the source code on all input.
> >
> > We might want the compiler to be such that the object code ultimately
> > has no different effect on the `store' and produces no different
> > `answer' as the source code on all valid input.
>
> No. You are already too specific. Notions like "answer", "store",
> and various resource utilization measures pertain to specific
> semantics. What I am demanding here is more abstract: I simply want
> the language definition to _say_ what these semantic aspects are, and
> how valid programs relate to them. Once we have this, I want a
> compiler to stick to the definition. Nothing more.
I think I want to be this specific, perhaps even more specific. I'm
talking about actual implementations of compilers that transform Lisp
or Scheme code to x86 instructions.
> If you want to blur the line between non-terminating and terminating
> programs (and have the compiler optimize away provably non-terminating
> programs),
No, I don't want the compiler to consider termination (and as I stated
above, I'm not sure that it *can*). I want the compiler to toss out
any function call whose result and mutations are unused.
> then I want you to have the language definition specify
> precisely for which programs this will happen.
I agree with this, but in a slightly different sense: I have the
language definition say what the program returns *if* it does
terminate (and I'm willing to live without defining the `answer' of
non-terminating programs), and I have the language definition say what
`answers' are `used' or not.
Within this definition, which I think is reasonable (and
constructable, incidentally, I'm not sure about adding termination
characteristics and definitions), it is perfectly fine for the
compiler to toss out code that is non-terminating in the case that
result is not used.
--
~jrm
Joe Marshall
> Joe Marshall <jmar...@alum.mit.edu> writes:
> >
> >They shouldn't. [depend on non-termination to be preserved]
>
> That depends on the language. I don't know Scheme well enough to know whether
> valid Scheme compilers are allowed to perform such optimizations. If you
> intended your comments to apply only to Scheme in particular, and you want us
> to believe them, then you should cite some relevent passage from the Scheme
> standard (be it an ISO standard or merely some de facto standard) to support
> them.
>
> Some languages are not sufficiently well specified for us to even say whether
> such optimizations are valid or not.
Good point. I'll think about this one.
> >> An optimizing compiler is not allowed to change the semantics of a
> >> program.
> >
> >An optimizing compiler is not allowed to change the semantics of a
> >*correct* program. It can do what it likes with incorrect ones.
>
> In any case, I don't like your terminology.
The terminology is a little specious. `Incorrect' programs don't
really _have_ semantics, do they?
--
~jrm
Peter Sestoft
> Why so? It's perfectly possible to add a nondeterministic choice
> operator to a pure functional language without breaking any of the
> usual equations. You do need to be aware of when and how the
> nondeterminism is resolved, though: a call-time-choice (the equivalent
> of call-by-value) strategy will break the beta rule for example, but
> the same can be said of any kind of side-effect.
Harald Søndergaard and I attempted to sort out these issues
(e.g. call-time-choice isn't exactly call-by-value) some years back:
@Article{Soendergaard:1990:ReferentialTransparency,
author = "H. S{\o}ndergaard and P. Sestoft",
title = "Referential Transparency, Definiteness and Unfoldability",
journal = "Acta Informatica",
year = "1990",
volume = "27",
pages = "505-517",
note = ""}
Sorry, I've got no electronic copy.
Peter
--
Department of Mathematics and Physics * http://www.dina.kvl.dk/~sestoft/
Royal Veterinary and Agricultural University * Tel +45 3528 2334
Thorvaldsensvej 40, DK-1871 Frederiksberg C, Denmark * Fax +45 3528 2350
Daniel C. Wang
Joe Marshall <jmar...@alum.mit.edu> writes:
{stuff deleted}
> What I'm questioning is whether you can in fact prove that a
> particular transformation preserves the termination characteristics of
> all programs it is presented with.
Consider the simple "identity transform" that takes any programs and returns
it's exactly without modification. This transform preserves the
non-termination of the original program.
This may seem trivial, but it is a demonstration that there exists at least
one "transform" with which you can prove that it preserves the
non-termination of programs. Slightly less trivial transforms also can be
shown to do the same, without having to worry about your fix-point
problems. You need not be skeptical, there are quiet a lot of proofs of this
form, and things "just work".
Nick Williams
Daniel C. Wang <danwan...@cs.princeton.edu> wrote:
>> What I'm questioning is whether you can in fact prove that a
>> particular transformation preserves the termination characteristics of
>> all programs it is presented with.
>Consider the simple "identity transform" that takes any programs and returns
>it's exactly without modification. This transform preserves the
>non-termination of the original program.
From the viewpoint of predicative semantics, isn't any
transformation that is a refinement of an original program
which is totally correct also provably correct also?
i.e.
progA is refined by progB iff
wp(progA, Q) => wp(progB, Q)
Similarly for data refinements with coupling invariants which
are not strict program refinements, but still satisfy:
progA is data-refined by progB iff
(\exists a | CI \and wp(progA, Q)) =>
wp(progC, (\exists a | CI \and Q))
Or am I missing the point here?
Fergus Henderson
>ol...@pobox.com writes:
>
>> There appears to be a close relationship between inconsistency
>> and referential transparency: an ambiguous term is obviously
>> referentially opaque.
>
>Why so? It's perfectly possible to add a nondeterministic choice
>operator to a pure functional language without breaking any of the
>usual equations.
That is true, but I think not in the sense that you mean it.
If you mean that you can add an operator
choose :: t -> t -> t
such that `choose a b' nondeterministically evaluates
to `a' or `b', then it is not true.
It is however possible to add nondeterminism to a pure functional
language and preserve all the usual equations. You just need to make
sure that your nondeterministic choice operator has an appropriate
type, e.g.
choose :: t -> t -> IO t -- `IO t' is the Haskell
-- I/O Monad
There are in fact several different methods for modelling
nondeterminism in pure functional languages; I can give you
some references if you want.
>You do need to be aware of when and how the
>nondeterminism is resolved, though: a call-time-choice (the equivalent
>of call-by-value) strategy will break the beta rule for example, but
>the same can be said of any kind of side-effect. To recover beta, you
>need what I think is called run-time-choice, in which case
>
> (lambda n. n + n) ( 1 or 2) // here "or" is the erratic choice
> // operator
>
>can evaluate to 2, 3 or 4 and is equivalent to
>
> (1 or 2) + (1 or 2)
>
>by beta.
I think that breaks "definiteness" -- the property that
each expression has a definite value -- and thus
destroys the invariant `forall x . x == x'.
See the paper by Sondergaard and Sestoft for details.
Joe Marshall
I've done some more thinking about preservation of termination or
non-termination by the compiler and I had an insight.
If you want the compiler to preserve termination characteristics, all
program transformations must be `applicative order'. If we allow
`normal order' transformations, we will not preserve termination
(i.e., the compiler may output code that terminates with a correct
answer where the interpreter would be non-terminating), but obviously,
for any applicative order program that *does* terminate, a
`normal-order' transformation will produce the same output.
Now I'm certainly willing to live with a compiler that does
normal-order transformations, but someone who expects non-terminating
code to remain non-terminating would obviously have problems with
this. Such a person would require that all transformations would be
done in applicative order.
So I'm going to ask some questions that I think are more interesting
than the one of preserving program termination:
1. What compiler optimizations are disallowed if you restrict the set
of optimizations to those that are applicative order? i.e., which
compiler optimization can you prove correct *without* using
normal-order reduction?
2. What compiler optimizations *require* the use of normal-order
reduction?
3. Finally, are any of the optimizations that *require* the use of
normal-order reduction among the `standard' operations that one
might expect of a simple compiler or an optimizing compiler?
--
~jrm
Joe Marshall
> In comp.lang.functional Joe Marshall <jmar...@alum.mit.edu> wrote:
> >> An optimizing compiler is not allowed to change the semantics of a
> >> program.
>
> > An optimizing compiler is not allowed to change the semantics of a
> > *correct* program. It can do what it likes with incorrect ones.
>
> It seems that you think that non-termination is something "incorrect" - but
> this is not necessarily true: there are indeed useful programs that can only
> be implemented by using potential (!) non-termination.
Unfortunately I'm giving that impression. I'll try to be more careful.
Daniel C. Wang
> I've done some more thinking about preservation of termination or
{stuff deleted}
Amr Sabry. The Formal Relationship between Direct and
Continuation-Passing Style Optimizing Compilers: A Synthesis of Two
Paradigms. Tech. Rep. TR94-241, Dept. of Computer Science, Rice
University, 1994.
http://www.cs.uoregon.edu/~sabry/papers/thesis.ps
Sabry, develops several complete theories of program equivalence for
applicative order langauges.
ol...@pobox.com
term has at most one normal form. Consistency implies referential
transparency: a term can be replaced by an equivalent term (with the
same normal form), without affecting the meaning of the program.
Indeterminism (in the form of a 'rand' procedure, external
interactions (user/network communication), etc) seems to preclude
consistency.
Objections:
- 'rand' is useful and should be allowed. Its indeterminism should not
tarnish the whole language
- "It's perfectly possible to add a nondeterministic choice operator to
a pure functional language without breaking any of the usual
equations. You do need to be aware of when and how the nondeterminism
is resolved"
- "It is however possible to add nondeterminism to a pure functional
language and preserve all the usual equations. You just need to make
sure that your nondeterministic choice operator has an appropriate
type [IO a]"
It appears that all the objections talk about Monads. And they are
right: monad is the way to introduce nondeterminism into a purely
functional language -- without affecting referential transparency. Of
which language, however?
It seems that a Monad implies a separate evaluator, or a second
_stage_ evaluator. A monadic program appears to be executed in two
stages. One, purely functional stage, does a "byte-compilation" so to
speak. It combines (a >>= b) smaller monads into a bigger monad. The
final result is one humongous monad, which gets associated with
main. The second stage then kicks in, and executes the monadic
bytecode in a "single-threaded" way. Ambiguities present in the
original code are resolved in the first stage. Even if the "byte-code"
contains side-effecting operations or throws exceptions, they no
longer matter as the "byte-code" is properly serialized.
I guess this all boils down to the definition of the "normal form".
Consider:
(- (read-int) (read-int))
If I try to reduce it completely, I run into indeterminism. I don't
know whether I subtract the first read number from the second, or the
other way around. This is inconsistency. Let's rewrite this example
into the following:
(bind-sequentially (lambda (x y) (- x y)) (read-int) (read-int))
where bind-sequentially is a function:
(define (bind-sequentially abstraction . args)
(apply abstraction args))
Well, this doesn't give us anything: the reduction of the first
bind-sequentially form runs into an ambiguity: it is not clear which
of the two (read-int) terms should be evaluated first.
Let's do this in stages however. On the first stage, let's assume
(read-int) an irreducible, "atomic" term. We also rewrite
bind-sequentially to do what it says to. Obviously we have to make
it a macro (because it runs on a separate stage)
(define-macro (bind-sequentially abstraction . args)
(let loop ((raw-args args) (cooked-args '()))
(if (null? raw-args)
`(,abstraction ,@(reverse cooked-args))
(let ((cooked-arg (gensym)))
`(let ((,cooked-arg ,(car raw-args)))
,(loop (cdr raw-args)
(cons cooked-arg cooked-args)))))))
Now we try the first stage of reduction. We get a "byte-compiled"
result
(let ((g0 (read-int)))
(let ((g1 (read-int)))
((lambda (x y) (- x y)) g0 g1)))
Note this is the unique normal form of the original expression. If we
apply the second stage of the reduction, with (read-int) now
considered reducible, we surprisingly get the determinate result.
Thus if we do reductions in stages, and introduce sequentializers,
them we can avoid inconsistency.
The same argument applies to a 'rand'-type non-determinism:
(define foo (erratic-or 1 2))
(+ foo foo)
On the first stage, we consider (erratic-or 1 2) to be
atomic. We may still make a beta-reduction
(+ (erratic-or 1 2) (erratic-or 1 2))
On the second stage, we unfreeze erratic-or applications and start
reducing them as well.
Sorry I didn't write this as clear as I wished. I've written a
short essay on monads, and am currently struggling to become satisfied
with it...
Matthias Blume
> If you want the compiler to preserve termination characteristics, all
> program transformations must be `applicative order'. If we allow
> `normal order' transformations, we will not preserve termination
> (i.e., the compiler may output code that terminates with a correct
> answer where the interpreter would be non-terminating), but obviously,
> for any applicative order program that *does* terminate, a
> `normal-order' transformation will produce the same output.
Your "insight" is the well-known fact that beta-reduction is not sound
for call-by-value languages.
You can do what you call "normal-order" reductions (i.e., beta) if you
can prove that they don't change the ordering of effects. If you
count non-termination as an "effect", this includes proving that
non-termination is not being tossed out.
[By the way, after converting a cbv program to, for example, CPS, you
are then free to perform "normal order" reductions as much as you
like.]
> Now I'm certainly willing to live with a compiler that does
> normal-order transformations, but someone who expects non-terminating
> code to remain non-terminating would obviously have problems with
> this. Such a person would require that all transformations would be
> done in applicative order.
>
> So I'm going to ask some questions that I think are more interesting
> than the one of preserving program termination:
>
> 1. What compiler optimizations are disallowed if you restrict the set
> of optimizations to those that are applicative order? i.e., which
> compiler optimization can you prove correct *without* using
> normal-order reduction?
There is a lot of literature on this stuff "out there". For example,
see Appel's "Compiling with Continuations".
> 2. What compiler optimizations *require* the use of normal-order
> reduction?
Not sure. Not even sure the question makes much sense.
> 3. Finally, are any of the optimizations that *require* the use of
> normal-order reduction among the `standard' operations that one
> might expect of a simple compiler or an optimizing compiler?
No.
Matthias Blume
You seem to think that in order to be able to decide "A -> B" it is
somehow necessary to be able to decide "B" (and/or "A"). That is not
so. (For example, I can trivially decide "A -> A" for arbitrary "A".)
> No, I don't want the compiler to consider termination (and as I stated
> above, I'm not sure that it *can*). I want the compiler to toss out
> any function call whose result and mutations are unused.
Why? Wouldn't it be much better if the compiler would tell the programmer:
"Look, I am smart, that's why I was able to prove that the result and
the effects of the following expression are not used by your program:
...
Do you really meant to write it that way?"
In my opinion, this is _much_ more useful than the compiler simply
tossing out something that the programmer wrote. (The programmer
probably wrote it with some purpose in mind. Not all software is
written by the proverbial thousand monkeys playing with the computer
keyboard.)
> > then I want you to have the language definition specify
> > precisely for which programs this will happen.
>
> I agree with this, but in a slightly different sense: I have the
> language definition say what the program returns *if* it does
> terminate (and I'm willing to live without defining the `answer' of
> non-terminating programs), and I have the language definition say what
> `answers' are `used' or not.
Ok, let me give you a little scenario that demonstrates the potential
dangers of using compilers that are "too smart".
Suppose you are writing this super-duper new software product. For
this, you are using the latest in development technology, with a
compiler, that -- of course -- proves as much as it can about a
program, tossing out unused non-terminating expressions left and
right.
You are testing your program on about a gazillion of real-life test
cases, and it works perfectly on each single one. Now you hit the
market, issuing press releases, etc.
Your first customer happens to be NASA, and they put your program into
their new multi-million dollar satellite. You are very confident
about the correctness of your program, so you happily sign the
contract that makes you liable for any failures. (I know, I know,
nobody would _really_ do something like that. I am exaggerating, of
course.)
Unfortunately, the satellite, once in orbit, does not respond to
mission control commands. A gazillion-dollar space shuttle mission
has to be launched to fetch it back and correct the problem. The
problem, as it turns out, is your software.
What happened is this: NASA uses this crummy old processor type
"ANCIENT" that nobody else is using anymore (because it is 15-year
proven hardware technology). Your fancy compiler is unable to produce
code for "ANCIENT", so a different compiler had been used. The other
compiler had been extensively verified to obey the definition of the
programming language you are using. Unfortunately, it does not
implement the "toss out unused expressions" optimization. Result:
Your program hung at startup, because some idiot on your team coded
the startup sequence to make a call to "bottom" where "bottom" was
defined as (define (bottom) (bottom)). You just never noticed it,
because your development system was "too smart for its own good".
Epilogue: NASA, embarrassed by the PR debacle, sues you. The
headlines concerning your company are completely unflattering. The
fortunes of your company go south. A few month later nobody remembers
who you were.
In summary: I think that it is sometimes dangerous to have the
compiler turn non-terminating programs into terminating ones. But
more importantly, it is _always_ unnecessary, because the better
approach is to issue a warning that enables the programmer to
eliminate the offending expression (if that is really the right thing
to do).
Matthias
PS: Before you jump on me with "But they would have tested the program
compiled with the other compiler, ...", let me say: I know. However,
I also know that NASA is not exactly known to be perfect in its
mission preparation, so perhaps your program does not hang on startup
but on encountering some particular input that they just didn't test
beforehand, but which does occur in outer space. (And this despite
the fact that during development you _did_ test that kind of input.)
John Clonts
>
> Joe Marshall <jmar...@alum.mit.edu> writes:
>
> > If you want the compiler to preserve termination characteristics, all
> > program transformations must be `applicative order'. If we allow
> > `normal order' transformations, we will not preserve termination
> > (i.e., the compiler may output code that terminates with a correct
> > answer where the interpreter would be non-terminating), but obviously,
> > for any applicative order program that *does* terminate, a
> > `normal-order' transformation will produce the same output.
>
> Your "insight" is the well-known fact that beta-reduction is not sound
> for call-by-value languages.
>
> You can do what you call "normal-order" reductions (i.e., beta) if you
> can prove that they don't change the ordering of effects. If you
> count non-termination as an "effect", this includes proving that
> non-termination is not being tossed out.
>
> [By the way, after converting a cbv program to, for example, CPS, you
> are then free to perform "normal order" reductions as much as you
> like.]
>
cbv = call by value
CPS = ?
Just skimming here as usual
Thanks,
John
Bruce Hoult
<jcl...@mastnet.net> wrote:
Continuation-Passing Style.
-- Bruce
John Clonts
Ok, thanks.
John
Fergus Henderson
>Let's define inconsistency of a programming language as existence
>of an expression/term, which, according to language's semantics, _may_
>be reduced to two distinct terms or values.
No, let's not. There is already existing terminology for that
property, e.g. "nondeterminacy", as used in the article that Peter
Sestoft just cited. I don't see any need to use the pejorative term
"inconsistent".
Actually there is some imprecision in the existing terminology, which
fails to carefully distinguish between expressions having nondeterministic
values and programs having nondeterministic behaviour (the first is
incompatible with having definiteness and unfoldability, as discussed
in the Sondergaard and Sestoft paper, while the second isn't). So
perhaps agreeing to some more precise terminology would be helpful.
But I don't think using the term "inconsistent" will help.
>This "pure functional" C++ code, when compiled with egcs-2.91.66 on
>i686/Linux and run, prints "2". If you move the implementation of
>function add() above the function bar() and compile with an -O4 flag,
>the result will be "1". Remove the optimization, and the result is "2"
>again. Isn't it wonderful?
>I guess the same will apply to Java as well.
IIRC, Java does specify the order of argument evaluation, so the
directly analogous problem won't occur in Java. However there are
some areas where Java programs have nondeterminstic behaviour, e.g.
when using threads.
Fergus Henderson
>So I'm going to ask some questions that I think are more interesting
>than the one of preserving program termination:
>
>1. What compiler optimizations are disallowed if you restrict the set
> of optimizations to those that are applicative order?
There are quite a few. However, it's hard to say whether they are
important ones. Their importance may depend on programming style.
For the Mercury compiler, the following optimizations are inhibited
by the compilation flag which enforces applicative order:
- Optimizing away calls to functions whose result is not used
- Reordering calls, e.g. for constraint propagation,
for accumulator introduction (for tail recursion),
or for certain kinds of deforestation.
Fergus Henderson
>Joe Marshall <jmar...@alum.mit.edu> writes:
>
>> No, I don't want the compiler to consider termination (and as I stated
>> above, I'm not sure that it *can*). I want the compiler to toss out
>> any function call whose result and mutations are unused.
>
>Why? Wouldn't it be much better if the compiler would tell the programmer:
>
> "Look, I am smart, that's why I was able to prove that the result and
> the effects of the following expression are not used by your program:
> ...
> Do you really meant to write it that way?"
That depends. If the code that the programmer wrote calls
a function and then immediately ignores the result, that is
probably a bug. But if this situation only arises as a result
of inlining and other simplifications that the compiler has
already performed, then generally it does not indicate a bug,
just an optimization opportunity.
The Mercury compiler does such simplifications in two passes.
The first pass occurs early on, before inlining, and if this pass finds
any code that is easily simplifiable, then the compiler issues
a warning. The second pass of simplification occurs after the
various high-level optimization phases such inlining, deforestation,
specialization of higher-order calls, etc., and the compiler does
NOT issue warnings if it discoveres any possible simplifications
in this pass.
>Ok, let me give you a little scenario that demonstrates the potential
>dangers of using compilers that are "too smart".
Certainly there are dangers. Compilers which do perform such optimizations
should have options to turn them off. If you want to write code for which
very high reliability is crucial, e.g. satellite control programs,
then you should disable such optimizations. However, for most
applications efficiency and programmer productivity are also very
important criteria, and so for typical applications the improvements in
efficiency and/or programmer productivity that result from better compiler
optimization are usually worth the small reduction in portability
and reliability.
Elliott Hughes
> IIRC, Java does specify the order of argument evaluation, so the
> directly analogous problem won't occur in Java.
Indeed. Section 15.6.4 of the Java Language Specification states that
argument lists are evaluated left-to-right. In fact, this is the title of the
section in question!
The same is true of binary operators' operands (section 15.6.1).
--
"I still believe in spite of everything that people are really good
at heart" -- Anne Frank
Joe Marshall
> Your "insight" is the well-known fact that beta-reduction is not sound
> for call-by-value languages.
It was a personal insight, not a global one. I don't intend to publish.
> You can do what you call "normal-order" reductions (i.e., beta) if you
> can prove that they don't change the ordering of effects. If you
> count non-termination as an "effect", this includes proving that
> non-termination is not being tossed out.
The point is that non-termination isn't an `effect' in the same sense
that a SET! expression is.
So when a compiler wants to do a beta reduction (assuming the absence
of SET! or SET-CAR! type side effects), you have to decide whether you
want to require the compiler to prove that the values substituted are
*not* _|_. Now it should be obvious that the compiler, in general,
can only produce a conservative guess of whether a particular
expression evaluates to _|_, so you are left with a choice:
A. Only allow beta reductions when the compiler can prove that the
values are not _|_.
B. Allow beta reductions unless the compiler can prove that any
substituted values *are* _|_.
C. Allow beta reductions without regard as to whether any value is
_|_.
Note that *all* of these choices lead to the exact same value in
terminating programs. I believe that the choice between these options
has a greater impact than simply turning a non-terminating applicative
order program into a terminating one, however. For example, dataflow
analysis involves simulating beta-reduction on abstract equivalence
classes of data. If you disallow beta-reduction unless you can prove
that the values are not _|_, you could reduce the opportunities for
optimization.
I think that the choice between these is a matter of taste and
engineering. Choice A is rather conservative, and may prevent certain
optimizations from taking place. Choice B is rather unusual because
it won't maintain non-termination except in trivial cases. It does
place a burden on the compiler to attempt a termination proof. Choice
C allows the compiler a bit more freedom. We know the compiled code
will not produce an `incorrect' answer, but it might produce an answer
where the source code did not.
It seems to me that it would be appropriate to have this under
user control. So I'll amend my initial statement:
Oleg said:
> A smart optimizing compiler ... can therefore compile "(foo
> (bottom))" to a value...
To which Simon Helsen <she...@acm.org> replied:
> But practioners will *expect* the above program not to terminate!
To which I originally said,
> They shouldn't.
But now I'll say, `They shouldn't if they turned the optimizations up
high enough.'
> > So I'm going to ask some questions that I think are more interesting
> > than the one of preserving program termination:
> >
> > 1. What compiler optimizations are disallowed if you restrict the set
> > of optimizations to those that are applicative order? i.e., which
> > compiler optimization can you prove correct *without* using
> > normal-order reduction?
>
> There is a lot of literature on this stuff "out there". For example,
> see Appel's "Compiling with Continuations".
That's a good one, but as a counterpoint, the stuff that Amr Sabry did
at Rice is also good, but quite a bit more `theoretical'.
> > 2. What compiler optimizations *require* the use of normal-order
> > reduction?
>
> Not sure. Not even sure the question makes much sense.
Sure it does. For instance, ((lambda (x) (+ x 3)) 5) can be
immediately optimized into the constant 8, but only if you
beta-reduce (and I'm sure no-one will object to that one). Or
((lambda (a b) b) <expr1> <expr2>) can `optimize' into
(begin <expr1> <expr2>), or if expr1 has no side effects (and terminates,
if you prefer) into simply expr2.
If you disallow beta reductions altogether, what you are left with is
rather unappealing. Alpha reductions don't speed things up much
(unless you count register assignment as an alpha reduction), and eta
reduction doesn't work in typed languages.
> > 3. Finally, are any of the optimizations that *require* the use of
> > normal-order reduction among the `standard' operations that one
> > might expect of a simple compiler or an optimizing compiler?
>
> No.
Not of a simple compiler, but certainly of an `aggressive' compiler, and
perhaps of a `non-aggressive' optimizing compiler.
--
~jrm
Joe Marshall
> You seem to think that in order to be able to decide "A -> B" it is
> somehow necessary to be able to decide "B" (and/or "A"). That is not
> so. (For example, I can trivially decide "A -> A" for arbitrary "A".)
Obviously the trivial example works. But suppose we were
collaborating on a compiler and I came up with some gee-whiz
`optimization' that I could prove works when a program terminates.
I suspect you might challenge me to prove that it preserves the
termination characteristics of the program, i.e., fails to terminate
for all programs that do not terminate.
I don't know that such a proof is possible for *all* interesting
transformations, not just the trivial ones.
> > No, I don't want the compiler to consider termination (and as I stated
> > above, I'm not sure that it *can*). I want the compiler to toss out
> > any function call whose result and mutations are unused.
>
> Why? Wouldn't it be much better if the compiler would tell the programmer:
>
> "Look, I am smart, that's why I was able to prove that the result and
> the effects of the following expression are not used by your program:
> ...
> Do you really meant to write it that way?"
That'd probably be cool, especially if there were an option to shut it
up when the answer is `yes, dammit, no stop complaining and start
compiling'.
> In my opinion, this is _much_ more useful than the compiler simply
> tossing out something that the programmer wrote. (The programmer
> probably wrote it with some purpose in mind. Not all software is
> written by the proverbial thousand monkeys playing with the computer
> keyboard.)
From what I've seen, the bulk of it is. Isn't that why Java was
invented?
> Ok, let me give you a little scenario that demonstrates the potential
> dangers of using compilers that are "too smart".
>
> [disaster elided]
Point taken, let's make optimization a command-line switch, and make
sure that the program runs correctly at all levels.
~jrm
Joe Marshall
> That depends. If the code that the programmer wrote calls
> a function and then immediately ignores the result, that is
> probably a bug. But if this situation only arises as a result
> of inlining and other simplifications that the compiler has
> already performed, then generally it does not indicate a bug,
> just an optimization opportunity.
Macro expansion often results in chunks of dead code and rather
non-optimal constructs, too.
Daniel C. Wang
> that a SET! expression is.
It is. The formal denotational semantics of programming languages makes this
clear. Perhaps, a better question to ask is why do you want to treat
non-termination as special case.
John Prevost
jm> The terminology is a little specious. `Incorrect' programs
jm> don't really _have_ semantics, do they?
Depends what you mean by semantics. For a program in a given
language, if that program is actually an acceptable program, it
certainly has semantics--even if they aren't what the programmer
intended. This is what I usually mean by incorrect.
Invalid programs--that is, programs which are not accepted as part of
the language (syntax error, type error in statically typed languages,
even link error potentially) might have partial semantics which a
smart tool could use to help the programmer solve whatever's wrong.
So I'd say all "incorrect" programs have semantics, and "invalid"
programs might.
John.
Guy McCusker
> >Why so? It's perfectly possible to add a nondeterministic choice
> >operator to a pure functional language without breaking any of the
> >usual equations.
>
> That is true, but I think not in the sense that you mean it.
>
> If you mean that you can add an operator
>
> choose :: t -> t -> t
>
> such that `choose a b' nondeterministically evaluates
> to `a' or `b', then it is not true.
Here's what is true, and what I meant: you can add such a "choose"
operator to a pure functional language (call-by-name/need) and not
violate any of the axioms of a cartesian closed category. That pretty
much only means beta and eta, but that's enough to be going on with.
> I think that breaks "definiteness" -- the property that
> each expression has a definite value -- and thus
> destroys the invariant `forall x . x == x'.
Well, okay, but I suppose what I meant by "breaking equations" was
invalidating equivalences between programs. If you add the choose
operator, it's still true that any program is equivalent to itself.
The problem you raise above is that adding choose falsifies a
(perfectly desirable) predicate in some metalogic of programs. I'm
with you on that.
Cheers,
Guy.
Fergus Henderson
>f...@cs.mu.oz.au (Fergus Henderson) writes:
>
>> >Why so? It's perfectly possible to add a nondeterministic choice
>> >operator to a pure functional language without breaking any of the
>> >usual equations.
>>
>> That is true, but I think not in the sense that you mean it.
>>
>> If you mean that you can add an operator
>>
>> choose :: t -> t -> t
>>
>> such that `choose a b' nondeterministically evaluates
>> to `a' or `b', then it is not true.
>
>Here's what is true, and what I meant: you can add such a "choose"
>operator to a pure functional language (call-by-name/need) and not
>violate any of the axioms of a cartesian closed category. That pretty
>much only means beta and eta, but that's enough to be going on with.
>
>> I think that breaks "definiteness" -- the property that
>> each expression has a definite value -- and thus
>> destroys the invariant `forall x . x == x'.
>
>Well, okay, but I suppose what I meant by "breaking equations" was
>invalidating equivalences between programs. If you add the choose
>operator, it's still true that any program is equivalent to itself.
If you add such a "choose" operator in a way that violates definiteness,
wouldn't that break the equivalence between the following programs?
Program 1: foo x = if x == x then 0 else 1
Program 2: foo x = if x == x then 0 else 42
(Strictly speaking of course we should be talking about program fragments,
not programs.)
Joe Marshall
> Joe Marshall <jmar...@alum.mit.edu> writes:
> {stuff deleted}
> > The point is that non-termination isn't an `effect' in the same sense
> > that a SET! expression is.
>
> It is.
I'm afraid I don't see how they are the same. SET! expressions can be
modeled by operating on the STORE. A non-termination arises because
you are not using normal-order reduction (at least the non-termination
I am talking about; I'm not trying to discuss how to `optimize'
programs that don't have normal forms), it has no effect whatsoever on
the store (unless, of course, the non-terminating program includes
operations on the store).
> The formal denotational semantics of programming languages makes this
> clear.
I guess I'm not sure what you are saying here.
> Perhaps, a better question to ask is why do you want to treat
> non-termination as special case.
Because I don't want to get my compiler involved in termination
proofs (a rather futile exercise, no?).
If I want to aggresively optimize my code, I want the compiler to be
able to do beta-reductions at compile time where it would be
fruitful. There are a few cases where doing such a reduction changes
the behavior of the resulting code:
1. When side effects on the store or the external environment are
involved, and
2. When the language uses applicative-order reduction and there is a
subexpression doesn't normalize under applicative order, but it
does under normal order.
At compile time, we obviously don't know everything about the dynamic
state of the code, so we have to approximate it. Approximating the
first (detecting side effects) is rather simple: there are a set of
known primitives that cause side effects, if you don't use them, you
have purely functional code. So I can quickly determine whether a
subexpression is `functional' or not.
However, if I need to preserve termination, I also have to prove that
the subexpression terminates before I can allow the beta reduction.
This is impossible in all but the very simplest of code.
Now the Church-Rosser theorem states that for any expression that has
a normal form, normal-order evaluation will produce it (other order
evaluation will also produce it, provided it produces anything). So I
know that if I allow beta reduction to go ahead *without* proving that
the program terminates, that *if* it produced an answer before, it
will produce the *same* answer now.
When I'm aggresively optimizing (mind you I want to be aggressive),
this is acceptable. Consider it a performance speedup where I have
made an infinite improvement in the performance.
Consider this code:
(define (foo x)
(let waste-time ((n (abs x)))
(declare (fixnum n))
(if (< n 0)
nil
(waste-time (- n 1))))
22)
It is apparent that the waste-time loop simply wastes time. I want my
optimizing compiler to chuck it out when the optimization setting is
high enough, not to generate code that sits there in a tight loop
decrementing a register.
--
~jrm
Riku Saikkonen
>It appears that all the objections talk about Monads. And they are
>right: monad is the way to introduce nondeterminism into a purely
>functional language -- without affecting referential transparency. Of
>which language, however?
>
>It seems that a Monad implies a separate evaluator, or a second
>_stage_ evaluator. A monadic program appears to be executed in two
>stages. One, purely functional stage, does a "byte-compilation" so to
>speak. It combines (a >>= b) smaller monads into a bigger monad. The
>final result is one humongous monad, which gets associated with
>main.
This is true for the Haskell IO monad, but not, I think, for monads
that the programmer defines (without special support from the
language). Non-determinism doesn't require a primitive monad like IO,
and only the IO monad needs a second "stage of evaluation".
For example, the Haskell list monad can be used for non-deterministic
computation, and the only language support for it is syntactic: if you
forget the nice [...] notation, you can define a similar monad
yourself.
Part of the Haskell list monad:
instance MonadPlus [] where -- "almost" Haskell code
mzero = []
mplus = (++)
(these are the non-deterministic operators FAIL and CHOOSE, or (amb)
and (amb x y) using the notation in SICP)
The definition of mplus doesn't specify in which order its arguments
are evaluated, but it does specify the order in which they appear in
the resulting list; thus the resulting list is "deterministic". For
example, "[1+2] `mplus` [3*4]" in the list monad doesn't specify which
operation is calculated first, but it does specify that the resulting
list of non-deterministic results is always [3,12] and not [12,3].
Thus, a function can do non-deterministic computation internally (in
the list monad) and remain referentially transparent, because the
programmer of the function can specify which of the possible results
is/are returned. As an example, the monadic parsers defined in Hutton
& Meijer's article _Functional Pearls: Monadic Parsing in Haskell_
(Journal of Functional Programming, 1(1), 1993) usually return only
the first possible parse result, by using a special (+++) operator
that works like (++) but returns only the first element of the
resulting list of non-deterministic choices.
--
-=- Rjs -=- r...@lloke.dna.fi
Matthias Blume
> The Mercury compiler does such simplifications in two passes.
> The first pass occurs early on, before inlining, and if this pass finds
> any code that is easily simplifiable, then the compiler issues
> a warning. The second pass of simplification occurs after the
> various high-level optimization phases such inlining, deforestation,
> specialization of higher-order calls, etc., and the compiler does
> NOT issue warnings if it discoveres any possible simplifications
> in this pass.
You don't say whether the Mercury compiler silently makes
"simplifications" that throw away effects or turn non-terminating
programs into terminating ones. If it does, thanks for the warning --
I'll stay away from it then. If it does not, I have no problem
whatsoever with that.
> Certainly there are dangers. Compilers which do perform such optimizations
> should have options to turn them off.
No, such "options" are not really "options" because they changes the
language and not merely the optimization level.
Matthias
--
Matthias Blume <blume@k_u_r_i_m_s.k_y_o_t_o-u.a_c.j_p>
Kyoto University, Research Institute for Mathematical Sciences
(remove those spam-preventing underscores from mail address)
Matthias Blume
> Matthias Blume <s...@my.sig> writes:
>
> > You seem to think that in order to be able to decide "A -> B" it is
> > somehow necessary to be able to decide "B" (and/or "A"). That is not
> > so. (For example, I can trivially decide "A -> A" for arbitrary "A".)
>
> Obviously the trivial example works. But suppose we were
> collaborating on a compiler and I came up with some gee-whiz
> `optimization' that I could prove works when a program terminates.
> I suspect you might challenge me to prove that it preserves the
> termination characteristics of the program, i.e., fails to terminate
> for all programs that do not terminate.
>
> I don't know that such a proof is possible for *all* interesting
> transformations, not just the trivial ones.
If the proof is not possible, then the transformation is not
interesting. By contraposition, all interesting transformation have
such a proof. :)
> > > No, I don't want the compiler to consider termination (and as I stated
> > > above, I'm not sure that it *can*). I want the compiler to toss out
> > > any function call whose result and mutations are unused.
> >
> > Why? Wouldn't it be much better if the compiler would tell the programmer:
> >
> > "Look, I am smart, that's why I was able to prove that the result and
> > the effects of the following expression are not used by your program:
> > ...
> > Do you really meant to write it that way?"
>
> That'd probably be cool, especially if there were an option to shut it
> up when the answer is `yes, dammit, no stop complaining and start
> compiling'.
Ok, perhaps I should have been even more precise. I don't care if the
compiler throws away expressions that it can prove to have all of the
following three properties:
1. have a result that is ignored by the rest of the program
2. have side effects (other than termination) that do not matter
for the program (e.g., no side effects at all)
3. always terminates
If one of these points does not hold, then I _never_ _ever_ want a
compiler to throw away that expression. However, if it is so smart as
to "see" that the expression has properties 1. and 2. but not
necessarily property 3., then I can imagine that I warning diagnostic
would be helpful. If there is a switch to "shut the compiler up",
then in this case I definitely don't want it to silently throw away
that expression.
> > Ok, let me give you a little scenario that demonstrates the potential
> > dangers of using compilers that are "too smart".
> >
> > [disaster elided]
>
> Point taken, let's make optimization a command-line switch, and make
> sure that the program runs correctly at all levels.
Actually, I do not want to have switches for "optimizations" that
alter semantics. (Toggling such a switch effectively changes the
language compiled by the compiler instead of merely changing the
quality of the generated code.)
Matthias
--
Matthias Blume <blume@k_u_r_i_m_s.k_y_o_t_o-u.a_c.j_p>
Kyoto University, Research Institute for Mathematical Sciences
Matthias Blume
Eliminating dead code is perfectly fine. Side-effecting or
non-terminating code that potentially gets executed is not dead,
however.
Matthias
--
Matthias Blume <blume@k_u_r_i_m_s.k_y_o_t_o-u.a_c.j_p>
Kyoto University, Research Institute for Mathematical Sciences
Matthias Blume
> A. Only allow beta reductions when the compiler can prove that the
> values are not _|_.
>
> B. Allow beta reductions unless the compiler can prove that any
> substituted values *are* _|_.
>
> C. Allow beta reductions without regard as to whether any value is
> _|_.
D. Allow beta-reductions "X reduces to Y" whenever the compiler can
prove that "X terminates iff Y terminates".
This is more general than A while still "correct". B and C simply
produce incorrect code under certain circumstances.
> I believe that the choice between these options has a greater impact
> than simply turning a non-terminating applicative order program into
> a terminating one, however. For example, dataflow analysis involves
> simulating beta-reduction on abstract equivalence classes of data.
> If you disallow beta-reduction unless you can prove that the values
> are not _|_, you could reduce the opportunities for optimization.
I don't see what this has to do with dataflow analysis. As you said,
the abstract interpretation is done on abstract values. Those
abstract values serve as conservative estimates of actual runtime
values. Ignoring termination during the analysis is just one of the
(many) reasons why the analysis is not (and cannot be) 100% precise.
> I think that the choice between these is a matter of taste and
> engineering.
To, me, the choice is between having a correct compiler and an incorrect one.
I prefer correct compilers, but opinions may vary... :)
> Choice A is rather conservative, and may prevent certain
> optimizations from taking place. Choice B is rather unusual because
> it won't maintain non-termination except in trivial cases. It does
> place a burden on the compiler to attempt a termination proof. Choice
> C allows the compiler a bit more freedom. We know the compiled code
> will not produce an `incorrect' answer, but it might produce an answer
> where the source code did not.
It may also wipe my harddisk clean when the original source did not.
> Sure it does. For instance, ((lambda (x) (+ x 3)) 5) can be
> immediately optimized into the constant 8, but only if you
> beta-reduce (and I'm sure no-one will object to that one). Or
> ((lambda (a b) b) <expr1> <expr2>) can `optimize' into
> (begin <expr1> <expr2>), or if expr1 has no side effects (and terminates,
> if you prefer) into simply expr2.
Saying "beta reduction is not sound in general" does not mean that
_all_ beta reductions are to be prohibited. In all your examples the
compiler can prove that the beta-step FOR THIS EXPRESSION is sound.
Applicative-order compilers do such things.
> If you disallow beta reductions altogether, what you are left with is
> rather unappealing. Alpha reductions don't speed things up much
> (unless you count register assignment as an alpha reduction), and eta
> reduction doesn't work in typed languages.
Huh?
While general eta reduction is also not sound in applicative-order
languages (again, for termination reasons), most of the time this has
nothing to do with types. Some eta-reductions, however, may be
illegal in polymorphic languages that have the so-called "value
restriction", because it can turn syntactic values into expressions
that are not syntactic values.
Markus Mottl
> From the viewpoint of predicative semantics, isn't any
> transformation that is a refinement of an original program
> which is totally correct also provably correct also?
> progA is refined by progB iff
> wp(progA, Q) => wp(progB, Q)
The problem is that proving that one condition implies another one is
generally undecidable.
That's the funny thing about Hoare-logic: it is itself (relative to
the assertion language) sound and complete. If the program is correct
in terms of the pre- and postconditions, there is a finite derivation
for it. Unfortunately, though the derivation might be correct, you
can't necessarily prove this, because this might require you to prove
the valid application of the consequence-rule - an undecidable problem.
Regards,
Markus Mottl
--
Markus Mottl, mo...@miss.wu-wien.ac.at, http://miss.wu-wien.ac.at/~mottl
Fergus Henderson
>f...@cs.mu.oz.au (Fergus Henderson) writes:
>
>> The Mercury compiler does such simplifications in two passes.
>> The first pass occurs early on, before inlining, and if this pass finds
>> any code that is easily simplifiable, then the compiler issues
>> a warning. The second pass of simplification occurs after the
>> various high-level optimization phases such inlining, deforestation,
>> specialization of higher-order calls, etc., and the compiler does
>> NOT issue warnings if it discoveres any possible simplifications
>> in this pass.
>
>You don't say whether the Mercury compiler silently makes
>"simplifications" that throw away effects or turn non-terminating
>programs into terminating ones.
That depends a bit on exactly what you mean by "terminating program".
The Mercury compiler's optimization options can certainly affect
whether or not a program will terminate, but I would not say that
they turn non-terminating programs into terminating ones.
The Mercury language refererence manual defines two different
operational semantics for Mercury programs. One of them (the "strict
sequential" semantics) in principle specifies a single behaviour
for each program, while the other one (the "commutative" semantics)
is a nondeterminstic semantics that specifies a _set_ of allowable
behaviours; this set always includes the behaviour of the strict
sequential semantics, but sometimes includes other possible behaviours
as well.
Mercury implementations are required to provide a mode in which they
implement the strict sequential semantics, but may also provide
a mode in which they implement the commutative semantics.
It is up to the user (i.e. the programmer) to choose which one they
want.
There are Mercury programs for which the strict sequential semantics
requires the program to terminate, but for which the commutative
semantics includes nontermination as one of the possible behaviours.
So, if the user has selected the commutative semantics, then the
optimization level can affect whether the program terminates.
However, the optimization level does not affect the program's
semantics; it just affects the implementation's choice from the
different possible behaviours that the commutative semantics allows.
>If it does, thanks for the warning -- I'll stay away from it then.
If you want to avoid languages which have nondeterministic semantics,
and for which there are some programs for which both termination and
nontermination are valid behaviours, then you will have to search
fairly hard to find such a language. In particular, be sure to stay
away from Fortran, C, C++, Java, Ada, and OCaml. Mercury should be OK,
so long as you make sure to select the strict sequential semantics.
If you venture to use Haskell, make sure that you steer clear of
dangerous extensions such as ghc's exception-handling and concurrency
support ;-)
>> Certainly there are dangers. Compilers which do perform such optimizations
>> should have options to turn them off.
>
>No, such "options" are not really "options" because they changes the
>language and not merely the optimization level.
For the University of Melbourne Mercury compiler, the compiler options
which affect the operational semantics are indeed listed in a separate
"Language Semantics Options" section of the user guide, rather than
being part of the "Optimization Options" section. The optimization
options do not change the operational semantics, although if the
seleted operational semantics for the given program is nondeterministic,
the optimization options may affect the program's behaviour.
You may argue that the different operational semantics for Mercury
constitute different languages, but I would say that they simply
constitute different semantics for the one language.
This disagreement is just a matter of terminology.
Note that the declarative semantics for Mercury programs
remains the same regardless of which operational semantics
is chosen, and the operational semantics is always required
to be sound with respect to the declarative semantics.
Fergus Henderson
>I don't care if the compiler throws away expressions that it can
>prove to have all of the following three properties:
>
> 1. have a result that is ignored by the rest of the program
> 2. have side effects (other than termination) that do not matter
> for the program (e.g., no side effects at all)
> 3. always terminates
>
>If one of these points does not hold, then I _never_ _ever_ want a
>compiler to throw away that expression.
You are of course entitled to your opinion.
However, many people find concurrent programming useful,
and are not willing to sacrifice concurrent programming
on the altar of Reproducibility. Sometimes you need
nondeterminism.
Daniel C. Wang
Joe Marshall <jmar...@alum.mit.edu> writes:
> "Daniel C. Wang" <danwan...@cs.princeton.edu> writes:
>
> > The formal denotational semantics of programming languages makes this
> > clear.
>
> I guess I'm not sure what you are saying here.
>
> > Perhaps, a better question to ask is why do you want to treat
> > non-termination as special case.
If I write
(+ 1 2)
I'd like my optimizing compiler to optimize it to the constant 3. Maybe
it's a really "smart" compiler and optimizes the answer to something like
the constant 1. Cause it's really a "smart" compiler and knows I really
didn't want general addition but addition of the integers modulo 2, because
it's a "smart" compiler.
I'd like my optimizing compiler to preserver the meaning of the program I
wrote.
If I write the partial function
(define f (lambda (x) (if (< n 2) 1 (diverge))))
(f 3)
I want my optimizing compiler to give me back that same partial function on
the integers. I don't want it to change the semantics of my program into
something I didn't want. If I want normal order evaluation, I know how to
simulate it in an applicative language. I don't want the compiler to give me
something I don't want or something that mucks with the semantics of my
program. It's my program, I wrote it the compiler should treat it nicely and
make it fast, but I would like it to please give me the same program back.
People ship software compiled in debug mode and all the optimizatons turned
off, cause they have enough problems with optimizers that break their
already broken code. I don't need an optimizer breaking code that's not
broken.
Your definiton of side-effect seems to be "anything that effects the store
or does I/O". While this has a nice intuitive feel to it, its kind of
ad-hoc. I prefer the defintion of side-effect as meaning any computation
that prevents me from proving the equality of two lambda terms with the
beta-eta rules. In an applicative order language, this make non-termination
a side-effect. It also makes, call-cc, exceptions, and other non local
control flow operations side-effects, which is a much more general
definition than yours.
If I want normal-order evaluation, I know where an how to get it. I like
applicative-order evaluation cause it easier for me to reason about. I don't
want your optimizer to start screwing up my code and my reasoning by
switching evaluations schemes on me. Its that simple.
Matthias Blume
> If you want to avoid languages which have nondeterministic semantics,
> and for which there are some programs for which both termination and
> nontermination are valid behaviours, then you will have to search
> fairly hard to find such a language. In particular, be sure to stay
> away from Fortran, C, C++, Java, Ada, and OCaml.
I actually do stay away from all of them as much as possible. (It is
possible -- at least for me -- with one exception: there is no way
around the occasional line of C.) The fact that OCaml is in the list
is a real shame, btw.
> Mercury should be OK,
> so long as you make sure to select the strict sequential semantics.
> If you venture to use Haskell, make sure that you steer clear of
> dangerous extensions such as ghc's exception-handling and concurrency
> support ;-)
Actually, if it is with the expressed purpose of supporting
concurrency, it is fine by me.
> For the University of Melbourne Mercury compiler, the compiler options
> which affect the operational semantics are indeed listed in a separate
> "Language Semantics Options" section of the user guide, rather than
> being part of the "Optimization Options" section. The optimization
> options do not change the operational semantics, although if the
> seleted operational semantics for the given program is nondeterministic,
> the optimization options may affect the program's behaviour.
>
> You may argue that the different operational semantics for Mercury
> constitute different languages, but I would say that they simply
> constitute different semantics for the one language.
> This disagreement is just a matter of terminology.
Indeed. In any case, I guess I could live with things if they are as
you describe them.
> and the operational semantics is always required
> to be sound with respect to the declarative semantics.
Of course. Anything less would be terrible.
Matthias
PS: I think I check out of this thread now. But for those who want to
continue: maybe a new Subject: would be a good idea... :)
--
Matthias Blume <blume@k_u_r_i_m_s.k_y_o_t_o-u.a_c.j_p>
Kyoto University, Research Institute for Mathematical Sciences
Guy McCusker
> If you add such a "choose" operator in a way that violates definiteness,
> wouldn't that break the equivalence between the following programs?
>
> Program 1: foo x = if x == x then 0 else 1
>
> Program 2: foo x = if x == x then 0 else 42
>
> (Strictly speaking of course we should be talking about program fragments,
> not programs.)
Yes, bad choice of words on my part again; I apologise. Here's the deal on
"choose":
1) it is not a conservative extension of a pure functional language
(your point); but
2) it does not violate any of the laws of functions (my point).
I got into this because of the assertion that "choose" violates
referential transparency, which is true if you think that referential
transparency means that if
M == N
evaluates to "true" then you can replace M by N everywhere with no
effect on semantics. With this interpretation, "choose" certainly
violates referential transparency.
My reading on referential transparency is that if a variable x gets
bound to M then you can replace x with M everywhere without affecting
the semantics. That is to say, the beta law holds. With this
interpretation, "choose" certainly does not violate referential
transparency.
Guy.
David Rush
"Daniel C. Wang" <danwan...@cs.princeton.edu> writes:
> Your definiton of side-effect seems to be "anything that effects the store
> or does I/O". While this has a nice intuitive feel to it, its kind of
> ad-hoc. I prefer the defintion of side-effect as meaning any computation
> that prevents me from proving the equality of two lambda terms with the
> beta-eta rules. In an applicative order language, this make non-termination
> a side-effect. It also makes, call-cc, exceptions, and other non local
> control flow operations side-effects, which is a much more general
> definition than yours.
I've been using call/cc a little bit in my scheme code, but I recently
made a rather significant change to use a third-party piece of
software that I needed to turn upside-down (making it event-driven
intead of main-loop). I used call/cc to do this, and debugging it
certainly felt like I was suddenly taking a trip back into the world
of global variables. I find it interesting that you consider it a
side-effecting operation, especially since I cold presumably write all
of my code in CPS, making it trivial (TM).
I haven't read Sabry's thesis yet (wlthough I am planning to), but I
would find it helpful if someone could provide a thumbnail description
of why it is considered side-effecting in applicative order. What
changes because of the CPS transform that makes using the kontinuation
parameter *not* a side-effect?
david rush
--
As you can see, I'm not entirely sure what the right questions to ask
are, either...
Joe Marshall
> Joe Marshall <jmar...@alum.mit.edu> writes:
>
> > A. Only allow beta reductions when the compiler can prove that the
> > values are not _|_.
> >
> > B. Allow beta reductions unless the compiler can prove that any
> > substituted values *are* _|_.
> >
> > C. Allow beta reductions without regard as to whether any value is
> > _|_.
>
> D. Allow beta-reductions "X reduces to Y" whenever the compiler can
> prove that "X terminates iff Y terminates".
>
> This is more general than A while still "correct".
Given the expression ((lambda (x) <result>) <expr>), which under
strict semantics is _|_ when <expr> is _|_, you are asking the
compiler to prove that `<result>, where <expr> is substituted for x'
is _|_ whenever <expr> is _|_. This is slightly more general than A,
I guess, but still makes the compiler perform termination proofs.
But in this case, as in A, you would have to prove, that all runtime
paths through the code attempted to evaluate <expr>, even those that
discard the value. I don't think beta reduction will buy you much in
this case.
> B and C simply produce incorrect code under certain circumstances.
You keep saying that.
> > I think that the choice between these is a matter of taste and
> > engineering.
>
> To, me, the choice is between having a correct compiler and an incorrect one.
> I prefer correct compilers, but opinions may vary... :)
`But there was a third option....' I prefer "not incorrect"
compilers. I will give my compiler the freedom to perform reductions
in any order that preserves the ordering of operations on the store
and i/o, and reduces to the same answer. But if there are no i/o or
store manipulations, then it is the case that for any expression, if
*some* order of evaluation terminates with an answer, then *all*
orders of evaluation _that terminate_ produce that *same* answer.
When I specify `high optimization' I want my compiler to produce _that
answer_ as expediently as possible.
> > Choice A is rather conservative, and may prevent certain
> > optimizations from taking place. Choice B is rather unusual because
> > it won't maintain non-termination except in trivial cases. It does
> > place a burden on the compiler to attempt a termination proof. Choice
> > C allows the compiler a bit more freedom. We know the compiled code
> > will not produce an `incorrect' answer, but it might produce an answer
> > where the source code did not.
>
> It may also wipe my harddisk clean when the original source did not.
Er, only if the original code specified that the harddisk should be
wiped, for instance,
(progn (function-that-might-not-terminate)
(wipe-harddisk))
I guess you'd feel comfortable running that in your interpreter, but
uncomfortable running it through the compiler. I'm uncomfortable
typing it my email message, let alone getting it near an evaluator.
Joe Marshall
> Joe Marshall <jmar...@alum.mit.edu> writes:
>
> > "Daniel C. Wang" <danwan...@cs.princeton.edu> writes:
> >
> > > The formal denotational semantics of programming languages makes this
> > > clear.
> >
> > I guess I'm not sure what you are saying here.
> >
> > > Perhaps, a better question to ask is why do you want to treat
> > > non-termination as special case.
>
> If I write
>
> (+ 1 2)
>
> I'd like my optimizing compiler to optimize it to the constant 3. Maybe
> it's a really "smart" compiler and optimizes the answer to something like
> the constant 1. Cause it's really a "smart" compiler and knows I really
> didn't want general addition but addition of the integers modulo 2, because
> it's a "smart" compiler.
That's a straw-man. No reduction of (+ 1 2), under the general
meaning of +, 1, and 2, would produce anything but 3.
I'm not suggesting that an optimizing compiler should *ever* produce
an answer different from the normal form.
> I'd like my optimizing compiler to preserver the meaning of the program I
> wrote.
>
> If I write the partial function
>
> (define f (lambda (x) (if (< n 2) 1 (diverge))))
> (f 3)
>
> I want my optimizing compiler to give me back that same partial function on
> the integers. I don't want it to change the semantics of my program into
> something I didn't want. If I want normal order evaluation, I know how to
> simulate it in an applicative language. I don't want the compiler to give me
> something I don't want or something that mucks with the semantics of my
> program. It's my program, I wrote it the compiler should treat it nicely and
> make it fast, but I would like it to please give me the same program back.
Ok, suppose I define F as such, so that the compiler `knows' that F is
not non-functional (evaluating F will not produce side effects)
(define f (lambda (x) (if (< n 2) 1 (f (+ n 1)))))
and I define G as follows:
(define g (lambda (a b) (* 0 (f a) b)))
You would be upset if the compiler had a rule specifying
"0 * anything" is zero? *I* wouldn't be, and I think a lot of people
would find it reasonable if the compiler compiled G as if it were
written (define g (lambda (a b) 0))
> People ship software compiled in debug mode and all the optimizatons turned
> off, cause they have enough problems with optimizers that break their
> already broken code. I don't need an optimizer breaking code that's not
> broken.
That and the fact that customer bug reports provide no useful
information when the debugging information is not present.
> If I want normal-order evaluation, I know where an how to get it. I like
> applicative-order evaluation cause it easier for me to reason about. I don't
> want your optimizer to start screwing up my code and my reasoning by
> switching evaluations schemes on me. Its that simple.
Fine, don't use optimizations.
--
~jrm
Joe Marshall
> Actually, I do not want to have switches for "optimizations" that
> alter semantics. (Toggling such a switch effectively changes the
> language compiled by the compiler instead of merely changing the
> quality of the generated code.)
Ok, I won't tell you about it.
John Clonts
(I'm tutoring myself in SICP, I don't think I've seen that in there?)
Cheers,
John
Nick Williams
John Clonts <jcl...@mastnet.net> wrote:
>Sorry to interrupt, but what is _|_ ?
_|_ is pronounced 'bottom', and is the greatest lower bound of a
complete lattice.
Cheers,
Nick.
--
[ Nick Williams ]
[ MSc Computation Mobile - 07957-138179 ]
[ New College, Oxford http://www.new.ox.ac.uk/~nick/ ]
Joe Marshall
> Sorry to interrupt, but what is _|_ ?
Not an interruption, it's always good to ask questions.
> (I'm tutoring myself in SICP, I don't think I've seen that in there?)
It's not in SICP.
The symbol I'm writing _|_ is usually printed as an upside down T.
It is called `bottom', and it is often used in describing the formal
semantics of a computer language. (Yes, there is a 'top' and it looks
like a T).
Informally speaking, `bottom' is the `result' of a non-terminating
program, 'top' would be the result of a program that `contradicted
itself', and all the other programs lie in between.
A `strict' language is one in which all the arguments to a function
are evaluated, regardless of whether or not they are needed. A
'non-strict' language is one in which the arguments to a function are
evaluated only if they are needed.
In a strict language, an expression that describes a function call is
equivalent to _|_ if any of its arguments are _|_. In a non-strict
language, this might not be the case.
Here is a program that is (informally) equivalent to bottom:
(define (bottom) (bottom))
You might encounter the expression
((lambda (x) 3) (bottom))
In a strict language, (F _|_) = _|_ for any function F, so the above
expression is equivalent to _|_. An implementation of a strict
language might use `call by value' evaluation. It would get
stuck in an infinite loop trying to evaluate (bottom).
In a non-strict language, we would substitute (bottom) for x before
attempting to reduce (bottom). Then we'd toss it and reduce the
expression to 3 because we don't need x. An implementation of a
non-strict language might use `call by need' evaluation. It would not
attempt to evaluate bottom until it was needed, which in this case it
isn't.
As it turns out, so long as _|_ doesn't show up (and ignoring side
effects), strict and non-strict languages always give you the same
answers for the same problems (this is part of the Church-Rosser
theorem). If an expression evaluates to _|_ in a non-strict language,
then it will evaluate to _|_ in a strict one. The *only* difference
is that there are *some* expressions that evaluate to _|_ in a strict
language that do *not* evaluate to _|_ in a non-strict language.
In the real-world, it turns out that most computer languages are
implemented using applicative order evaluation and are strict. It
seems that non-strict languages are harder to implement efficiently
and harder to understand in the presence of side effects and I/O.
Since you can show that for programs that produce answers the answer
you get by using applicative order evaluation is the same as you would
get from normal-order evaluation, so applicative order is generally
used.
Hope this helps.
~jrm
Daniel C. Wang
David Rush <ku...@bellsouth.net> writes:
{stuff deleted}
> What changes because of the CPS transform that makes using the kontinuation
> parameter *not* a side-effect?
It's not the CPS transform that's the problem, it's the use of call-cc in a
direct (un-cpsed code) that destroys the ability to reason about term
equality in the uncpsed code. Perhaps the best way to think about it is that
after the CPS transform every function takes an extra arguement 'the current
continuation' which is threaded through the evaluation of the program just
like you would thread a state parameter through functional code.
Call-cc and throw basically get and set this state parameter, which isn't
explicit in the direct version. If you've done a CPS transform on your
program call-cc stops becoming a side-effect, because you don't even need it
as a primitive, and you are just programming with higher-order functions.
The same goes with exceptions.
The CPS transform makes many control-effects explicit and they stop becoming
control-effects. Just like you can turn a function that preforms side-effcts
on the store into a purely functional effect free program with explicit
store passing of a functional store.
Daniel C. Wang
> meaning of +, 1, and 2, would produce anything but 3.
So why exactly should we let the compiler muck with the termination
semantics of my program?
> and I define G as follows:
> (define g (lambda (a b) (* 0 (f a) b)))
>
> You would be upset if the compiler had a rule specifying
> "0 * anything" is zero? *I* wouldn't be, and I think a lot of people
> would find it reasonable if the compiler compiled G as if it were
> written (define g (lambda (a b) 0))
Yes... and I think you're wrong about what lots of other people expect.
> Fine, don't use optimizations.
I won't use transformations that destroy the meaning of my program, which I
don't call optimizations.
Daniel Ortmann
...
> To generalize, every language that has a function 'rand', or permits some
> kind of indeterminism is inconsistent in the above sense. Likewise every
> language that involves interaction with an external environment is most
> likely inconsistent, as it is generally very difficult or impractical to
> explicitly specify all the external state (including the possibility of a
> file system filling up, a hacker breaking in, or bugs in the kernel).
> There appears to be a close relationship between inconsistency and
> referential transparency: an ambiguous term is obviously referentially
> opaque. On the other hand, a term that has only one normal form and can be
> reduced to it is referentially transparent: every instance of this term in a
> program can be replaced by the reduced form without changing program's
> semantics.
To which types of program design or program operations might greater rigor be
practically applied?
--
Daniel Ortmann, IBM Circuit Technology, Rochester, MN 55901-7829
ort...@vnet.ibm.com or ort...@us.ibm.com and 507.253.6795 (external)
ort...@rchland.ibm.com and tieline 8.553.6795 (internal)
ort...@isl.net and 507.288.7732 (home)
"The answers are so simple, and we all know where to look,
but it's easier just to avoid the question." -- Kansas
ol...@pobox.com
r...@lloke.dna.fi (Riku Saikkonen) wrote:
> Non-determinism doesn't require a primitive monad like IO,
> and only the IO monad needs a second "stage of evaluation".
Yes, you're very right! I see now that there is indeed another way to
deal with non-determinism.
Let's consider a lambda calculus with integers and corresponding
induction rules.
If we introduce a term 'rand', which indeterministically reduces to 0 or
1, we break a lot of useful properties of the language. For example,
x == x will no longer be a tautology, and
(\x.x==x) rand
can be reduced to either true or false. This non-bottom term does not
have any definite normal form.
However, we can "lift the domain". Instead of integers we can talk about
_sets_ of integers, or "distributions". The latter can be defined by
(distribution/generating) functions: lambda abstractions. We can
easily generalize succ/add etc. induction rules for integers to deal
with sets or distributions. I guess we will end up with something like
interval calculus or fuzzy logic. The best thing is that we regain
determinism: \x.x==x is again a tautology, as, from the point of view
of distribution, rand == rand _is_ true, always.
As you pointed out, this "lifted point of view" can also be expressed
via monads. This seems to indicate that one can view monads either
as staging, or as "lifting of the domain". On one hand we can freeze the
reduction of 'rand' at the first stage; this implies the second stage
to thaw frozen reductions. On the other hand, we can consider 'rand' to
reduce to a set. Because now 'rand' has a different (static or
dynamic) type, rand == 1 is ill-typed. When executing rand == x, an
appropriate operation == should be chosen, which compares sets rather
than numbers. Similarly, using Wadler's famous example:
foo = print "ha"
bar = foo >> foo
main = bar
Taking a staging approach, we freeze 'print' and do other reductions
that still apply. We end up with something like
main = sequentially(print "ha",print "ha").
Then we thaw print and let the output commence. On the other hand, we can
define print:: a -> World -> World. (>>) is then a mere functional
composition. When foo is invoked returning 'print "ha"', nothing is
printed as 'print "ha"' is a function requiring an argument (the
World). This is a regular function that can be manipulated as usual:
the only peculiarity is the type World cannot be mentioned explicitly.
> Thus, a function can do non-deterministic computation internally (in
> the list monad) and remain referentially transparent, because the
> programmer of the function can specify which of the possible results
> is/are returned.
Isn't it what underlies interval arithmetics, fuzzy logic, rough sets?
Sent via Deja.com http://www.deja.com/
Before you buy.
hrum...@cc.hut.fi
> Your definiton of side-effect seems to be "anything that effects the store
> or does I/O". While this has a nice intuitive feel to it, its kind of
> ad-hoc. I prefer the defintion of side-effect as meaning any computation
> that prevents me from proving the equality of two lambda terms with the
> beta-eta rules. In an applicative order language, this make non-termination
> a side-effect. It also makes, call-cc, exceptions, and other non local
> control flow operations side-effects, which is a much more general
> definition than yours.
From a practical point of view, non-termination certainly can have an
observable effect on store and I/O; thus I don't think that you can
ignore non-termination even if you define a side-effect as "anything
that effects the store or does I/O".
Hannu Rummukainen
Peter Hancock
> From a practical point of view, non-termination certainly can have an
> observable effect on store and I/O; thus I don't think that you can
> ignore non-termination even if you define a side-effect as "anything
> that effects the store or does I/O".
Sorry to be dense, but could you help me to understand this? How can
it have an observable effect? Only God can observe nontermination;
sometimes us finite creatures can figure it out by looking at the code,
but that's not an observation.
Do you mean that sometimes we run a program, and everything goes dead,
and we think "uh-oh, it's hung"? That sometimes happens because the
program is going to terminate in 2^128 seconds or sometime after the
heat death of the universe.
Something that bothers me about domain theory is that sometimes people
in it argue by cases on whether the value of an expression is bottom
or otherwise; but bottom is really the absence of a value. There's
something fishy about arguments/definitions by cases on undecidable
propositions.
--
Peter Hancock
hrum...@cc.hut.fi
> Sorry to be dense, but could you help me to understand this? How can
> it have an observable effect? Only God can observe nontermination;
> sometimes us finite creatures can figure it out by looking at the code,
> but that's not an observation.
Well, you got me there :)
Even though you cannot observe nontermination, you can often observe the
lack of it (but as you point out, sometimes lack of termination is
practically indistinguishable from nontermination).
What I was trying to say is that if you optimize away nonterminating
function calls, you can change the observable side effects of a program,
and you don't need a special definition of a side effect to come to this
conclusion.
Hannu Rummukainen
Tim Bradshaw
> Sorry to be dense, but could you help me to understand this? How can
> it have an observable effect? Only God can observe nontermination;
> sometimes us finite creatures can figure it out by looking at the code,
> but that's not an observation.
Although I don't think it would work for this, a common technique in
physics is to conformally transform the coordinate system in such a
way that things out at infinity are brought in to finite distances and
times. This is very useful as it allows you to specify things like
boundary conditions in terms of finite coordinate values. I'm not
sure why it won't work here, but I think it's because of the
discreteness of the space whereas in physics everything is continuous.
--tim
Matthias Blume
> Matthias Blume <s...@my.sig> writes:
>
> > Joe Marshall <jmar...@alum.mit.edu> writes:
> >
> > > A. Only allow beta reductions when the compiler can prove that the
> > > values are not _|_.
> > >
> > > B. Allow beta reductions unless the compiler can prove that any
> > > substituted values *are* _|_.
> > >
> > > C. Allow beta reductions without regard as to whether any value is
> > > _|_.
> >
> > D. Allow beta-reductions "X reduces to Y" whenever the compiler can
> > prove that "X terminates iff Y terminates".
> >
> > This is more general than A while still "correct".
>
> Given the expression ((lambda (x) <result>) <expr>), which under
> strict semantics is _|_ when <expr> is _|_, you are asking the
> compiler to prove that `<result>, where <expr> is substituted for x'
> is _|_ whenever <expr> is _|_. This is slightly more general than A,
> I guess, but still makes the compiler perform termination proofs.
Yes. In general it may not be easier, but in specific cases it can
be. (You have to prove that "<result> terminates _IFF_ <expr>
terminates". This can be a _lot_ easier than proving that "<result>
terminates".)
> > B and C simply produce incorrect code under certain circumstances.
>
> You keep saying that.
I'm glad you noticed.
> > I prefer correct compilers, but opinions may vary... :)
>
> `But there was a third option....' I prefer "not incorrect"
> compilers. I will give my compiler the freedom to perform reductions
> in any order that preserves the ordering of operations on the store
> and i/o, and reduces to the same answer. But if there are no i/o or
> store manipulations, then it is the case that for any expression, if
> *some* order of evaluation terminates with an answer, then *all*
> orders of evaluation _that terminate_ produce that *same* answer.
> When I specify `high optimization' I want my compiler to produce _that
> answer_ as expediently as possible.
No. This is not just "not correct", it is "incorrect". In my opinion,
there is no third option between "correct" and "incorrect" as the
latter is the logical negation of the former. A compiler that turns a
non-terminating program into a terminating one can turn a program that
gives no answer into one that gives a wrong answer. Now, while this
seems to be ok with you, it is not ok with me. A wrong answer is
infinitely worse than no answer, in my opinion.
Matthias
Matthias Blume
> Something that bothers me about domain theory is that sometimes people
> in it argue by cases on whether the value of an expression is bottom
> or otherwise; but bottom is really the absence of a value. There's
> something fishy about arguments/definitions by cases on undecidable
> propositions.
Ok. Most of mathematics is fishy then.
Matthias
Lars Lundgren
> Informally speaking, `bottom' is the `result' of a non-terminating
> program,
I do not like this terminology. I see bottom as a value from wich you can
not extract any information.
> 'top' would be the result of a program that `contradicted
> itself',
Can you please explain what you mean by this?
I thought that bottom was the least element in every domain, and that
most domains does not have a unique top element.
Ex: The Bool domain:
True False
\ /
_|_
Furthermore, thinking informally about logic, and the curry howard
isomorphism, a program that `contradicted itself' sounds more like some
thing absurd ( _|_ ) than something true ( T ). (This usage of
top/bottom is maybe not related)
> and all the other programs lie in between.
>
/Lars L
Russell Wallace
> For this, the definition should clearly specify a decidable predicate
> Correct(P) (for programs P)
Impossible.
Consider a program that calculates values x and y then computes (/ x y),
and a language that specifies it is an error to divide by zero. In
general it is undecidable whether y will be zero, therefore undecidable
whether the program is correct.
(And I agree with the position that an optimizing compiler should make
sure the expression is evaluated correctly *unless* y is zero in which
case it can do pretty much whatever it likes.)
--
"To summarize the summary of the summary: people are a problem."
Russell Wallace
mailto:mano...@iol.ie
Matthias Blume
> Matthias Blume wrote:
> > For this, the definition should clearly specify a decidable predicate
> > Correct(P) (for programs P)
>
> Impossible.
>
> Consider a program that calculates values x and y then computes (/ x y),
> and a language that specifies it is an error to divide by zero. In
> general it is undecidable whether y will be zero, therefore undecidable
> whether the program is correct.
>
> (And I agree with the position that an optimizing compiler should make
> sure the expression is evaluated correctly *unless* y is zero in which
> case it can do pretty much whatever it likes.)
Read again what I wrote. (I even made a remark about this in my
original post because I expected some people to be confused.)
Again: For this discussion, when I say "correct" I do NOT mean "does
what I want it to do"!!! (Perhaps I should have used a different
word, for example "valid" instead of "correct".)
Joe Marshall
> On 14 Apr 2000, Joe Marshall wrote:
>
> > Informally speaking, `bottom' is the `result' of a non-terminating
> > program,
>
> I do not like this terminology. I see bottom as a value from wich you can
> not extract any information.
I was speaking informally.
> > 'top' would be the result of a program that `contradicted
> > itself',
>
> Can you please explain what you mean by this?
Using a less informal terminology, top is a value from which you can
extract too much (overspecified) information.
> I thought that bottom was the least element in every domain, and that
> most domains does not have a unique top element.
>
> Ex: The Bool domain:
>
> True False
> \ /
> _|_
Top is usually added to a domain just like bottom is. You tack it on
to create a unique top element. So the bool domain would be:
_ _
|
/ \
True False
\ /
_|_
As bottom is neither true nor false, top is *both* true and false.
From what I've seen, top is much less interesting than bottom. In the
function domain, when you compute a least fixed point, you might
wonder if it is _|_, but you almost never go in the other direction
(computing a `most' fixed point?) and wonder if you might have top.
--
~jrm
Riku Saikkonen
Yes, though those (at least interval arithmetic) tend to compress the
returned "list of possible values" into continuous areas of values,
and also act on areas: implementations of interval arithmetics don't
look at every possible value one by one (indeed, they can't, if the
domain is not discrete).
I guess the gist of this is that a non-deterministic computation can
be made deterministic by processing a deterministic set (or list or
other structure) of non-deterministic possibilities instead of single
values. Another example of this is the algorithm that translates an
NFA (non-deterministic finite automaton) to a DFA, transforming single
non-deterministic states to deterministic sets of states.
--
-=- Rjs -=- r...@lloke.dna.fi
Diego Dainese
(Fergus Henderson) wrote:
[...]
> There are in fact several different methods for modelling
> nondeterminism in pure functional languages; I can give you
> some references if you want.
>
I'm interested, can you give me them?
Thanks,
--
Diego | To reply remove the `x' and swap the | Sorry for my
Dainese | words around the `@' in the address. | bad English.
Fergus Henderson
>In comp.lang.functional on 12 Apr 2000 17:58:22 GMT f...@cs.mu.oz.au
>(Fergus Henderson) wrote:
>[...]
>> There are in fact several different methods for modelling
>> nondeterminism in pure functional languages; I can give you
>> some references if you want.
>
>I'm interested, can you give me them?
* John Hughes, John O'Donnell, ``Expressing and Reasoning About
Non-deterministic Functional Programs,'' in Proc. of the 1989
Glasgow Workshop on Functional Prog., pp. 308-28.
* F. Warren Burton, ``Nondeterminism with Referential
Transparency in Functional Programming Languages,'' in Computer
Journal, 31(3), 1988, pp. 243-7.
* F. Warren Burton, ``Encapsulating non-determinacy in an
abstract data type with determinate semantics,'' in Journal of
Functional Programming, 1(1), 1991, pp. 3-20.
* P. L. Wadler, ``How to replace failure by a list of successes,''
in Proc. Functional Programming Languages and Computer Architecture,
La Jolla, June 1995, ACM.
--
Fergus Henderson <f...@cs.mu.oz.au> | "I have always known that the pursuit
WWW: <http://www.cs.mu.oz.au/~fjh> | of excellence is a lethal habit"
PGP: finger f...@128.250.37.3 | -- the last words of T. S. Garp.
Lenny Gray
>"Daniel C. Wang" <danwan...@cs.princeton.edu> writes:
>
>> Your definiton of side-effect seems to be "anything that effects the store
>> or does I/O". While this has a nice intuitive feel to it, its kind of
>> ad-hoc. I prefer the defintion of side-effect as meaning any computation
>> that prevents me from proving the equality of two lambda terms with the
>> beta-eta rules. In an applicative order language, this make non-termination
>> a side-effect. It also makes, call-cc, exceptions, and other non local
>> control flow operations side-effects, which is a much more general
>> definition than yours.
>
>From a practical point of view, non-termination certainly can have an
>observable effect on store and I/O; thus I don't think that you can
>ignore non-termination even if you define a side-effect as "anything
>that effects the store or does I/O".
>
>Hannu Rummukainen
From that same practical point of view (probably, though, only one in
which multi-threading is going on), so can _speed_ have an observable
effect on store and I/O. So shall we then disallow optimization?
- Lenny Gray -
Kenneth Mr
> Something that bothers me about domain theory is that sometimes
people
> in it argue by cases on whether the value of an expression is bottom
> or otherwise; but bottom is really the absence of a value. There's
> something fishy about arguments/definitions by cases on undecidable
> propositions.
Bottom is not the absence of a value. It is part of the mathematical
model, it is that the machine evaluating the expression is not
expected to produce the value. It is not undecidable, its just
uncomputable. One has to try to keep separate the idea of the
functions is a pure mathematical sense and their use to compute actual
results. Some people call it denotional and operational semantics (I
think).
The concept doesn't arise much in practical work. It is only if
you are trying to prove properties of your program, eg including
partial and infinite values. For example trying to take n of an
infinite list is ok but trying to take head of reverse of an infinite
list is not ok because reverse is bottom for partial lists.
Duncan Coutts
l...@cc.gatech.edu
> Matthias Blume <s...@my.sig> writes:
>
> >I don't care if the compiler throws away expressions that it can
> >prove to have all of the following three properties:
> >
> > 1. have a result that is ignored by the rest of the program
> > 2. have side effects (other than termination) that do not matter
> > for the program (e.g., no side effects at all)
> > 3. always terminates
> >
> >If one of these points does not hold, then I _never_ _ever_ want a
> >compiler to throw away that expression.
>
> You are of course entitled to your opinion.
>
> However, many people find concurrent programming useful,
> and are not willing to sacrifice concurrent programming
> on the altar of Reproducibility. Sometimes you need
> nondeterminism.
He didn't say he wanted to throw out non-determinism alltogether.
However, it's good to have the nondeterministic parts carefully
labeled and pointed out.
There are two intertwined issues here, IMHO:
1. Termination is an important property of programs. A
non-terminating program is often fatally incorrect.
2. Compilers are best when they are consistent with each other
in important aspects. With consistent compilers, a program
that works under one compiler, will continue to work under
any other.
To briefly repeat the scenario pointed out earlier, it sucks if a
program terminates under compiler A, and then after you leave someone
recompiles it under compiler B, and it stops terminating.
-Lex
Joe Marshall
> To briefly repeat the scenario pointed out earlier, it sucks if a
> program terminates under compiler A, and then after you leave someone
> recompiles it under compiler B, and it stops terminating.
It generally sucks if person B `recompiles' a program and the
program suddenly stops working. But this happens all the time, you
see compiler-specific language extensions, switches that must be
turned on or off for particular platforms, `optimizations' that must
be turned on or off, etc. etc.
I generally avoid writing side-effect-free non-terminating code and
then discarding the value (at least on purpose), so having the
compiler toss it out even if it can't *prove* it terminates is just
fine by me.
I know others disagree.
--
~jrm