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

[wilbowma]

#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)
  ;; single binder; passes
  (check-true
   (redex-match? lc (λ x x) (term (λ x x))))
  (check-true
   (judgment-holds (translate (λ x x) (λ x x))))
  ;; many binders; fails
  (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 y z x) (term (λ x y z x))))
  (check-true
   (judgment-holds (translate (λ x y z x) (λ x y z x)))))

[wilbowma]

FWIW, seems to predate #67

[rfindler]

Yes; it is in 6.5, for example.

[wilbowma]

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)))))

[wilbowma]

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

[wilbowma]

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.

[rfindler]

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?

[wilbowma]

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"

[rfindler]

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)))

[wilbowma]

Exactly.

[rfindler]

Thanks.

[wilbowma]

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