Comments (16)
(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.
Related Issues (20)
- Feature request: tag-with-names for apply-reduction-relation* HOT 2
- test-->>∃ #:steps n passes test if n > than the number of actual reduction steps for a term. HOT 4
- `traces` doesn't draw arrows after "fix layout" HOT 5
- `stepper` doesn't display whole term... unless I *narrow* its box?
- Feature Request: `stepper` with judgment-form use rule names
- Feature request: adjust font for `stepper` HOT 3
- Redex rejects literals at different ellipsis depths in binding form declarations HOT 1
- Generating random expressions sometimes results in an infinite loop
- where/error failures give no information about source of error HOT 6
- where/error failures don't tell you what failed to match
- using judgment-holds within define-relation HOT 1
- Redex's reduction graph windows sneakily hide part of term reductions HOT 1
- where/error doesn't report errors sometimes HOT 8
- define-metafunction does not check type signature on LHS HOT 3
- Docs missing a word I can't fill in. HOT 1
- `derivation/ps` always causes an error by calling a non-existent method HOT 1
- Default rendering font changed between Racket v8.8 and v8.9? HOT 4
- Redex PDF output contains a wrong font, while Racket REPL renders the correct font HOT 2
- Reduce space between rendered rules of a judgement form HOT 3
- `traces/ps` doesn't render arrows HOT 1
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from redex.