Support simultaneous substitutions

[rfindler]

Thanks for offering this change, @philnguyen !

I think it needs some documentation, and I'm wondering why overloading substitute in this way is the best choice (as compared to having a second function).

But mostly I wonder why calling substitute multiple times is a bad idea. I do see that calling substitute multiple times returns different results than the substitute in the PR (as in the example below) -- is that the rationale here?

#lang racket
(require redex/reduction-semantics)

(define-language λ
  (e ::= (λ (x) e) (e e) x)
  (x ::= variable-not-otherwise-mentioned)
  #:binding-forms
  (λ (x) e #:refers-to x))

(default-language λ)

(define t (term (λ (x) (λ (q) (w (x (y z)))))))
(term (substitute (substitute ,t y (λ (a) x)) z (λ (b) w)))
;; = (term (λ (x«2») (λ (q«3») (w (x«2» ((λ (a«4») x) (λ (b) w)))))))
(term (substitute ,t (y z) ((λ (a) x) (λ (b) w))))
;; = (term (λ (x«5») (λ (q«6») (w (x«5» ((λ (a) x) (λ (b) w)))))))

[rfindler]

Ah, I see why: the performance difference is significant, as in the below.

And maybe the reason for not introducing a new name is to avoid clashes with existing code. If so, did you consider something where the arguments to substitute are of this shape: (substitute <expr> (<x> <e>) ...)? It seems a bit nicer to keep the "x" next to "e" that its being replaced with.

#lang racket
(require redex/reduction-semantics)

(define-language λ
  (e ::= (λ (x) e) (e e) x)
  (x ::= variable-not-otherwise-mentioned)
  #:binding-forms
  (λ (x) e #:refers-to x))

(default-language λ)

(define size 4000)

(define t
  (let loop ([n size])
    (cond
      [(zero? n)
       (for/list ([i (in-range size)])
         (string->symbol (~a "x" i)))]
      [else (term (λ (,(string->symbol (~a "x" (- n 1))))
                    ,(loop (- n 1))))])))

(define vars (for/list ([i (in-range size)]) 'x))
(define rhses (for/list ([i (in-range size)]) 10))

(define (subst-n)
  (for/fold ([t t])
            ([var (in-list vars)]
             [rhs (in-list rhses)])
    (term (substitute ,t ,var ,rhs))))

(collect-garbage) (collect-garbage) (collect-garbage)
(define a2 (time (subst-n)))

(collect-garbage) (collect-garbage) (collect-garbage)
(define a1 (time (term (substitute ,t ,vars ,rhses))))

(test-equal a1 a2)
(test-results)

[philnguyen]

Thanks Robby! I updated the doc, changed the argument to (substitute <expr> (<x> <e>) ...), and updated the test to demonstrate where this would differ from applying each substitution one by one.

About the motivation, I think apart from performance, there are cases where it is useful?

For example, if we have the following:

(λxy. x y) y z

, my understanding is we can't just straightforwardly do the substitutions in sequence

(x y)[x -> y][y -> z]

, and we could either re-use the 1-arg substitute while keeping the remaining bindings untouched (e.g. (λy. x y)[x -> y] first, then [y -> z] on the resulting body with y renamed from capture-avoiding), or re-implement the simultaneous substitution in this PR?

[mfelleisen]

For the record, if we follow Barendregt and old logic books, a term such as

(λxy. x y) y z

is considered "not ready for reduction/substitution". Barendregt resolves this with "behind the scenes" alpha renaming. (Logic books did this explicitly.) So if PL theoreticians were to use the solid foundations laid out 40 years ago, redex would do so too. And for some reason I thought we were doing this after Paul. What I am missing here? (Then again, most PL theory people no longer know about Barendregt and his careful treatment of these issues. So perhaps it doesn't matter.)

[rfindler]

I think that maybe @philnguyen and @mfelleisen (or maybe Berendregt) have slightly different interpretations of the term λxy. x y. If you look at it as implicit currying, then doing the β reduction corresponds to these two calls to substitute, which works out fine and as matthias writes, the behind-the-scenes stuff is indeed happening, thanks to @paulstansifer .

> (term (substitute (λ (y) (x y)) x y))
'(λ (y«1») (y y«1»))
> (term (substitute (y y«1») y«1» z))
'(y z)

But if you think of it as a n-ary lambda and you try to recur and call substitute n times directly on the body of the lambda, you get the wrong answer:

> (term (substitute (substitute (x y) x y) y z))
'(z z)

What this means is that if you're using substitute and thinking of the n-ary style λ expressions, you need to write the β rule differently, as in the code below (the examples above were run in the REPL you get from the code below, if you want to try things out).

#lang racket
(require redex)

(define-language λ
  (e ::= (λ (x ...) e) (e e ...) x)
  (x ::= variable-not-otherwise-mentioned)
  #:binding-forms
  (λ (x) e #:refers-to x))

(default-language λ)

(define-judgment-form λ
  #:mode (--> I O)

  [------------------ β0
   (--> ((λ () e)) e)]

  [----------------------------------------------------- βn
   (--> ((λ (x_1 x_2 ...) e) e_1 e_2 ...)
        ((substitute (λ (x_2 ...) e) x_1 e_1) e_2 ...))])

(define-judgment-form λ
  #:mode (-->* I O)

  [----------- refl
   (-->* e e)]

  [(--> e_1 e_2) (-->* e_2 e_3)
   ---------------------------- tran
   (-->* e_1 e_3)])

(show-derivations
 (build-derivations
  (-->* ((λ (x y) (x y)) y z)
        (x_1 ...))))

[mfelleisen]

Yes I know :-)

1. Substitution demands the existence of an alpha equivalence relation.
2. Beta demands "ready for reduction" and that means the parameters and the arguments don't overlap in variables. ([Bar] sets up two conditions for hygiene; this is one of them and it naturally generalizes.)
3. When they do overlap, beta doesn't trigger and therefore a "hidden alpha" must take place first.

This should work in all cases. So I am baffled why it fails to work for Paul's extension. That's all.

[rfindler]

Is maybe the missing piece that the alpha renaming happens when destructuring the lambda (because it is listed as a binding form)? Does that plus the code examples help unbaffle? So when doing the let or the n-ary lambda we alpha-rename only once and then substitute twice, which is what makes it go wrong?

[rfindler]

Oops, there are two errors that I made in the discussion above.

But if you think of it as a n-ary lambda [...]

First, just below this quoted part, I wrote an example where I called substitute, but I called it wrongly; it won't be called like that in a rule; it'll be called with the freshened variables! So that was totally misleading.

The second error is that the binding-forms declaration should have been

  #:binding-forms
  (λ (x ...) e #:refers-to (shadow x ...))

[rfindler]

Oh, oops: looks like deftogether was the wrong thing, sorry! This is probably what the docs should have been:

diff --git a/redex-doc/redex/scribblings/ref/languages.scrbl b/redex-doc/redex/scribblings/ref/languages.scrbl
index 8a5844d..ac1e1bf 100644
--- a/redex-doc/redex/scribblings/ref/languages.scrbl
+++ b/redex-doc/redex/scribblings/ref/languages.scrbl
@@ -545,10 +545,9 @@ If the @racket[lang] argument is not supplied, it
 defaults to the value of @racket[(default-language)], which must not @racket[#f].
 }

-@deftogether[(@defform[#:kind "metafunction"
-                       (substitute val old-var new-val)]{}
-              @defform[#:kind "metafunction"
-                       (substitute val (old-var new-val) ...)]{})]{
+@defform*[#:kind "metafunction"
+          [(substitute val old-var new-val)
+           (substitute val (old-var new-val) ...)]]{
 A metafunction that returns a value like @racket[val], except that any free occurences of
 @racket[old-var] have been replaced with @racket[new-val], in a capture-avoiding fashion. The bound
 names of @racket[val] may be freshened in order to accomplish this, based on the binding information

[philnguyen]

I fixed that. Thanks!

[rfindler]

Thank you!