Variable capture in stepper's substitution

[racket-bug-submit]

Originally submitted on: Wed Oct 31 14:20:02 -0400 2007

When substituting a lambda term M into the body of another lambda term N, the stepper doesn't alpha-rename to avoid capturing free variables in M.

Steps to reproduce:

Stepping the program

(define x 42)

(define f (lambda (g) (lambda (x) (g x))))

((f (lambda (y) x)) 0)

reaches the term

(((lambda (g) (lambda (x) (g x))) (lambda (y) x)) 0)

which the stepper reduces to

((lambda (x) ((lambda (y) x) x)) 0)

capturing the free occurence of x.

This bug was converted from Gnats bug 9030.

[racket-bug-submit]

On Wed, 31 Oct 2007 14:27:27 -0400, matthias@ccs.neu.edu wrote:

It's just the illusion of capturing, it isn't real as this program
demonstrates:

(define x 42)

(define f
  (lambda (g)
    (lambda (x)
      (g 21))))

((f (lambda (y) x)) 0)

Of course, now it looks like the Stepper doesn't know what it is doing.

On Oct 31, 2007, at 2:20 PM, clklein@cs.uchicago.edu wrote:

A new problem report is waiting at http://bugs.plt-scheme.org/query/?cmd=view&pr=9030

Reported by Casey Klein for release: 371.3-svn31oct2007

*\ Description: When substituting a lambda term M into the body of another lambda
term N, the stepper doesn't alpha-rename to avoid capturing free
variables in M.

*\ How to repeat: Stepping the program

(define x 42)

(define f (lambda (g) (lambda (x) (g x))))

((f (lambda (y) x)) 0)

reaches the term

(((lambda (g) (lambda (x) (g x))) (lambda (y) x)) 0)

which the stepper reduces to

((lambda (x) ((lambda (y) x) x)) 0)

capturing the free occurence of x.

*\ Environment: unix "Linux radius.cs.uchicago.edu 2.6.18-5-686-bigmem #1 SMP Sun
Aug 12 23:05:22 UTC 2007 i686 GNU/Linux" (i386-linux/3m) (get- display-depth) = 16 Docs Installed: (("/var/tmp/plt/share/plt/doc" "r5rs" "mzscheme" "mred" "help"
"tour" "drscheme" "srfi" "mzlib" "misclib" "mrlib" "framework"
"foreign" "mzc" "tools" "insidemz" "web-server" "swindle" "plot"
"gui" "guide" "quick" "reference" "release-notes" "scribble" "t-y- scheme" "tex2page" "beginning" "beginning-abbr" "intermediate"
"intermediate-lambda" "advanced" "teachpack" "teachpack-htdc"
"profj-beginner" "profj-intermediate" "profj-intermediate-access"
"profj-advanced")) Human Language: english (current-memory-use) 95969284

