Terms with #:...bind are alpha-equivalent?, but don't redex-match? about redex HOT 11 CLOSED

FWIW, seems to predate #67

from redex.

Yes; it is in 6.5, for example.

from redex.

Further work finds this may not be related to redex-match? or #:...bind, as part of the test suite was incorrect. See the modified version below. I think it was illegal to use y and z as binding names in the pattern. This does not explain why the judgment doesn't hold, though.

#lang racket/base
(require redex/reduction-semantics)

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

(define-judgment-form lc
  #:mode (translate I O)
  #:contract (translate e e)

  [(translate x x)]

  [(translate e_f1 e_f2)
   (translate e_a1 e_a2) ...
   ----------------------------------------
   (translate (e_f1 e_a1 ...) (e_f2 e_a2 ...))]

  [(translate e_1 e_2)
   --------------------------------------------
   (translate (λ x ... e_1) (λ x ... e_2))])

(module+ test
  (require rackunit racket/function)
  ;; Unnested
  (check-true
   (redex-match? lc (λ x x) (term (λ x x))))
  (check-true
   (redex-match? lc (λ x x) (term (λ y y))))
  (check-true
   (judgment-holds (translate (λ x x) (λ x x))))
  ;; fails
  (check-true
   (judgment-holds (translate (λ y y) (λ y y))))
  ;; Nested
  (check
   (curry alpha-equivalent? lc)
   (term (λ x y z x))
   (car (judgment-holds (translate (λ x y z x) e) e)))
  (check-true
   (redex-match? lc (λ x x_1 x_2 x) (term (λ x y z x))))
  (check-true
   (judgment-holds (translate (λ x x_1 x_2 x) (λ x x_1 x_2 x))))
  ;; fails
  (check-true
   (judgment-holds (translate (λ x y z x) (λ x y z x)))))

from redex.

Definitely related to binding; if I disable the #:binding-forms declarations, these all pass. But doesn't seem related to #:...bind in particular.

from redex.

No longer sure this is a bug per se, but perhaps a usability issue: (check-true (judgment-holds (translate (λ y y) (λ x x)))) passes.

Since y is renamed when decending under the binder, the name y no longer matches. It works when using the name x because x is also a non-terminal, so the renamed x matches as an x non-terminal.

from redex.

I think we would need @paulstansifer to ring in here, but after looking at this code for a little while, I think you just can't do that. Maybe.

I think I see what you're trying to do, and what's stopping the process is the two occurrences of x in the λ case aren't the same variable any more. Is that what you're seeing too?

from redex.

My understanding is that (check-true (judgment-holds (translate (λ y y) (λ y y)))) fails because y gets renamed, and hence the output pattern no longer matches "literally the name y".
(check-true (judgment-holds (translate (λ y y) (λ x x)))) works because y is renamed consistently, and this output pattern matches "some name x"

from redex.

Oh, of course. I just realized that, only to come back here and find your comment. So: yes.

Are we in agreement that everything is fine with the implementation (but that this is a subtle point to be aware of and perhaps improve the documentation somewhere or something?) And if translate actually did some translation, you might write:

(judgment-holds (translate (λ x x) (λ x_2 x_2)))

from redex.

Exactly.

from redex.

Thanks.

from redex.

Sorry to raise the dead, but I finally have a workaround for this. It may make sense to merge it into Redex, as it makes testing I/O judgments much easier, but otherwise I'll leave it here for those that might come looking: https://gist.github.com/wilbowma/c230a3d165262e8c68401769ba2dcbc3

from redex.