Re: [r6rs-discuss] [Formal] Formal semantics should not contain complicating optimizations
Great, agreement. :) For the record, however, I think that there is a much longer way to go before a) the semantics can actually be used to reason about space behavior and b) the editors would accept such a semantics as binding on implementations of Scheme. Thanks again for pointing out the bug in the semantics, btw. Robby On 3/16/07, AndrevanTonder <[EMAIL PROTECTED]> wrote: On Fri, 16 Mar 2007, Robby Findler wrote: > Okay, sure. You've said that several times now. I agree (for the > second time): the semantics cannot be used to reason about space > behavior! > > You also stated that the semantics gets sharing wrong. If all you mean > is the below, then I understand what you mean there is nothing more to > say, as far as I'm concerned. > > But, just in an attempt to be clear to you, I'm claiming that there is > no observable way in which sharing is wrong. Except for the incomplete implementation of EQV? on procedures, which you have said is not technically wrong, but presumably can be observed not to give the correct answer ;-) But okay, I'll drop the space behaviour issue for now, given that it is apparently and unfortunately not a design goal of the editors, after one final remark: You could easily get a semantics with the space and sharing behaviour that is implied by the discussion on procedure location tags and eqv? by a very small modification whereby user procedure parameters are put in the store (as pairs currently are) rather than substituted directly. Scalar values and primitives could still be substituted directly, so the readability of many simple reduction sequences would not be affected. Given that this seems to be a trivial modification, I think an implementation in which this behaviour is provided as an option would be an easy thing to make available. It would be valuable to those of us who are interested in reasoning about space. Andre ___ r6rs-discuss mailing list [email protected] http://lists.r6rs.org/cgi-bin/mailman/listinfo/r6rs-discuss
Re: [r6rs-discuss] [Formal] Formal semantics should not contain complicating optimizations
On Fri, 16 Mar 2007, Robby Findler wrote: Okay, sure. You've said that several times now. I agree (for the second time): the semantics cannot be used to reason about space behavior! You also stated that the semantics gets sharing wrong. If all you mean is the below, then I understand what you mean there is nothing more to say, as far as I'm concerned. But, just in an attempt to be clear to you, I'm claiming that there is no observable way in which sharing is wrong. Except for the incomplete implementation of EQV? on procedures, which you have said is not technically wrong, but presumably can be observed not to give the correct answer ;-) But okay, I'll drop the space behaviour issue for now, given that it is apparently and unfortunately not a design goal of the editors, after one final remark: You could easily get a semantics with the space and sharing behaviour that is implied by the discussion on procedure location tags and eqv? by a very small modification whereby user procedure parameters are put in the store (as pairs currently are) rather than substituted directly. Scalar values and primitives could still be substituted directly, so the readability of many simple reduction sequences would not be affected. Given that this seems to be a trivial modification, I think an implementation in which this behaviour is provided as an option would be an easy thing to make available. It would be valuable to those of us who are interested in reasoning about space. Andre ___ r6rs-discuss mailing list [email protected] http://lists.r6rs.org/cgi-bin/mailman/listinfo/r6rs-discuss
Re: [r6rs-discuss] [Formal] Formal semantics should not contain complicating optimizations
Ah, thanks for pointing that out. Given that those semantics may change, I'll hold off fixing that until I know what the behavior is supposed to be. Robby On 3/16/07, AndrevanTonder <[EMAIL PROTECTED]> wrote: It is where library bodies are said to expand to the equivalent of a letrec* (in the expansion process section). Whatever else may happen in future versions to the specification of libraries/toplevel-programs, I would hope that their consistency with internal definitions be maintained in this regard. The letrec* in question would be (letrec* ((x (set! y 1)) (y y)) y) This is illegal according to the specification of letrec*, which says "One restriction on letrec* is very important: it must be possible to evaluate each without assigning or referring to the value the corresponding or the of any of the bindings that follow it in . If this restriction is violated, an exception with condition type &assertion is raised." Andre On Fri, 16 Mar 2007, Robby Findler wrote: > I went back and re-read the library section, but I can't find where > this is said to be illegal. > > Can you explain yourself a little bit more, please? > > Thanks, > Robby > > On 3/16/07, AndrevanTonder <[EMAIL PROTECTED]> wrote: >> A small issue: I have noticed that 10.9 addresses programs such as >> >>(define x (set! y 1)) >>(define y 2) >> >> This kind of thing is illegal in the current specification. >> >> Andre >> >> >> > > ___ r6rs-discuss mailing list [email protected] http://lists.r6rs.org/cgi-bin/mailman/listinfo/r6rs-discuss
Re: [r6rs-discuss] [Formal] Formal semantics should not contain complicating optimizations
Okay, sure. You've said that several times now. I agree (for the second time): the semantics cannot be used to reason about space behavior! You also stated that the semantics gets sharing wrong. If all you mean is the below, then I understand what you mean there is nothing more to say, as far as I'm concerned. But, just in an attempt to be clear to you, I'm claiming that there is no observable way in which sharing is wrong. In yet more words, there is no program that produces 3 when it should produce 4, due to missed sharing (not that the 3 and 4 are important, except that they are different from each other). Robby On 3/16/07, AndrevanTonder <[EMAIL PROTECTED]> wrote: On Thu, 15 Mar 2007, Robby Findler wrote: > The semantics does correctly model sharing (of values that aren't > procedures -- and the informal semantics does not give a complete > specification of that particular sharing anyways). > > Is it possible you are misunderstanding how it works? Here is an example of what I mean: Consider the following implementation of pairs as closures: (define kons (lambda (x y) (lambda (k) (k x y The formal semantics then expands lists such (kons 1 (kons 2 (kons 3 (kons 4 (kons 5 6) to expressions whose size is linear in the number of elements, as one would expect: (lambda (k) (k 1 (lambda (k) (k 2 (lambda (k) (k 3 (lambda (k) (k 4 (lambda (k) (k 5 6)) If we add the following apparently innocuous assertion to the definition of kons: (define kons (lambda (x y) (lambda (k) (some-test y) (k x y my reading of the informal semantics leads me to believe that the space behaviour will remain linear. It will indeed be linear in all practical Scheme implementations. However, the formal semantics now expands lists such as (kons 1 (kons 2 (kons 3 (kons 4 (kons 5 6) to expressions whose size is nonlinear in the number of elements. Instead of the previous short expression, we now get the following enormous expression: (lambda (k) (some-test (lambda (k) (some-test (lambda (k) (some-test (lambda (k) (some-test (lambda (k) (some-test 6) (k 5 6))) (k 4 (lambda (k) (some-test 6) (k 5 6) (k 3 (lambda (k) (some-test (lambda (k) (some-test 6) (k 5 6))) (k 4 (lambda (k) (some-test 6) (k 5 6))) (k 2 (lambda (k) (some-test (lambda (k) (some-test (lambda (k) (some-test 6) (k 5 6))) (k 4 (lambda (k) (some-test 6) (k 5 6) (k 3 (lambda (k) (some-test (lambda (k) (some-test 6) (k 5 6))) (k 4 (lambda (k) (some-test 6) (k 5 6) (k 1 (lambda (k) (some-test (lambda (k) (some-test (lambda (k) (some-test (lambda (k) (some-test 6) (k 5 6))) (k 4 (lambda (k) (some-test 6) (k 5 6) (k 3 (lambda (k) (some-test (lambda (k) (some-test 6) (k 5 6))) (k 4 (lambda (k) (some-test 6) (k 5 6))) (k 2 (lambda (k) (some-test (lambda (k) (some-test (lambda (k) (some-test 6) (k 5 6))) (k 4 (lambda (k) (some-test 6) (k 5 6) (k 3 (lambda (k) (some-test (lambda (k) (some-test 6) (k 5 6))) (k 4 (lambda (k) (some-test 6) (k 5 6)) In other words, I cannot use the formal semantics to reason about space behaviour. This is a pity, since I would like to use some version of reduction semantics to reason specifically about the space behaviour of promises (see a prior thread about the behaviour of DELAY/FORCE and the need to add a third primitive LAZY to express lazy algorithms that will run in bounded space). Andre ___ r6rs-discuss mailing list [email protected] http://lists.r6rs.org/cgi-bin/mailman/listinfo/r6rs-discuss
Re: [r6rs-discuss] [Formal] Formal semantics should not contain complicating optimizations
On Fri, 16 Mar 2007, AndrevanTonder wrote: (letrec* ((x (set! y 1)) (y y)) y) Correction - that should be (letrec* ((x (set! y 1)) (y 2)) y) It is still illegal. Andre ___ r6rs-discuss mailing list [email protected] http://lists.r6rs.org/cgi-bin/mailman/listinfo/r6rs-discuss
Re: [r6rs-discuss] [Formal] Formal semantics should not contain complicating optimizations
On Thu, 15 Mar 2007, Robby Findler wrote: The semantics does correctly model sharing (of values that aren't procedures -- and the informal semantics does not give a complete specification of that particular sharing anyways). Is it possible you are misunderstanding how it works? Here is an example of what I mean: Consider the following implementation of pairs as closures: (define kons (lambda (x y) (lambda (k) (k x y The formal semantics then expands lists such (kons 1 (kons 2 (kons 3 (kons 4 (kons 5 6) to expressions whose size is linear in the number of elements, as one would expect: (lambda (k) (k 1 (lambda (k) (k 2 (lambda (k) (k 3 (lambda (k) (k 4 (lambda (k) (k 5 6)) If we add the following apparently innocuous assertion to the definition of kons: (define kons (lambda (x y) (lambda (k) (some-test y) (k x y my reading of the informal semantics leads me to believe that the space behaviour will remain linear. It will indeed be linear in all practical Scheme implementations. However, the formal semantics now expands lists such as (kons 1 (kons 2 (kons 3 (kons 4 (kons 5 6) to expressions whose size is nonlinear in the number of elements. Instead of the previous short expression, we now get the following enormous expression: (lambda (k) (some-test (lambda (k) (some-test (lambda (k) (some-test (lambda (k) (some-test (lambda (k) (some-test 6) (k 5 6))) (k 4 (lambda (k) (some-test 6) (k 5 6) (k 3 (lambda (k) (some-test (lambda (k) (some-test 6) (k 5 6))) (k 4 (lambda (k) (some-test 6) (k 5 6))) (k 2 (lambda (k) (some-test (lambda (k) (some-test (lambda (k) (some-test 6) (k 5 6))) (k 4 (lambda (k) (some-test 6) (k 5 6) (k 3 (lambda (k) (some-test (lambda (k) (some-test 6) (k 5 6))) (k 4 (lambda (k) (some-test 6) (k 5 6) (k 1 (lambda (k) (some-test (lambda (k) (some-test (lambda (k) (some-test (lambda (k) (some-test 6) (k 5 6))) (k 4 (lambda (k) (some-test 6) (k 5 6) (k 3 (lambda (k) (some-test (lambda (k) (some-test 6) (k 5 6))) (k 4 (lambda (k) (some-test 6) (k 5 6))) (k 2 (lambda (k) (some-test (lambda (k) (some-test (lambda (k) (some-test 6) (k 5 6))) (k 4 (lambda (k) (some-test 6) (k 5 6) (k 3 (lambda (k) (some-test (lambda (k) (some-test 6) (k 5 6))) (k 4 (lambda (k) (some-test 6) (k 5 6)) In other words, I cannot use the formal semantics to reason about space behaviour. This is a pity, since I would like to use some version of reduction semantics to reason specifically about the space behaviour of promises (see a prior thread about the behaviour of DELAY/FORCE and the need to add a third primitive LAZY to express lazy algorithms that will run in bounded space). Andre ___ r6rs-discuss mailing list [email protected] http://lists.r6rs.org/cgi-bin/mailman/listinfo/r6rs-discuss
Re: [r6rs-discuss] [Formal] Formal semantics should not contain complicating optimizations
It is where library bodies are said to expand to the equivalent of a letrec* (in the expansion process section). Whatever else may happen in future versions to the specification of libraries/toplevel-programs, I would hope that their consistency with internal definitions be maintained in this regard. The letrec* in question would be (letrec* ((x (set! y 1)) (y y)) y) This is illegal according to the specification of letrec*, which says "One restriction on letrec* is very important: it must be possible to evaluate each without assigning or referring to the value the corresponding or the of any of the bindings that follow it in . If this restriction is violated, an exception with condition type &assertion is raised." Andre On Fri, 16 Mar 2007, Robby Findler wrote: I went back and re-read the library section, but I can't find where this is said to be illegal. Can you explain yourself a little bit more, please? Thanks, Robby On 3/16/07, AndrevanTonder <[EMAIL PROTECTED]> wrote: A small issue: I have noticed that 10.9 addresses programs such as (define x (set! y 1)) (define y 2) This kind of thing is illegal in the current specification. Andre ___ r6rs-discuss mailing list [email protected] http://lists.r6rs.org/cgi-bin/mailman/listinfo/r6rs-discuss
Re: [r6rs-discuss] [Formal] Formal semantics should not contain complicating optimizations
I went back and re-read the library section, but I can't find where this is said to be illegal. Can you explain yourself a little bit more, please? Thanks, Robby On 3/16/07, AndrevanTonder <[EMAIL PROTECTED]> wrote: A small issue: I have noticed that 10.9 addresses programs such as (define x (set! y 1)) (define y 2) This kind of thing is illegal in the current specification. Andre ___ r6rs-discuss mailing list [email protected] http://lists.r6rs.org/cgi-bin/mailman/listinfo/r6rs-discuss
Re: [r6rs-discuss] [Formal] Formal semantics should not contain complicating optimizations
A small issue: I have noticed that 10.9 addresses programs such as (define x (set! y 1)) (define y 2) This kind of thing is illegal in the current specification. Andre ___ r6rs-discuss mailing list [email protected] http://lists.r6rs.org/cgi-bin/mailman/listinfo/r6rs-discuss
Re: [r6rs-discuss] [Formal] Formal semantics should not contain complicating optimizations
Jason Orendorff wrote: Thomas Lord wrote: You miss my point. We have overwhelming empirical evidence that in some situations it is useful for string-ref to be O(1) and in other situations for it to be O(n).If an implementation is to be Scheme, is its choice between those to be mandated by the report? If there are two use cases, there should be two APIs. That way, people know what to expect when they use each one. They can write portable programs. They can even handle when both kinds of situations arise in the same program. ...Or was this a metaphor for something else? I guess I'm missing your point too. -j How about an analogy, then? And then I'll apply it. The analogy is to, say, the handling of local bindings in a classic lisp -- the choice between shallow and deep binding. They have very different performance characteristics, at least if implemented using simple techniques. One may be a fantastic choice for a dinky little lisp designed to run in an embedded system, the other a fantastic choice for an optimizing compiler. (Don't mistake this for a comprehensive account of the trade-offs between shallow and deep binding but, hopefully you take my point or can google around to get the gist of it.) Now, one lisp dialect can admit both techniques. And the author of a portable library can write for that dialect, rather than for either kind of implementation, and their code can be useful in both. So, applying the analogy: It is useful to have a semantic definition for the dialect that is agnostic about the performance characteristics of various operations. It can be useful to write code against that dialect. -t ___ r6rs-discuss mailing list [email protected] http://lists.r6rs.org/cgi-bin/mailman/listinfo/r6rs-discuss
Re: [r6rs-discuss] [Formal] Formal semantics should not contain complicating optimizations
Thomas Lord wrote: You miss my point. We have overwhelming empirical evidence that in some situations it is useful for string-ref to be O(1) and in other situations for it to be O(n).If an implementation is to be Scheme, is its choice between those to be mandated by the report? If there are two use cases, there should be two APIs. That way, people know what to expect when they use each one. They can write portable programs. They can even handle when both kinds of situations arise in the same program. ...Or was this a metaphor for something else? I guess I'm missing your point too. -j ___ r6rs-discuss mailing list [email protected] http://lists.r6rs.org/cgi-bin/mailman/listinfo/r6rs-discuss
Re: [r6rs-discuss] [Formal] Formal semantics should not contain complicating optimizations
John Cowan wrote: BTW, it occurred to me that a representation-switching implementation of strings can switch representations atomically provided the pointer to the code units (8-bit, 16-bit, or 32-bit) contains some tag bits indicating which one it is. When a string mutator detects that it needs to convert the representation, it builds up a new representation in freshly allocated memory, constructs the specially tagged pointer to it, and atomically swaps in the new pointer for the old. No locks. Meanwhile, another thread has picked up the old pointer, added an index and is about to mutate now-stale memory just after you've swapped pointers. The difficulty in implementing that kind of string isn't limited to threaded systems, either. You can easily wind up with stale pointers to the previous string rep lots of ways. It's not *that* hard, I think, to do it well, though. String rep changes shouldn't happen all that often (and you can take simple steps to make sure that's the case). So, for example, you can reasonably trade off locking granularity (latency on rep changes) for overall speed. There's other tricks that can help, too, but we've prbly handed out enough rope (cough, cough) for people string themselves up, already. (hint, hint) In some sense, coming to grips with the extra code all this takes is, if done well, also a way to come to grips with how memory hierarchies really work. -t ___ r6rs-discuss mailing list [email protected] http://lists.r6rs.org/cgi-bin/mailman/listinfo/r6rs-discuss
Re: [r6rs-discuss] [Formal] Formal semantics should not contain complicating optimizations
From: John Cowan <[EMAIL PROTECTED]> Subject: Re: [r6rs-discuss] [Formal] Formal semantics should not contain complicating optimizations Date: Thu, 15 Mar 2007 22:32:51 -0400 > Thomas Lord scripsit: > > > You miss my point. We have overwhelming empirical evidence > > that in some situations it is useful for string-ref to be O(1) and > > in other situations for it to be O(n).If an implementation is > > to be Scheme, is its choice between those to be mandated by the > > report? > > No, it is not to be mandated by the report, and it isn't. > > BTW, it occurred to me that a representation-switching implementation > of strings can switch representations atomically provided the > pointer to the code units (8-bit, 16-bit, or 32-bit) contains > some tag bits indicating which one it is. When a string mutator > detects that it needs to convert the representation, it builds up > a new representation in freshly allocated memory, constructs the > specially tagged pointer to it, and atomically swaps in the new > pointer for the old. No locks. That's similar to what Gauche does for its utf-8 string. A Scheme string is merely a type tag and a pointer to a "string body". Mutation causes allocation of a "string body" and swapping the pointer atomically. --shiro ___ r6rs-discuss mailing list [email protected] http://lists.r6rs.org/cgi-bin/mailman/listinfo/r6rs-discuss
Re: [r6rs-discuss] [Formal] Formal semantics should not contain complicating optimizations
Thomas Lord scripsit: > You miss my point. We have overwhelming empirical evidence > that in some situations it is useful for string-ref to be O(1) and > in other situations for it to be O(n).If an implementation is > to be Scheme, is its choice between those to be mandated by the > report? No, it is not to be mandated by the report, and it isn't. BTW, it occurred to me that a representation-switching implementation of strings can switch representations atomically provided the pointer to the code units (8-bit, 16-bit, or 32-bit) contains some tag bits indicating which one it is. When a string mutator detects that it needs to convert the representation, it builds up a new representation in freshly allocated memory, constructs the specially tagged pointer to it, and atomically swaps in the new pointer for the old. No locks. -- Mark Twain on Cecil Rhodes:John Cowan I admire him, I freely admit it, http://www.ccil.org/~cowan and when his time comes I shall[EMAIL PROTECTED] buy a piece of the rope for a keepsake. ___ r6rs-discuss mailing list [email protected] http://lists.r6rs.org/cgi-bin/mailman/listinfo/r6rs-discuss
Re: [r6rs-discuss] [Formal] Formal semantics should not contain complicating optimizations
Mikael Tillenius wrote: Thomas Lord wrote: Yes. And, in practice, it is useful to implement them in different ways and, at the same time, by which metrics we mean "efficient" varies from situation to situation. Yes. What I meant was that the specification in 5.92 is hard to implement efficiently (e.g. string-ref is O(1)) if you want to store the strings internally as utf8 or utf16. Some people want to do that. Therefore (among other things) the current specification is controversial. Oh, well... my formal comment (submitted last night) would fix that. The changes it advocates, alas, require more work than is present in the proposal but hopefully it is enough to spark some interest in the direction. -t Firm up what *you* mean by "reasonable", give that thing a more reasonable name than "reasonable", and refer to that. Sorry but I'm vague on purpose here. But to give you some examples: It is reasonable if things like string-ref, vector-ref is O(1) in time. Its reasonable if a string with n characters use O(n) bytes. It is not reasonable for string-ref and vector-ref to take O(n) time. It's not reasonable for a string with n characters to use O(n^2) bytes of memory. Another way to define what I mean by reasonable is to say that every Scheme implementation I know about is reasonable. Ok, were getting off topic here. To sum things up I think is is useful to be able to assume certain things about time and memory consumption in a programming language. Maybe it does not belong in the language specification. /Mikael ___ r6rs-discuss mailing list [email protected] http://lists.r6rs.org/cgi-bin/mailman/listinfo/r6rs-discuss
Re: [r6rs-discuss] [Formal] Formal semantics should not contain complicating optimizations
Thomas Lord wrote: Yes. And, in practice, it is useful to implement them in different ways and, at the same time, by which metrics we mean "efficient" varies from situation to situation. Yes. What I meant was that the specification in 5.92 is hard to implement efficiently (e.g. string-ref is O(1)) if you want to store the strings internally as utf8 or utf16. Some people want to do that. Therefore (among other things) the current specification is controversial. Firm up what *you* mean by "reasonable", give that thing a more reasonable name than "reasonable", and refer to that. Sorry but I'm vague on purpose here. But to give you some examples: It is reasonable if things like string-ref, vector-ref is O(1) in time. Its reasonable if a string with n characters use O(n) bytes. It is not reasonable for string-ref and vector-ref to take O(n) time. It's not reasonable for a string with n characters to use O(n^2) bytes of memory. Another way to define what I mean by reasonable is to say that every Scheme implementation I know about is reasonable. Ok, were getting off topic here. To sum things up I think is is useful to be able to assume certain things about time and memory consumption in a programming language. Maybe it does not belong in the language specification. /Mikael ___ r6rs-discuss mailing list [email protected] http://lists.r6rs.org/cgi-bin/mailman/listinfo/r6rs-discuss
Re: [r6rs-discuss] [Formal] Formal semantics should not contain complicating optimizations
Mikael Tillenius wrote: Thomas Lord wrote: How would you reconcile your category of "reasonable implementation" with all of the complexity-varying, all useful approaches to implementing string-ref that people talk about? Isn't this part of why strings is so controversial. Different people want to implement them in different ways and at the same time be able to access parts of them in a efficient way. Yes. And, in practice, it is useful to implement them in different ways and, at the same time, by which metrics we mean "efficient" varies from situation to situation. Yes, some of that language probably needs cleaned-up, with particular attention to the "must v. should" distinction. My gosh, if we were to get to that point before the end of this year, in my view, it'll probably be evidence that R6 is shaping up nicely. It would make it harder to use Scheme as a way to talk about algorithms and their efficiency if we cannot do some basic assumptions about the underlying Scheme implementation. Of course one could always say things like: "On a reasonable implementation this algorithm would be O(n)". Firm up what *you* mean by "reasonable", give that thing a more reasonable name than "reasonable", and refer to that. -t ___ r6rs-discuss mailing list [email protected] http://lists.r6rs.org/cgi-bin/mailman/listinfo/r6rs-discuss
Re: [r6rs-discuss] [Formal] Formal semantics should not contain complicating optimizations
On 3/15/07, AndrevanTonder <[EMAIL PROTECTED]> wrote: On Thu, 15 Mar 2007, Robby Findler wrote: > The formal semantics makes no claim to let you reason about the space > behavior of your program! But the body of the document does make some solid guarantees on space, and further allows one to infer behaviour w.r.t. copying and sharing of lambda parameters. Shouldn't one of the the purposes of an operational (as opposed to denotational) semantics be precisely to formalize this kind of reasoning? The semantics does correctly model sharing (of values that aren't procedures -- and the informal semantics does not give a complete specification of that particular sharing anyways). Is it possible you are misunderstanding how it works? For example, this is modeled correctly: ((lambda (c) ((lambda (x y) (set-car! x 3) (car y)) c c)) (cons 1 2)) It produces 3, as you probably expect. You can try it out. Download the semantics and edit the "show-examples.scm" file! Insofar as it does not, I would consider it incorrect. That is not the usual meaning of the word "incorrect". Perhaps "incomplete" or "not what I wanted". :) But thanks for clarifying. I'm going to assume that the earlier uses of "incorrect" were in this sense. I hope that's okay. I have only seriously needed an operational semantics a few times, all of which involved reasoning about space behaviour. An operational semantics that does the unnecessary copying of the current specification would have been no use to me in any of these cases. Okay. I see the value of the operational semantics in r6, as compared to the denotational in r5 as: - it covers a larger part of the language - it comes with a stepper to promote experimentation - it has simpler mathematical underpinnings (making is accessible to a wider audience) My dream is that every Scheme programmer can use the semantics that comes with r6 to play around with parts of the language to see how things work. I don't mean to discredit the denotational semantics in r5 or denotational semantics in general. I do, however, believe that this operational semantics is a good fit for the Scheme report. Robby ___ r6rs-discuss mailing list [email protected] http://lists.r6rs.org/cgi-bin/mailman/listinfo/r6rs-discuss
Re: [r6rs-discuss] [Formal] Formal semantics should not contain complicating optimizations
Thomas Lord wrote: How would you reconcile your category of "reasonable implementation" with all of the complexity-varying, all useful approaches to implementing string-ref that people talk about? Isn't this part of why strings is so controversial. Different people want to implement them in different ways and at the same time be able to access parts of them in a efficient way. Yes, some of that language probably needs cleaned-up, with particular attention to the "must v. should" distinction. My gosh, if we were to get to that point before the end of this year, in my view, it'll probably be evidence that R6 is shaping up nicely. It would make it harder to use Scheme as a way to talk about algorithms and their efficiency if we cannot do some basic assumptions about the underlying Scheme implementation. Of course one could always say things like: "On a reasonable implementation this algorithm would be O(n)". It may be handy to think about observables. In some sense, the meaning of a program is how it modulates its output ports and responds to modulations of its input ports.There are some temporal constraints that relate those but mostly in the sense of modeling causality, not performance. It's useful to talk about atemporal mathematical objects that relate those modulations and that's the level of description I'd expect from a formal semantics. Formal operational models, of which it appears their can be many useful ones with critical differences among them, are interesting when we can see that they in fact satisfy the formal semantic constraints. It is also interesting to watch how the user alters the semantics of a program by terminating it prematurely when it fails to respond to user interaction. /Mikael ___ r6rs-discuss mailing list [email protected] http://lists.r6rs.org/cgi-bin/mailman/listinfo/r6rs-discuss
Re: [r6rs-discuss] [Formal] Formal semantics should not contain complicating optimizations
On Thu, 15 Mar 2007, Robby Findler wrote: The formal semantics makes no claim to let you reason about the space behavior of your program! But the body of the document does make some solid guarantees on space, and further allows one to infer behaviour w.r.t. copying and sharing of lambda parameters. Shouldn't one of the the purposes of an operational (as opposed to denotational) semantics be precisely to formalize this kind of reasoning? Insofar as it does not, I would consider it incorrect. I have only seriously needed an operational semantics a few times, all of which involved reasoning about space behaviour. An operational semantics that does the unnecessary copying of the current specification would have been no use to me in any of these cases. Andre ___ r6rs-discuss mailing list [email protected] http://lists.r6rs.org/cgi-bin/mailman/listinfo/r6rs-discuss
Re: [r6rs-discuss] [Formal] Formal semantics should not contain complicating optimizations
Alexander Kjeldaas wrote: On 3/15/07, Thomas Lord <[EMAIL PROTECTED]> wrote: Mikael Tillenius wrote: > Thomas Lord wrote: >> AndrevanTonder wrote: >>> I would like to be able to reason about the space behaviour of a >>> program using the formal semantics. >> >> Please, no. That would mean that an implementation which did >> not exhibit the space behavior you predict that way is not conforming. >> It sounds to me like you want a mathematical model of space >> behavior *of some particular implementations* (and, you'd want >> a proof that that model is consistent with the formal semantics). >> >> The formal semantics should describe, as far as practical, the >> constraints that apply to all implementations -- but nothing >> more. > Please yes! ;-) > > If space and time behaviour cannot be entirely ignored in real world > programming. While it is impossible to describe these in terms of > seconds and bytes a programmer must be able to know whether an > algorithm is O(1), O(n) or O(2^n) in terms of both space and time and > this must be the same on all reasonable implementations. How would you reconcile your category of "reasonable implementation" with all of the complexity-varying, all useful approaches to implementing string-ref that people talk about? What if scheme had immutable strings? Henry Baker sais this about functional strings in "Equal Rights for Functional Objects or, The More Things Change, The More They Are the Same" (which btw includes some really good arguments in favor of immutable objects) http://home.pipeline.com/~hbaker1/ObjectIdentity.html : "Functional strings can have interesting implementations. A representation of a string as a tree whose leaves are individual characters offers O(1) complexity concatenation; while element indexing is more expensive, it is usually less common than concatenation." Alexander You miss my point. We have overwhelming empirical evidence that in some situations it is useful for string-ref to be O(1) and in other situations for it to be O(n).If an implementation is to be Scheme, is its choice between those to be mandated by the report? -t ___ r6rs-discuss mailing list [email protected] http://lists.r6rs.org/cgi-bin/mailman/listinfo/r6rs-discuss
Re: [r6rs-discuss] [Formal] Formal semantics should not contain complicating optimizations
On 3/15/07, David Van Horn <[EMAIL PROTECTED]> wrote: Robby Findler wrote: > The formal semantics makes no claim to let you reason about the space > behavior of your program! > > You've said twice now that you think the formal semantics is > incorrect. Your explanations of why don't seem right to me, but they > are still vague. Please explain (unless you were talking about space > both times?) The specification of eqv? (9.6) requires: (let ((p (lambda (x) x))) (eqv? x x)) ===> #t But the substitution model and the eqv? rule in the formal semantics: P[(eqv? uproc uproc)] ---> unknown Seems to imply: (let ((p (lambda (x) x))) (eqv? x x)) ===> unknown The formal semantics is missing the location tags as described in 9.5.2, unless I am missing something (not unlikely). You got it right. But "unknown" is the formal semantics way of saying "I don't cover that". That particular example wouldn't be difficult, tho. The reason it got dropped from the semantics is that it seems quite difficult (and without much value, relative to the difficulty) to cover when eqv? is allowed to return #f. Jacob and I did cover that in the r5 semantics, which appeared at the Scheme workshop. We're also working on a followup version of the r5 semantics that explains this in more detail. I hope you won't mind if I'll refer you to that (forthcoming) paper, for now. Robby ___ r6rs-discuss mailing list [email protected] http://lists.r6rs.org/cgi-bin/mailman/listinfo/r6rs-discuss
Re: [r6rs-discuss] [Formal] Formal semantics should not contain complicating optimizations
On 3/15/07, Thomas Lord <[EMAIL PROTECTED]> wrote: Mikael Tillenius wrote: > Thomas Lord wrote: >> AndrevanTonder wrote: >>> I would like to be able to reason about the space behaviour of a >>> program using the formal semantics. >> >> Please, no. That would mean that an implementation which did >> not exhibit the space behavior you predict that way is not conforming. >> It sounds to me like you want a mathematical model of space >> behavior *of some particular implementations* (and, you'd want >> a proof that that model is consistent with the formal semantics). >> >> The formal semantics should describe, as far as practical, the >> constraints that apply to all implementations -- but nothing >> more. > Please yes! ;-) > > If space and time behaviour cannot be entirely ignored in real world > programming. While it is impossible to describe these in terms of > seconds and bytes a programmer must be able to know whether an > algorithm is O(1), O(n) or O(2^n) in terms of both space and time and > this must be the same on all reasonable implementations. How would you reconcile your category of "reasonable implementation" with all of the complexity-varying, all useful approaches to implementing string-ref that people talk about? What if scheme had immutable strings? Henry Baker sais this about functional strings in "Equal Rights for Functional Objects or, The More Things Change, The More They Are the Same" (which btw includes some really good arguments in favor of immutable objects) http://home.pipeline.com/~hbaker1/ObjectIdentity.html : "Functional strings can have interesting implementations. A representation of a string as a tree whose leaves are individual characters offers O(1) complexity concatenation; while element indexing is more expensive, it is usually less common than concatenation." Alexander ___ r6rs-discuss mailing list [email protected] http://lists.r6rs.org/cgi-bin/mailman/listinfo/r6rs-discuss
Re: [r6rs-discuss] [Formal] Formal semantics should not contain complicating optimizations
real world programming. That phrase gets tossed around too much. People fetishize the social role of the report in some pretty superstitious ways, I think. It's like looking for (or wishing for) a control point for all the wrong things in the wrong place. -t ___ r6rs-discuss mailing list [email protected] http://lists.r6rs.org/cgi-bin/mailman/listinfo/r6rs-discuss
Re: [r6rs-discuss] [Formal] Formal semantics should not contain complicating optimizations
David Van Horn wrote: Robby Findler wrote: The formal semantics makes no claim to let you reason about the space behavior of your program! You've said twice now that you think the formal semantics is incorrect. Your explanations of why don't seem right to me, but they are still vague. Please explain (unless you were talking about space both times?) The specification of eqv? (9.6) requires: (let ((p (lambda (x) x))) (eqv? x x)) ===> #t Sorry, this example should read: (let ((p (lambda (x) x))) (eqv? p p)) David ___ r6rs-discuss mailing list [email protected] http://lists.r6rs.org/cgi-bin/mailman/listinfo/r6rs-discuss
Re: [r6rs-discuss] [Formal] Formal semantics should not contain complicating optimizations
Robby Findler wrote: The formal semantics makes no claim to let you reason about the space behavior of your program! You've said twice now that you think the formal semantics is incorrect. Your explanations of why don't seem right to me, but they are still vague. Please explain (unless you were talking about space both times?) The specification of eqv? (9.6) requires: (let ((p (lambda (x) x))) (eqv? x x)) ===> #t But the substitution model and the eqv? rule in the formal semantics: P[(eqv? uproc uproc)] ---> unknown Seems to imply: (let ((p (lambda (x) x))) (eqv? x x)) ===> unknown The formal semantics is missing the location tags as described in 9.5.2, unless I am missing something (not unlikely). David ___ r6rs-discuss mailing list [email protected] http://lists.r6rs.org/cgi-bin/mailman/listinfo/r6rs-discuss
Re: [r6rs-discuss] [Formal] Formal semantics should not contain complicating optimizations
Mikael Tillenius wrote: Thomas Lord wrote: AndrevanTonder wrote: I would like to be able to reason about the space behaviour of a program using the formal semantics. Please, no. That would mean that an implementation which did not exhibit the space behavior you predict that way is not conforming. It sounds to me like you want a mathematical model of space behavior *of some particular implementations* (and, you'd want a proof that that model is consistent with the formal semantics). The formal semantics should describe, as far as practical, the constraints that apply to all implementations -- but nothing more. Please yes! ;-) If space and time behaviour cannot be entirely ignored in real world programming. While it is impossible to describe these in terms of seconds and bytes a programmer must be able to know whether an algorithm is O(1), O(n) or O(2^n) in terms of both space and time and this must be the same on all reasonable implementations. How would you reconcile your category of "reasonable implementation" with all of the complexity-varying, all useful approaches to implementing string-ref that people talk about? The report already recognizes this in some places, e.g. tail calls must not consume any storage and vector-ref is faster than list-ref (most probably O(1) and O(n)). Yes, some of that language probably needs cleaned-up, with particular attention to the "must v. should" distinction. My gosh, if we were to get to that point before the end of this year, in my view, it'll probably be evidence that R6 is shaping up nicely. However, I recognize that this is rarely (if ever) part of a language specification. It may be handy to think about observables. In some sense, the meaning of a program is how it modulates its output ports and responds to modulations of its input ports.There are some temporal constraints that relate those but mostly in the sense of modeling causality, not performance. It's useful to talk about atemporal mathematical objects that relate those modulations and that's the level of description I'd expect from a formal semantics. Formal operational models, of which it appears their can be many useful ones with critical differences among them, are interesting when we can see that they in fact satisfy the formal semantic constraints. -t /Mikael ___ r6rs-discuss mailing list [email protected] http://lists.r6rs.org/cgi-bin/mailman/listinfo/r6rs-discuss
Re: [r6rs-discuss] [Formal] Formal semantics should not contain complicating optimizations
Thomas Lord wrote: AndrevanTonder wrote: I would like to be able to reason about the space behaviour of a program using the formal semantics. Please, no. That would mean that an implementation which did not exhibit the space behavior you predict that way is not conforming. It sounds to me like you want a mathematical model of space behavior *of some particular implementations* (and, you'd want a proof that that model is consistent with the formal semantics). The formal semantics should describe, as far as practical, the constraints that apply to all implementations -- but nothing more. Please yes! ;-) If space and time behaviour cannot be entirely ignored in real world programming. While it is impossible to describe these in terms of seconds and bytes a programmer must be able to know whether an algorithm is O(1), O(n) or O(2^n) in terms of both space and time and this must be the same on all reasonable implementations. The report already recognizes this in some places, e.g. tail calls must not consume any storage and vector-ref is faster than list-ref (most probably O(1) and O(n)). However, I recognize that this is rarely (if ever) part of a language specification. /Mikael ___ r6rs-discuss mailing list [email protected] http://lists.r6rs.org/cgi-bin/mailman/listinfo/r6rs-discuss
Re: [r6rs-discuss] [Formal] Formal semantics should not contain complicating optimizations
AndrevanTonder wrote: I would like to be able to reason about the space behaviour of a program using the formal semantics. Please, no. That would mean that an implementation which did not exhibit the space behavior you predict that way is not conforming. It sounds to me like you want a mathematical model of space behavior *of some particular implementations* (and, you'd want a proof that that model is consistent with the formal semantics). The formal semantics should describe, as far as practical, the constraints that apply to all implementations -- but nothing more. -t Direct substitution can change a program's space behaviour from polynomial to exponential. Given this, as far a space behaviour is concerned, the current semantics is incorrect (compared with the body of the report). Andre ___ r6rs-discuss mailing list [email protected] http://lists.r6rs.org/cgi-bin/mailman/listinfo/r6rs-discuss ___ r6rs-discuss mailing list [email protected] http://lists.r6rs.org/cgi-bin/mailman/listinfo/r6rs-discuss
Re: [r6rs-discuss] [Formal] Formal semantics should not contain complicating optimizations
The formal semantics makes no claim to let you reason about the space behavior of your program! You've said twice now that you think the formal semantics is incorrect. Your explanations of why don't seem right to me, but they are still vague. Please explain (unless you were talking about space both times?) Robby On 3/15/07, AndrevanTonder <[EMAIL PROTECTED]> wrote: On Thu, 15 Mar 2007, Robby Findler wrote: >> This is not obvious to me. Doesn't simple substitution have the danger of >> leading to exponential explosion in size due to unnecessary copying of the >> argument throughout the body? I would think that this would happen for >> many >> common programs, making them harder to follow. > > Substitution is a very simple way to think of function application, > going back to some of our earliest exposure to mathematics in school > (at least in this country). I don't dispute that, but this is not how the text describes function application. While being pedagogical is not a bad secondary goal, a formal semantics must be correct first. I would like to be able to reason about the space behaviour of a program using the formal semantics. Direct substitution can change a program's space behaviour from polynomial to exponential. Given this, as far a space behaviour is concerned, the current semantics is incorrect (compared with the body of the report). Andre ___ r6rs-discuss mailing list [email protected] http://lists.r6rs.org/cgi-bin/mailman/listinfo/r6rs-discuss
Re: [r6rs-discuss] [Formal] Formal semantics should not contain complicating optimizations
On Thu, 15 Mar 2007, Robby Findler wrote: This is not obvious to me. Doesn't simple substitution have the danger of leading to exponential explosion in size due to unnecessary copying of the argument throughout the body? I would think that this would happen for many common programs, making them harder to follow. Substitution is a very simple way to think of function application, going back to some of our earliest exposure to mathematics in school (at least in this country). I don't dispute that, but this is not how the text describes function application. While being pedagogical is not a bad secondary goal, a formal semantics must be correct first. I would like to be able to reason about the space behaviour of a program using the formal semantics. Direct substitution can change a program's space behaviour from polynomial to exponential. Given this, as far a space behaviour is concerned, the current semantics is incorrect (compared with the body of the report). Andre ___ r6rs-discuss mailing list [email protected] http://lists.r6rs.org/cgi-bin/mailman/listinfo/r6rs-discuss
Re: [r6rs-discuss] [Formal] Formal semantics should not contain complicating optimizations
On 3/15/07, AndrevanTonder <[EMAIL PROTECTED]> wrote: On Thu, 15 Mar 2007, Robby Findler wrote: > This is not an "optimization" in the usual sense of the word (altho > one could make a case it is a cognitive optimization. Those seem good, > however). First, I suspect it may be incorrect. Doesn't simple substitution destroy the correct behaviour of eq? No. Second, I think it is a cognitive complication. It introduces a distinction that is never mentioned in the informal semantics, in fact clashing with a strict reading of the latter. A newcomer will see applications proceeding sometimes in one way and sometimes in another, depending on the presence of set! somewhere later in the code. Comparison with the informal description will lead to more surprise. > The rule is split like that to avoid complicating the semantics when > no assignments happen. The overall goal is to make it easier to follow > along with a reduction sequence and a simple substitution is easier to > follow along with than putting the variable into the store and taking > it back out again. At least it is in my experience. This is not obvious to me. Doesn't simple substitution have the danger of leading to exponential explosion in size due to unnecessary copying of the argument throughout the body? I would think that this would happen for many common programs, making them harder to follow. Substitution is a very simple way to think of function application, going back to some of our earliest exposure to mathematics in school (at least in this country). Robby ___ r6rs-discuss mailing list [email protected] http://lists.r6rs.org/cgi-bin/mailman/listinfo/r6rs-discuss
Re: [r6rs-discuss] [Formal] Formal semantics should not contain complicating optimizations
On Thu, 15 Mar 2007, Robby Findler wrote: This is not an "optimization" in the usual sense of the word (altho one could make a case it is a cognitive optimization. Those seem good, however). First, I suspect it may be incorrect. Doesn't simple substitution destroy the correct behaviour of eq? Second, I think it is a cognitive complication. It introduces a distinction that is never mentioned in the informal semantics, in fact clashing with a strict reading of the latter. A newcomer will see applications proceeding sometimes in one way and sometimes in another, depending on the presence of set! somewhere later in the code. Comparison with the informal description will lead to more surprise. The rule is split like that to avoid complicating the semantics when no assignments happen. The overall goal is to make it easier to follow along with a reduction sequence and a simple substitution is easier to follow along with than putting the variable into the store and taking it back out again. At least it is in my experience. This is not obvious to me. Doesn't simple substitution have the danger of leading to exponential explosion in size due to unnecessary copying of the argument throughout the body? I would think that this would happen for many common programs, making them harder to follow. Andre ___ r6rs-discuss mailing list [email protected] http://lists.r6rs.org/cgi-bin/mailman/listinfo/r6rs-discuss
Re: [r6rs-discuss] [Formal] Formal semantics should not contain complicating optimizations
This is not an "optimization" in the usual sense of the word (altho one could make a case it is a cognitive optimization. Those seem good, however). The rule is split like that to avoid complicating the semantics when no assignments happen. The overall goal is to make it easier to follow along with a reduction sequence and a simple substitution is easier to follow along with than putting the variable into the store and taking it back out again. At least it is in my experience. Robby On 3/14/07, AndrevanTonder <[EMAIL PROTECTED]> wrote: --- This message is a formal comment which was submitted to [EMAIL PROTECTED], following the requirements described at: http://www.r6rs.org/process.html --- Name: Andre van Tonder Email : andre at het.brown.edu Type: simplification Priority: low Component : Formal semantics Version : 5.92 Pages : 61-73 Dependencies: None Summary: The current formal semantics contains at least one, and possibly more, unnecessary performance optimizations that complicate it rather more than necessary. Such optimizations have no place in a formal description of the semantics and should be removed. Description: An example of such an optimization occurs on pages 69 and 70, where procedure parameters are treated differently depending on whether they are the target of set! in the body of the procedure. This is unnecessary. It clashes with the informal description in the body of the report, and it complicates the semantics with an unnecessary rule [6appN], and an unnecessary variable assigment metafunction that takes about 25 lines (more than half of page 70) to describe. Both of these, and possibly other rules depending on this distinction, should be removed. This is one unnecessary complication, presumably based on optimization considerations, that I noticed. A more careful reading may turn up other optimization-related complications. This formal comment is intended to apply to all cases where the formal semantics may be simplified by discarding optimizations. ___ r6rs-discuss mailing list [email protected] http://lists.r6rs.org/cgi-bin/mailman/listinfo/r6rs-discuss ___ r6rs-discuss mailing list [email protected] http://lists.r6rs.org/cgi-bin/mailman/listinfo/r6rs-discuss
