Confusing behavior: literals interpreted as variables for binding purposes about redex HOT 16 CLOSED

(I wonder if we should add some sort of debugging option to automatically print out freshening events as they happen; I add a printf to do that every time binding is doing something weird.)

In this case, the problem is that nothing, despite being a literal, it still being interpreted as a binder, and the form (machine nothing ()) is getting freshened to (machine nothing«0» ()). Using () or (nothing) instead of nothing makes the test pass.

What's going on is specific to variables. Redex has a simple rule: if a variable is referred to (either by #:refers-to or #:exports), it is a binder. Otherwise it's a reference. There is currently no provision for saying that a particular variable doesn't participate in binding at all. (So using (nothing) inside a context where the name nothing is bound will also result in bad stuff.)

I'm a little stumped here; I haven't used literals extensively in Redex, and I don't have an intuition for what a Redexy solution to this problem is (I'm thinking of it as a usability problem). Perhaps something as simple as saying that all literals (= names on the RHS of a rule but not on the LHS of any rule) are not variables, and so cannot be freshened?

(I don't think circularity has anything to do with it; I think it's just that if you take away those two rules, (machine nothing ()) is no longer a binding form, and so doesn't get freshened.)

from redex.

from redex.

This seems related to #68. Patterns and binding have unexpected behavior together. Consider the following program. Exactly one test fails, can you spot which?

(for the uninitiated,
(redex-judgment-holds-chk j [args ...] ...) is short for
(check-true (judgment-holds (j args ...))) ...)

#lang racket
(require redex/reduction-semantics)

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

(define-judgment-form λL
  #:mode (out1 I O)
  #:contract (out1 e e)

  [----------
   (out1 e e)])

(define-judgment-form λL
  #:mode (out2 I O)
  #:contract (out2 e e)

  [----------
   (out2 x x)]

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

(define-judgment-form λL
  #:mode (out3 I I)
  #:contract (out3 e e)

  [(out2 e_1 e_2)
   ----------
   (out3 e_1 e_2)])

(module+ test
  (require redex-chk)
  (redex-judgment-holds-chk
   out1
   [(λ (x) x) (λ (x) x)]
   [(λ (x_1 x_2) x_1) (λ (x_1 x_2) x_1)]
   [(λ (y z) z) (λ (y z) z)]
   [(λ (y z) z) (λ (x_1 x_2) x_2)])

  (redex-judgment-holds-chk
   out2
   [(λ (x) x) (λ (x) x)]
   [(λ (x_1 x_2) x_1) (λ (x_1 x_2) x_1)]
   [(λ (y z) z) (λ (y z) z)]
   [(λ (y z) z) (λ (x_1 x_2) x_2)])

  (redex-judgment-holds-chk
   out3
   [(λ (x) x) (λ (x) x)]
   [(λ (x_1 x_2) x_1) (λ (x_1 x_2) x_1)]
   [(λ (y z) z) (λ (y z) z)]
   [(λ (y z) z) (λ (x_1 x_2) x_2)]))

from redex.

Does it make sense to change the freshening process so that it just ignores literals? (I doubt this will help with @wilbowma 's example, but it probably will with the original symptom and #98)

from redex.

That makes a lot of sense. Can we do the dual process: turn literals that are in binding positions in a pattern into a fresh identifier pattern variable? (I think that's what's necessary to solve my example, but not sure it's possible. Also not sure it's desired behavior in 100% of patterns)

from redex.

from redex.

Ah sorry. I guess I was thinking of literals as arbitrary symbols that don't necessarily appear in the grammar, e.g., y and z in my above tests. In these cases, I think of them as variables, but Redex recognizes them as symbols in a pattern. Hence, (lambda (x) x) doesn't match the pattern (lambda (y) y).

My suggestion was, for these symbols, when they appear in a pattern and in binding position, can they be automatically turned into fresh pattern variables? For example, can we change (lambda (y z) y), when it appears as a pattern instead of a term, into (lambda (x_1 x_2) x_1)?

from redex.

I would to comment that I'm having this same issue, that identifiers that are supposed to be literals are treated as variable and thus incorrectly renamed.

from redex.

(define-language L
  [x ::= variable-not-otherwise-mentioned]
  [e ::= x null (cons e e) (λ p e)]
  [p ::= x null (cons p p)]
  #:binding-forms
  null #:exports nothing
  (λ p e #:refers-to p)
  (cons p_1 p_2) #:exports (shadow p_1 p_2))

(term (substitute (λ null null) x y) #:lang L)
;; '(λ null«0» null«0»)

Is there a workaround yet?

from redex.

I don't know if the commit I just pushed (19f48d2) solves the original problem in this PR. If @florence / @wilbowma would have a look, that'd be appreciated. (It does make the results for that first program in this thread be what @florence expected.)

from redex.

This is great, thanks @rfindler.

from redex.

Actually, looks like it breaks reduction relations.

(define red
  (reduction-relation L
    (--> e e)))

(traces red '(cons null null))
; α-equal-hash-code: arity mismatch;
;  the expected number of arguments does not match the given number
;   expected: 4
;   given: 3

from redex.

Whoops, sorry. (And there were already tests for those, I just didn't run them :( )

from redex.

@iitalics I missed the merge window with this fix. Is it important for this to get into a release, or shall I leave it as is (meaning it will be in a release only in 3 months from now)?

CC @stamourv

from redex.

Its not a big deal

from redex.

Thanks, though

from redex.