bard@gjalp.cs.cornell.edu (Bard Bloom) (09/02/89)
I have seen a folk theorem that it is impossible to define swap(x,y) in Algol, where swap is supposed to be a procedure with two call-by-name integer arguments which exchanges their values. It's not exactly clear what the statement of the theorem should be when (say) x and y have side effects. I've asked around MIT and some at Cornell, and nobody seems to have a reference to the statement or proof. Anyone remember where this came from? Thanks, Bard Bloom
dik@cwi.nl (Dik T. Winter) (09/02/89)
In article <31690@cornell.UUCP> bard@cs.cornell.edu (Bard Bloom) writes: > I have seen a folk theorem that it is impossible to define swap(x,y) in > Algol, where swap is supposed to be a procedure with two call-by-name integer > arguments which exchanges their values. It's not exactly clear what the > statement of the theorem should be when (say) x and y have side effects. > Define: "procedure" swap(x) with:(y); "begin" "integer" z; z:= x; x:= y; y:= z; "end" swap; Perfectly legal, and it works if x and y have no side effects. But if an argument has side effects, there is a problem: "integer" i, j; "integer" "array" x[10], y[10]; "integer" "procedure" indexi; "begin" indexi := i; i := i + 1 "end"; "integer" "procedure" indexj; "begin" indexj := j; j := j + 1 "end:; i := 1; j := 1; swap(x[indexi], y[indexj]); will not swap x[1] and y[1], but y[1] will be stored in x[2] and x[1] will be stored in y[2], and there is no possible rewrite of swap that corrects this. -- dik t. winter, cwi, amsterdam, nederland INTERNET : dik@cwi.nl BITNET/EARN: dik@mcvax
samuel@bifrost.cs.cornell.edu (Samuel M. Weber) (09/03/89)
In article <31690@cornell.UUCP> bard@cs.cornell.edu (Bard Bloom) writes: >I have seen a folk theorem that it is impossible to define swap(x,y) in >Algol, where swap is supposed to be a procedure with two call-by-name integer >arguments which exchanges their values. > >I've asked around MIT and some at Cornell, and nobody seems to have a >reference to the statement or proof. Anyone remember where this came from? On page 428 of the new Dragon book it says "A correctly working version of swap apparently cannot be written if call-by-name is used.", and references Fleck, A. C. "The impossibility of content exchange through the by-name parameter transmission technique." SIGPLAN Notices 11:11 (November 1976) -- Sam Weber samuel@cs.cornell.edu
bard@gjalp.cs.cornell.edu (Bard Bloom) (09/03/89)
In article <8369@boring.cwi.nl> dik@cwi.nl (Dik T. Winter) writes: > [vanilla swap procedure, and example using side effects and arrays] >will not swap x[1] and y[1], but y[1] will be stored in x[2] and >x[1] will be stored in y[2], and there is no possible rewrite of swap >that corrects this. >dik t. winter, cwi, amsterdam, nederland Yes, yes, yes, we all know that, but what is the *proof* that there is no possible rewrite? The informal argument is pretty simple -- to write swap(x,y), you need to reference each of x and y twice, and all kinds of things can happen between the references, and we all know that as well. I'm trying to track down the theorem and its proof. Trying to formalize that "you need to reference..." line is rather hard. The theorem I want says "There is no possible integer swap routine." This presumably requires quantifying over all possible code bodies, somehow. The only proof methods I can think of are: 1) Grind through the operational semantics of Algol. This sounds like a real demon. I haven't a clue about what the right induction hypothesis might be. 2) Conjure up an adequate denotational semantics for Algol in which there is no integer swap routine. Neither one of these sounds elementary. When I've heard the fact stated, it sounded as if it had an elementary proof and not just a plausibility argument. -- Bard
johnl@esegue.segue.boston.ma.us (John R. Levine) (09/03/89)
In article <31736@cornell.UUCP> bard@cs.cornell.edu (Bard Bloom) writes: >In article <8369@boring.cwi.nl> dik@cwi.nl (Dik T. Winter) writes: >> [vanilla swap procedure, and example using side effects and arrays] >>will not swap x[1] and y[1], but y[1] will be stored in x[2] and >>x[1] will be stored in y[2], and there is no possible rewrite of swap >>that corrects this. > >Yes, yes, yes, we all know that, but what is the *proof* that there is no >possible rewrite? ... [discussion of operational and/or denotational >semantics.] Golly, back when I was taking math courses rather than computer wonk stuff, all of our proofs were informal. The idea that long mechanical proofs are even legitimate math has only recently come to be accepted in mathematical circles and is still controversial. (Is there any more reason to believe that a 10,000 line mechanical proof is bug-free than that a 10,000 line program is?) In the case of the Algol 60 swap question, people long ago agreed that there was no way to write a reliable swap, since the two arguments can affect each other in arbitrary ways, the simplest example being swap(i, a[i]). I suspect you could show it's reducible to the halting problem. By the way, A J Perlis once told me that when they defined call by name, they thought that they were coming up with a more elegant refinement of call by reference that avoided the need to define the semantics in terms of the underlying implementation. It wasn't until Jensen's device came along a year or so later that they realized what a can of worms they'd opened. -- John R. Levine, Segue Software, POB 349, Cambridge MA 02238, +1 617 492 3869 {ima|lotus}!esegue!johnl, johnl@ima.isc.com, Levine@YALE.something Massachusetts has 64 licensed drivers who are over 100 years old. -The Globe
bard@gjalp.cs.cornell.edu (Bard Bloom) (09/04/89)
In article <1989Sep3.163014.4697@esegue.segue.boston.ma.us> johnl@esegue.UUCP (John R. Levine) writes: > >Golly, back when I was taking math courses rather than computer wonk stuff, >all of our proofs were informal. The idea that long mechanical proofs are >even legitimate math has only recently come to be accepted in mathematical >circles and is still controversial. I'd be quite happy with a proof in the usual mathematical style. All the proofs quoted so far are more along the lines of the old `proofs' of Euclid's Fifth, the ones which eventually concluded "...which is repugnant to the nature of the straight line." Yes, there's something there, but it's not right yet. >In the case of the Algol 60 swap question, people long ago agreed that there >was no way to write a reliable swap, since the two arguments can affect each >other in arbitrary ways, the simplest example being swap(i, a[i]). I >suspect you could show it's reducible to the halting problem. As usual, this is a persuasive informal argument, but it's not clear how to formalize it in any nice way. This "people long ago agreed" doesn't seem quite up to the usual mathematical standards of proof. BTW, I'd be surprised if it were reducible to the halting problem (depending on what "it" you're talking about) -- just a guess, but I have spent most of my professional life (1) showing that things weren't definable in particular classes of programming languages, and (2) reducing things to the halting problem, especially to do (1). >John R. Levine, Segue Software, POB 349, Cambridge MA 02238, +1 617 492 3869 Bard Bloom, Cornell University.
ok@cs.mu.oz.au (Richard O'Keefe) (09/04/89)
There is a formal proof. I believe it was published in the Algol Bulletin, but it has been about six years since I read it. You might look through the Amsterdam MC (now CWI) reports as well.
hankd@pur-ee.UUCP (Hank Dietz) (09/05/89)
In article <31728@cornell.UUCP> samuel@cs.cornell.edu (Samuel M. Weber) writes: >In article <31690@cornell.UUCP> bard@cs.cornell.edu (Bard Bloom) writes: >>I have seen a folk theorem that it is impossible to define swap(x,y) in >>Algol, where swap is supposed to be a procedure with two call-by-name integer >>arguments which exchanges their values. >> >>I've asked around MIT and some at Cornell, and nobody seems to have a >>reference to the statement or proof. Anyone remember where this came from? > >On page 428 of the new Dragon book it says "A correctly working version >of swap apparently cannot be written if call-by-name is used.", and >references Fleck, A. C. "The impossibility of content exchange through >the by-name parameter transmission technique." SIGPLAN Notices 11:11 >(November 1976) > > -- Sam Weber > samuel@cs.cornell.edu Call by name in Algol is call by thunk: the address of a routine to evaluate the lvalue of each argument is passed. Hence, using the notation of C (but assuming call by thunk): swap(a, b) int a, b; { int *p = &a; /* a's side-effect occurs */ int *q = &b; /* b's side-effect occurs */ int t = *p; *p = *q; *q = t; } Would do a swap invoking side-effects exactly once for each argument (and in a specified order). Call by thunk only prohibits writing a swap function if your language doesn't support an lvalue operator, such as C's "&" address-of. I don't recall if Algol has such an operator or not, but certainly the fact that call by name is used does not prevent it. -hankd@ecn.purdue.edu
SEZ@S67.Prime.COM (09/08/89)
In response to this note: >/* ---------- "swap(x,y) in Algol 60" ---------- */ >I have seen a folk theorem that it is impossible to define swap(x,y) in >Algol, where swap is supposed to be a procedure with two call-by-name integer >arguments which exchanges their values. It's not exactly clear what the >statement of the theorem should be when (say) x and y have side effects. > >I've asked around MIT and some at Cornell, and nobody seems to have a >reference to the statement or proof. Anyone remember where this came from? > >Thanks, > Bard Bloom The easiest example is: swap(a[i], i); The issue is that Algol's call-by-name mechanism would require that if you change the value of "i" then you are referencing a different element of the array "a". Stan Zaborowski ------------------------------------------------------------------------ | The above opinions are mine, mine alone, and no one else's but mine.| |No clear thinking, Right-Wing, Libertarian would ever hold the same | |opinions as anyone else; unless, of course, you would like to make it | |worth my while . . . | ------------------------------------------------------------------------ | I am the NRA. That should make | This space | | you feel better. | for rent | ------------------------------------------------------------------------