Comments (11)
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.
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.