Collections: (("/home/clklein/.plt-scheme/371.3/collects" non-existent-path) ("/ var/tmp/plt/lib/plt/collects" "afm" "big" "ffi" "net" "sgl" "xml"
"eopl" "help" "htdp" "html" "lang" "lazy" "make" "r5rs" "mred"
"plot" "srfi" "wxme" "framework" "teachpack" "handin-client"
"mzscheme" "games" "icons" "htdch" "mrlib" "mzcom" "mzlib"
"graphics" "profj" "setup" "tests" "trace" "xelda" "combinator- parser" "waterworld" "preprocessor" "sirmail" "test-box-recovery"
"skipper" "handin-server" "tex2page" "texpict" "scribblings"
"profjWizard" "stepper" "scribble" "web-server" "config" "compiler"
"swindle" "dynext" "hierlist" "macro-debugger" "frtime" "defaults"
"guibuilder" "drscheme" "syntax-color" "mrflow" "srpersist"
"mztake" "planet" "mysterx" "errortrace" "slatex" "syntax"
"version" "algol60" "honu-module" "parser-tools" "openssl"
"embedded-gui" "slideshow" "repos-time-stamp" "info-domain"
"readline" "launcher" "string-constants" "browser")) Computer Language: (("Teaching Languages" "How to Design Programs"
"Intermediate Student with lambda") (#6(#t quasiquote repeating- decimal #f #t none) #f ()))

[racket-bug-submit]

On Wed, 31 Oct 2007 13:37:23 -0500, robby@cs.uchicago.edu wrote:

Yes, just the illusion. Yes, the stepper looks bad. :)

Robby

On 10/31/07, Matthias Felleisen matthias@ccs.neu.edu wrote:

It's just the illusion of capturing, it isn't real as this program demonstrates:

(define x 42)

(define f
  (lambda (g)
    (lambda (x)
      (g 21))))

((f (lambda (y) x)) 0)

Of course, now it looks like the Stepper doesn't know what it is doing.

On Oct 31, 2007, at 2:20 PM, clklein@cs.uchicago.edu wrote:

A new problem report is waiting at http://bugs.plt-scheme.org/query/?cmd=view&pr=9030

Reported by Casey Klein for release: 371.3-svn31oct2007

*\ Description: When substituting a lambda term M into the body of another lambda term N, the stepper doesn't alpha-rename to avoid capturing free variables in M.

*\ How to repeat: Stepping the program

(define x 42)

(define f (lambda (g) (lambda (x) (g x))))

((f (lambda (y) x)) 0)

reaches the term

(((lambda (g) (lambda (x) (g x))) (lambda (y) x)) 0)

which the stepper reduces to

((lambda (x) ((lambda (y) x) x)) 0)

capturing the free occurence of x.

*\ Environment: unix "Linux radius.cs.uchicago.edu 2.6.18-5-686-bigmem #1 SMP Sun Aug 12 23:05:22 UTC 2007 i686 GNU/Linux" (i386-linux/3m) (get- display-depth) = 16 Docs Installed: (("/var/tmp/plt/share/plt/doc" "r5rs" "mzscheme" "mred" "help" "tour" "drscheme" "srfi" "mzlib" "misclib" "mrlib" "framework" "foreign" "mzc" "tools" "insidemz" "web-server" "swindle" "plot" "gui" "guide" "quick" "reference" "release-notes" "scribble" "t-y- scheme" "tex2page" "beginning" "beginning-abbr" "intermediate" "intermediate-lambda" "advanced" "teachpack" "teachpack-htdc" "profj-beginner" "profj-intermediate" "profj-intermediate-access" "profj-advanced")) Human Language: english (current-memory-use) 95969284

Collections: (("/home/clklein/.plt-scheme/371.3/collects" non-existent-path) ("/ var/tmp/plt/lib/plt/collects" "afm" "big" "ffi" "net" "sgl" "xml" "eopl" "help" "htdp" "html" "lang" "lazy" "make" "r5rs" "mred" "plot" "srfi" "wxme" "framework" "teachpack" "handin-client" "mzscheme" "games" "icons" "htdch" "mrlib" "mzcom" "mzlib" "graphics" "profj" "setup" "tests" "trace" "xelda" "combinator- parser" "waterworld" "preprocessor" "sirmail" "test-box-recovery" "skipper" "handin-server" "tex2page" "texpict" "scribblings" "profjWizard" "stepper" "scribble" "web-server" "config" "compiler" "swindle" "dynext" "hierlist" "macro-debugger" "frtime" "defaults" "guibuilder" "drscheme" "syntax-color" "mrflow" "srpersist" "mztake" "planet" "mysterx" "errortrace" "slatex" "syntax" "version" "algol60" "honu-module" "parser-tools" "openssl" "embedded-gui" "slideshow" "repos-time-stamp" "info-domain" "readline" "launcher" "string-constants" "browser")) Computer Language: (("Teaching Languages" "How to Design Programs" "Intermediate Student with lambda") (#6(#t quasiquote repeating- decimal #f #t none) #f ()))

[racket-bug-submit]

On Wed, 31 Oct 2007 12:59:48 -0700, clements@brinckerhoff.org wrote:

--Apple-Mail-7-805226706 Content-Transfer-Encoding: 7bit Content-Type: text/plain; charset=US-ASCII; delsp=yes; format=flowed

On Oct 31, 2007, at 11:20 AM, clklein@cs.uchicago.edu wrote:

A new problem report is waiting at http://bugs.plt-scheme.org/query/?cmd=view&pr=9030

Reported by Casey Klein for release: 371.3-svn31oct2007

*\ Description: When substituting a lambda term M into the body of another lambda
term N, the stepper doesn't alpha-rename to avoid capturing free
variables in M.

Yep.

Okay if I file this as a change-request?

John

[racket-bug-submit]

On Wed, 31 Oct 2007 15:45:12 -0500, clklein@cs.uchicago.edu wrote:

On Wed, Oct 31, 2007 at 12:59:48PM -0700, John Clements wrote:

On Oct 31, 2007, at 11:20 AM, clklein@cs.uchicago.edu wrote:

A new problem report is waiting at http://bugs.plt-scheme.org/query/?cmd=view&pr=9030

Reported by Casey Klein for release: 371.3-svn31oct2007

*\ Description: When substituting a lambda term M into the body of another lambda
term N, the stepper doesn't alpha-rename to avoid capturing free
variables in M.

Yep.

Okay if I file this as a change-request?

John

Sure.

[racket-bug-submit]

On Wed, 31 Oct 2007 16:57:21 -0400, clements classified this bug as change-request

change to the way the stepper currently operates

[racket-bug-submit]

On Wed, 31 Oct 2007 16:57:21 -0400, clements assigned this bug to clements

stepper issue

[racket-bug-submit]

On Wed, 31 Oct 2007 16:57:21 -0400, clements marked this bug as analyzed and wrote:

analyzed

[racket-bug-submit]

On Wed, 31 Oct 2007 16:07:37 -0500, robby@cs.uchicago.edu wrote:

This seems like a bug to me, too.

Robby

On 10/31/07, Matthias Felleisen matthias@ccs.neu.edu wrote:

Eh? It violates the specification! Your paper is not broken because you used closed lambda terms.

On Oct 31, 2007, at 4:57 PM, clements@plt-scheme.org wrote:

Class changed from "sw-bug" to "change-request" by clements at Wed, 31 Oct 2007 16:57:21 -0400 Reason>>> change to the way the stepper currently operates

Responsible changed from "nobody" to "clements" by clements at Wed, 31 Oct 2007 16:57:21 -0400 Reason>>> stepper issue

State changed from "open" to "analyzed" by clements at Wed, 31 Oct 2007 16:57:21 -0400 Reason>>> analyzed

View: http://bugs.plt-scheme.org/query/?cmd=view&pr=9030

[racket-bug-submit]

On Wed, 31 Oct 2007 17:03:48 -0400, matthias@ccs.neu.edu wrote:

Eh? It violates the specification! Your paper is not broken because
you used closed lambda terms.

On Oct 31, 2007, at 4:57 PM, clements@plt-scheme.org wrote:

Class changed from "sw-bug" to "change-request" by clements at Wed,
31 Oct 2007 16:57:21 -0400 Reason>>> change to the way the stepper currently operates

Responsible changed from "nobody" to "clements" by clements at Wed,
31 Oct 2007 16:57:21 -0400 Reason>>> stepper issue

State changed from "open" to "analyzed" by clements at Wed, 31 Oct
2007 16:57:21 -0400 Reason>>> analyzed

View: http://bugs.plt-scheme.org/query/?cmd=view&pr=9030

[racket-bug-submit]

On Wed, 31 Oct 2007 14:25:19 -0700, clements@brinckerhoff.org wrote:

On Oct 31, 2007, at 2:03 PM, Matthias Felleisen wrote:

Eh? It violates the specification! Your paper is not broken because
you used closed lambda terms.

Okay, okay...

The basic problem here is the top-level variables. That is, if the
"x" bound in the (lambda (y) x) term were a non-top-level variable,
it would be shown as (lambda (y) 42), rather than (lambda (y) x).

So, the apparent fix would be to perform renaming on all top-level
variables, not just those bound by a "local". Naturally, this would
only be necessary in languages where lambdas are displayed as inline
lambdas. That is, intermediate-with-lambda and up.

Sound good?

John Clements

[racket-bug-submit]

On Wed, 31 Oct 2007 16:33:53 -0500, robby@cs.uchicago.edu wrote:

Usually one renames bound identifiers to work around this (since free identifiers can't be freely renamed).

Robby

On 10/31/07, John Clements clements@brinckerhoff.org wrote:

On Oct 31, 2007, at 2:03 PM, Matthias Felleisen wrote:

Eh? It violates the specification! Your paper is not broken because you used closed lambda terms.

Okay, okay...

The basic problem here is the top-level variables. That is, if the "x" bound in the (lambda (y) x) term were a non-top-level variable, it would be shown as (lambda (y) 42), rather than (lambda (y) x).

So, the apparent fix would be to perform renaming on all top-level variables, not just those bound by a "local". Naturally, this would only be necessary in languages where lambdas are displayed as inline lambdas. That is, intermediate-with-lambda and up.

Sound good?

John Clements

[racket-bug-submit]

On Wed, 31 Oct 2007 17:51:07 -0400, matthias@ccs.neu.edu wrote:

I prefer John's solution. Works like a charm and is intuitive.
Except: how do you scale this to the set! language?

On Oct 31, 2007, at 5:33 PM, Robby Findler wrote:

Usually one renames bound identifiers to work around this (since free identifiers can't be freely renamed).

Robby

On 10/31/07, John Clements clements@brinckerhoff.org wrote:

On Oct 31, 2007, at 2:03 PM, Matthias Felleisen wrote:

Eh? It violates the specification! Your paper is not broken because you used closed lambda terms.

Okay, okay...

The basic problem here is the top-level variables. That is, if the "x" bound in the (lambda (y) x) term were a non-top-level variable, it would be shown as (lambda (y) 42), rather than (lambda (y) x).

So, the apparent fix would be to perform renaming on all top-level variables, not just those bound by a "local". Naturally, this would only be necessary in languages where lambdas are displayed as inline lambdas. That is, intermediate-with-lambda and up.

Sound good?

John Clements

[racket-bug-submit]

On Wed, 31 Oct 2007 16:55:47 -0500, robby@cs.uchicago.edu wrote:

You can rename the set!s too, no?

I actually think that the other is more intuitive, at least once you take a slightly deeper look. (At first glance, no, I agree with that.)

Robby

On 10/31/07, Matthias Felleisen matthias@ccs.neu.edu wrote:

I prefer John's solution. Works like a charm and is intuitive. Except: how do you scale this to the set! language?

On Oct 31, 2007, at 5:33 PM, Robby Findler wrote:

Usually one renames bound identifiers to work around this (since free identifiers can't be freely renamed).

Robby

On 10/31/07, John Clements clements@brinckerhoff.org wrote:

On Oct 31, 2007, at 2:03 PM, Matthias Felleisen wrote:

Eh? It violates the specification! Your paper is not broken because you used closed lambda terms.

Okay, okay...

The basic problem here is the top-level variables. That is, if the "x" bound in the (lambda (y) x) term were a non-top-level variable, it would be shown as (lambda (y) 42), rather than (lambda (y) x).

So, the apparent fix would be to perform renaming on all top-level variables, not just those bound by a "local". Naturally, this would only be necessary in languages where lambdas are displayed as inline lambdas. That is, intermediate-with-lambda and up.

Sound good?

John Clements

[racket-bug-submit]

On Wed, 31 Oct 2007 15:03:09 -0700, jacobm@cs.uchicago.edu wrote:

On Oct 31, 2007 2:51 PM, Matthias Felleisen matthias@ccs.neu.edu wrote:

I prefer John's solution. Works like a charm and is intuitive.

Unless I'm missing something it won't work for toplevel names that are introduced by imports, such as bindings from teachpacks or builtins. Consider

(define (g f) (lambda (cons) (f cons empty)))

(g cons)

This is exactly the free-variable capture problem (treating variables that aren't bound in the source code of the program as free). IMHO it's probably not worthwhile to try for a `simpler' solution than the standard one.

-jacob

On Oct 31, 2007, at 5:33 PM, Robby Findler wrote:

Usually one renames bound identifiers to work around this (since free identifiers can't be freely renamed).

Robby

On 10/31/07, John Clements clements@brinckerhoff.org wrote:

On Oct 31, 2007, at 2:03 PM, Matthias Felleisen wrote:

Eh? It violates the specification! Your paper is not broken because you used closed lambda terms.

Okay, okay...

The basic problem here is the top-level variables. That is, if the "x" bound in the (lambda (y) x) term were a non-top-level variable, it would be shown as (lambda (y) 42), rather than (lambda (y) x).

So, the apparent fix would be to perform renaming on all top-level variables, not just those bound by a "local". Naturally, this would only be necessary in languages where lambdas are displayed as inline lambdas. That is, intermediate-with-lambda and up.

Sound good?

John Clements

[racket-bug-submit]

On Wed, 31 Oct 2007 17:07:59 -0500, robby@cs.uchicago.edu wrote:

I just meant that if you think for a moment, renaming bound variables makes sense. If you don't think much, renaming the globals is fine. If you think harder yet again, you realize that the globals are in fact bound too, but that's 2 levels in, from what I can tell.

Anways, I think Jacob's point trumps all this.

Robby

On 10/31/07, John Clements clements@brinckerhoff.org wrote:

On Oct 31, 2007, at 2:55 PM, Robby Findler wrote:

You can rename the set!s too, no?

I actually think that the other is more intuitive, at least once you take a slightly deeper look. (At first glance, no, I agree with that.)

This last sentence is surely one of the most fascinating last sentences of any e-mail I've ever receieved... :).

I agree with Robby on his first point; I don't see the problem example with set! and renaming of top-level variables. I do see a problem with set! of non-top-level variables, but fortunately none of the teaching languages (incl. Advanced) make this possible (at least, not the last time I checked).

WRT the intuitiveness of the solution: I think that my proposal is more consistent with the treatment of local in intermediate. From a pragmatic standpoint, it's definitely a smaller change to the code. I think this also lends credence to my prior sentence.

(Followups trimmed.)

John

[racket-bug-submit]

On Wed, 31 Oct 2007 15:06:47 -0700, clements@brinckerhoff.org wrote:

On Oct 31, 2007, at 3:03 PM, Jacob Matthews wrote:

On Oct 31, 2007 2:51 PM, Matthias Felleisen matthias@ccs.neu.edu
wrote:

I prefer John's solution. Works like a charm and is intuitive.

Unless I'm missing something it won't work for toplevel names that are introduced by imports, such as bindings from teachpacks or builtins. Consider

(define (g f) (lambda (cons) (f cons empty)))

(g cons)

This is exactly the free-variable capture problem (treating variables that aren't bound in the source code of the program as free). IMHO it's probably not worthwhile to try for a `simpler' solution than the standard one.

I was hoping to be able to report that this was illegal, but it's not.

John

[racket-bug-submit]

On Wed, 31 Oct 2007 15:05:28 -0700, clements@brinckerhoff.org wrote:

On Oct 31, 2007, at 2:55 PM, Robby Findler wrote:

You can rename the set!s too, no?

I actually think that the other is more intuitive, at least once you take a slightly deeper look. (At first glance, no, I agree with that.)

This last sentence is surely one of the most fascinating last
sentences of any e-mail I've ever receieved... :).

I agree with Robby on his first point; I don't see the problem
example with set! and renaming of top-level variables. I do see a
problem with set! of non-top-level variables, but fortunately none of
the teaching languages (incl. Advanced) make this possible (at least,
not the last time I checked).

WRT the intuitiveness of the solution: I think that my proposal is
more consistent with the treatment of local in intermediate. From a
pragmatic standpoint, it's definitely a smaller change to the code. I
think this also lends credence to my prior sentence.

(Followups trimmed.)

John

[racket-bug-submit]

On Wed, 31 Oct 2007 17:06:16 -0500, robby@cs.uchicago.edu wrote:

Oh! I had just assumed that shadowing top-level names would be an error in the teaching languages, but I see that it isn't.

Perhaps we should make it be?

Robby

On 10/31/07, Jacob Matthews jacobm@cs.uchicago.edu wrote:

On Oct 31, 2007 2:51 PM, Matthias Felleisen matthias@ccs.neu.edu wrote:

I prefer John's solution. Works like a charm and is intuitive.

Unless I'm missing something it won't work for toplevel names that are introduced by imports, such as bindings from teachpacks or builtins. Consider

(define (g f) (lambda (cons) (f cons empty)))

(g cons)

This is exactly the free-variable capture problem (treating variables that aren't bound in the source code of the program as free). IMHO it's probably not worthwhile to try for a `simpler' solution than the standard one.

-jacob

On Oct 31, 2007, at 5:33 PM, Robby Findler wrote:

Usually one renames bound identifiers to work around this (since free identifiers can't be freely renamed).

Robby

On 10/31/07, John Clements clements@brinckerhoff.org wrote:

On Oct 31, 2007, at 2:03 PM, Matthias Felleisen wrote:

Eh? It violates the specification! Your paper is not broken because you used closed lambda terms.

Okay, okay...

The basic problem here is the top-level variables. That is, if the "x" bound in the (lambda (y) x) term were a non-top-level variable, it would be shown as (lambda (y) 42), rather than (lambda (y) x).

So, the apparent fix would be to perform renaming on all top-level variables, not just those bound by a "local". Naturally, this would only be necessary in languages where lambdas are displayed as inline lambdas. That is, intermediate-with-lambda and up.

Sound good?

John Clements

[racket-bug-submit]

On Wed, 31 Oct 2007 18:08:06 -0400, matthias@ccs.neu.edu wrote:

Same here. How silly I am.

On Oct 31, 2007, at 6:06 PM, Robby Findler wrote:

Oh! I had just assumed that shadowing top-level names would be an error in the teaching languages, but I see that it isn't.

Perhaps we should make it be?

Robby

On 10/31/07, Jacob Matthews jacobm@cs.uchicago.edu wrote:

On Oct 31, 2007 2:51 PM, Matthias Felleisen matthias@ccs.neu.edu
wrote:

I prefer John's solution. Works like a charm and is intuitive.

Unless I'm missing something it won't work for toplevel names that
are introduced by imports, such as bindings from teachpacks or builtins. Consider

(define (g f) (lambda (cons) (f cons empty)))

(g cons)

This is exactly the free-variable capture problem (treating variables that aren't bound in the source code of the program as free). IMHO it's probably not worthwhile to try for a `simpler' solution than the standard one.

-jacob

On Oct 31, 2007, at 5:33 PM, Robby Findler wrote:

Usually one renames bound identifiers to work around this (since
free identifiers can't be freely renamed).

Robby

On 10/31/07, John Clements clements@brinckerhoff.org wrote:

On Oct 31, 2007, at 2:03 PM, Matthias Felleisen wrote:

Eh? It violates the specification! Your paper is not broken
because you used closed lambda terms.

Okay, okay...

The basic problem here is the top-level variables. That is, if
the "x" bound in the (lambda (y) x) term were a non-top-level
variable, it would be shown as (lambda (y) 42), rather than (lambda (y) x).

So, the apparent fix would be to perform renaming on all top-level variables, not just those bound by a "local". Naturally, this
would only be necessary in languages where lambdas are displayed as
inline lambdas. That is, intermediate-with-lambda and up.

Sound good?

John Clements